研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 245 件中 1 - 20 件目／全件表示 >>

Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms 査読有り国際誌

Naoki Nishida, Misaki Kojima, and Takumi Kato

Journal of Logical and Algebraic Methods in Programming 145 巻頁： 1 - 18 2025年5月

担当区分：筆頭著者,　責任著者記述言語：英語掲載種別：研究論文（学術雑誌）出版者・発行元：Elsevier

To transform an imperative program into a logically constrained term rewrite system (LCTRS, for short), previous work transforms a list of statements into rewrite rules in a stepwise manner, and proves the correctness along the transformation and the big-step semantics of the program. On the other hand, the small-step semantics of a programming language consists of inference rules that define single transitions of configurations. Partial instances of such inference rules are almost the same as rewrite rules in the transformed LCTRS. In this paper, we aim at establishing a framework for simpler definitions and correctness proofs of transformations from programs into LCTRSs. To this end, for the transformation in previous work as an example, we show the existence of an injective function from configurations of a given program to terms, and reformulate the transformation by means of the injective function. The injective function enables us to make a one-to-one correspondence between single small-step transitions and reduction steps, and provides bisimilarity between the program and transformed LCTRS, resulting in a simpler correctness proof.

DOI： 10.1016/j.jlamp.2025.101056

A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems 査読有り国際誌

Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

Journal of Logical and Algebraic Methods in Programming 144 巻頁： 1 - 15 2025年3月

担当区分：筆頭著者,　責任著者記述言語：英語掲載種別：研究論文（学術雑誌）出版者・発行元：Elsevier

In the last decade, several transformations of an imperative program into a logically constrained term rewrite system (LCTRS, for short) have been investigated and extended. They do not preserve the nesting of statements, generating rewrite rules like transition systems, while function calls are represented by the nesting of function symbols. Structural features of the original program must often be useful in analyzing the transformed LCTRS. To use such features, we have to know how to transform the program into the LCTRS by keeping the correspondence between statements in the program and the introduced auxiliary function symbols in the LCTRS, or by transforming the LCTRS into a control flow graph to, e.g., recover loop information. In this paper, we propose a nesting-preserving transformation of a SIMP program (a C-like integer program) into an LCTRS. The transformation is mostly based on previous work and introduces the nesting of function symbols that correspond to the nesting of statements in the original program. To be more precise, we propose a construction of a tree homomorphism which is used as a post-process of the transformation in previous work, i.e., which is applied to the LCTRS obtained from the program. As a correctness statement for the nesting-preserving transformation, we show that the tree homomorphism is sound and complete for the reduction of the LCTRS.

DOI： 10.1016/j.jlamp.2025.101045

Transforming concurrent programs with semaphores into logically constrained term rewrite systems 査読有り国際誌

Misaki Kojima, Naoki Nishida, Yutaka Matsubara

Journal of Logical and Algebraic Methods in Programming 143 巻頁： 1 - 23 2025年2月

担当区分：責任著者記述言語：英語掲載種別：研究論文（学術雑誌）出版者・発行元：Elsevier

In this paper, as a first step of modeling concurrent programs by logically constrained term rewrite systems (LCTRSs, for short), we show transformations of concurrent programs with semaphore-based exclusive control into LCTRSs. To this end, we show how to encode configurations of concurrent programs with a fixed number of processes. Then, we show how to encode some well-known operations for semaphores by rewrite rules, showing two transformations of concurrent programs with semaphores into LCTRSs. We adopt list-using and list-free approaches to the encoding of waiting queues for semaphores in LCTRSs. While the former straightforwardly uses lists, the latter uses a so-called take-a-number system in order to avoid using any recursive data structures for waiting queues.

DOI： 10.1016/j.jlamp.2024.101033

On Solving All-Path Reachability Problems for Starvation Freedom of Concurrent Rewrite Systems Under Process Fairness 査読有り国際誌

Misaki Kojima and Naoki Nishida

Proceedings of the 18th International Conference on Reachability Problems (RP 2024) 15050 巻頁： 54 - 70 2024年9月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）出版者・発行元：Springe, Cham

Logically constrained term rewrite systems are useful models of not only sequential but also concurrent programs. We have proposed a framework to soundly reduce starvation freedom of a concurrent program to an all-path reachability problem of the corresponding logically constrained term rewrite system, where process fairness is not considered. In this paper, we show a disproof criterion for starvation freedom and then extend the framework to starvation freedom under process fairness.

DOI： 10.1007/978-3-031-72621-7_5

制約付き書換え帰納法による証明における選言型制約を持つ等式の分割の完全性について

平等望, 西田直樹, 酒井正彦

令和6年度電気・電子・情報関係学会東海支部連合大会講演論文集 ( H6-4 ) 頁： 1 2024年8月

CRaris: CR checker for LCTRSs in ARI Style

Naoki Nishida and Misaki Kojima

Proceedings of the 13th International Workshop on Confluence 頁： 83 - 84 2024年7月

On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs 査読有り

Misaki Kojima and Naoki Nishida

Proceedings of the 13th International Workshop on Confluence 頁： 2 - 8 2024年7月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（研究会，シンポジウム資料等）

A logically constrained term rewrite system (LCTRS, for short) modeling a concurrent program is usually non-terminating, left-linear, and overlapping, but sometimes confluent w.r.t. an initial ground term which corresponds to an initial configuration of the program. In this paper, we show how to prove confluence of such an LCTRS w.r.t. the initial term. To be more precise, we add the rule from the initial term to a fresh constant to the LCTRS, and construct a proof tree for the all-path reachability problem from the initial term to the constant. If the directed graph obtained from the proof tree by considering it as a cyclic proof is strongly connected and each node corresponds to a single term, then all terms reachable from the initial term can be reduced back to the initial one and thus the original LCTRS is confluent w.r.t. the initial one.

CO3 (Version 2.5)

Naoki Nishida and Misaki Kojima

Proceedings of the 13th International Workshop on Confluence 頁： 71 - 72 2024年7月

Equational Theories and Validity for Logically Constrained Term Rewriting 査読有り国際共著

Takahito Aoto, Naoki Nishida, and Jonas Schöpf

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2018), LIPIcs 299 巻頁： 31:1 - 31:21 2024年7月

担当区分：筆頭著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derives a new notion of consistency for constrained equational theories.

DOI： 10.4230/LIPIcs.FSCD.2024.31

A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations 査読有り国際誌

Misaki Kojima and Naoki Nishida

Journal of Information Processing 32 巻頁： 417 - 435 2024年5月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（学術雑誌）出版者・発行元：Information Processing Society of Japan

An all-path reachability (APR, for short) problem of a logically constrained term rewrite system (LCTRS, for short) is a pair of constrained terms representing state sets. An APR problem is demonically valid if every finite execution path from any state in the first set to an irreducible state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by an LCTRS to an APR problem with irreducible constant destinations. In this paper, by focusing on quasi-termination of constrained narrowing, we characterize a class of LCTRSs of which APR problems with constant destinations are decidable. Quasi-termination of a (constrained) term w.r.t. narrowing is the finiteness of the set of reachable narrowed (constrained) terms from the initial (constrained) term up to variable renaming (and equivalence of constraints). To this end, we first introduce an inference rule for disproofs to a proof system for APR problems with constant destinations and formulate (dis)proof trees of APR problems in the style of cyclic proofs. Secondly, to prove correctness of disproof trees, we adapt constrained narrowing to LCTRSs and show soundness of constrained narrowing of LCTRSs w.r.t. constrained rewriting. Thirdly, we show a sufficient condition of LCTRSs for quasi-termination of constrained narrowing starting from linear constrained terms that have no nesting of defined symbols: Rewrite rules are right-linear and nesting-free w.r.t. defined symbols, and the application of rewrite rules for (mutually) recursive defined symbols does not increase the height of resulting constrained terms of narrowing. Finally, we show that if a constrained term is quasi-terminating w.r.t. narrowing of an LCTRS over a sort-wise finite signature with a decidable theory, then the APR problem consisting of the constrained term and an irreducible constant is decidable.

DOI： 10.2197/ipsjjip.32.417

Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting 査読有り国際誌

Misaki Kojima and Naoki Nishida

Journal of Logical and Algebraic Methods in Programming 135 巻頁： 1 - 19 2023年10月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（学術雑誌）

A concurrent program with semaphore-based exclusive control can be modeled by a logically constrained term rewrite system. In this paper, we first propose a framework to reduce the non-occurrence of a specified runtime error in the program to an all-path reachability problem of the transformed logically constrained term rewrite system. Here, an all-path reachability problem of the system is a pair of state sets and is demonically valid if every finite execution path starting with a state in the first set and ending with a terminating state includes a state in the second set. Then, we propose a weakened but easily-implementable variant of an existing proof system for all-path reachability problems. As a case study, we deal with the race freedom of concurrent programs with semaphore-based exclusive control.

DOI： 10.1016/j.jlamp.2023.100903

On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic 査読有り

Ayuka Mastumi, Naoki Nishida, Misaki Kojima, and Donghoon Shin

Proceedings of the 19th International Workshop on Termination 頁： 1 - 6 2023年8月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（研究会，シンポジウム資料等）

As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewrite systems (LCTRSs, for short). However, the polynomial interpretation processor is not so effective against LCTRSs with bit-vector arithmetic (BV-LCTRSs, for short). In this paper, we propose a novel DP processor for BV-LCTRSs to solve a singleton DP problem consisting of a dependency pair forming a self-loop. The processor is based on an acyclic directed graph such that the nodes are bit-vectors and any dependency chain of the problem is projected to a path of the graph. We show a sufficient condition for the existence of such an acyclic graph, and simplify it for a specific case.

DOI： 10.48550/arXiv.2307.14094

CO3 (Version 2.4)

Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

Proceedings of the 12th International Workshop on Confluence 頁： 67 2023年8月

A New Format for Rewrite Systems 査読有り国際共著

Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schöpf, Kiraku Shintani, Rene Thiemann, and Akihisa Yamada

Proceedings of the 12th International Workshop on Confluence 頁： 32 - 37 2023年8月

On Representations of Waiting Queues for Semaphores in Logically Constrained Term Rewrite Systems 査読有り

Misaki Kojima and Naoki Nishida

Informal Proceedings of the 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2023) 頁： 1 - 6 2023年7月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

A transformation of concurrent programs with semaphore-based exclusive control and waiting queues into logically constrained term rewrite systems (LCTRSs, for short) has been proposed. To represent waiting queues, the transformation adopts a turn waiting system with number tickets, while the use of usual lists is a straightforward approach. In this abstract, we show a list-based approach to waiting queues and compare the two approaches by means of verification of race freedom of a simple reader-writer example.

A Nesting-Preserving Transformation of SIMP Programs into Logically Constrained Term Rewrite Systems 査読有り

Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

Informal Proceedings of the 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2023) 頁： 1 - 11 2023年7月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

In the last decade, several transformations of an imperative program into a logically constrained term rewrite system (LCTRS, for short) have been investigated and extended. They do not preserve the nesting of statements, generating rewrite rules like transition systems, while function calls are represented by the nesting of function symbols. Structural features of the original program must be often useful in analyzing the transformed LCTRS, but, to use such features, we have to know how to transform the program into the LCTRS, e.g., we keep the correspondence between statements in the program and the introduced auxiliary function symbols in the LCTRS. In this paper, we propose a nesting-preserving transformation of a SIMP program (a C integer program) into an LCTRS. The transformation is almost based on previous work and introduces the nesting of function symbols that correspond to statements in the original program. To be more precise, we propose a construction of a tree homomorphism which is used as a post-process of the transformation in previous work, i.e., which is applied to the LCTRS obtained from the program. As a correctness of the nesting-preserving transformation, we show that the tree homomorphism is sound and complete for the reduction of the LCTRS.

ビットベクトル制約付き項書換え系の停止性証明のための多項式解釈プロセッサについて

松見歩佳，西田直樹，小嶋美咲，申東訓

電子情報通信学会技術報告 122 巻 ( 432 ) 頁： 85 - 90 2023年3月

担当区分：責任著者記述言語：日本語掲載種別：研究論文（研究会，シンポジウム資料等）

ビットベクトル制約付き項書換え系（BV-LCTRS）はC言語などのプログラムのモデルとして有用である．等価性検証に書換え帰納法を用いる際には，与えられた書換え系に帰納法の仮定となる書換え規則を加えて得られる書換え系の停止性が何度も証明される. LCTRSの停止性証明には項書換え系と同様に依存対プロセッサを使用して証明する枠組みの依存対フレームワークが用いられるが，整数制約を持つLCTRSの停止性証明において最も強力なプロセッサの1つである多項式解釈プロセッサはBV-LCTRSには適用できない．本稿では，BV-LCTRSの停止性証明を強化することを目的として，新たな依存対プロセッサとしてビットベクトル上の多項式解釈プロセッサと単一自己ループ除去プロセッサを提案する．

From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting 査読有り国際誌

Misaki Kojima and Naoki Nishida

Proceedings of the 25th International Symposium on Practical Aspects of Declarative Languages, Lecture Notes in Computer Science 13880 巻頁： 161 - 179 2023年1月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）出版者・発行元：Springer, Cham

An all-path reachability problem of a logically constrained term rewrite system is a pair of constrained terms representing state sets, and is demonically valid if every finite execution path from any state in the first set to a terminating state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by a logically constrained term rewrite system to an all-path reachability problem of the system. In this paper, we extend the framework to verification of starvation freedom of asynchronous integer transition systems with shared variables such that some processes enter critical sections.

DOI： 10.1007/978-3-031-24841-2_11

CO3 (Version 2.3)

Naoki Nishida and Misaki Kojima

Proceedings of the 11th International Workshop on Confluence 頁： 63 2022年8月

Confluence Competition 2022 国際共著

Raul Gutierrez, Aart Middeldorp, Naoki Nishida, and Kiraku Shintani

Proceedings of the 11th International Workshop on Confluence 頁： 54 2022年8月

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹