研究者詳細 - 西田　直樹

論文 - 西田　直樹

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

アージェントロケーションを持つUppaal記述から論理制約付き項書き換え系への変換について

田辺竣也, 小嶋美咲, 西田直樹, 酒井正彦

情報処理学会第88回全国大会講演論文集頁： 249 - 250 2026年3月

制約付き書換えにおける複数の項に関する合流性の同時証明のためのナローインググラフについて

難波美優, 小嶋美咲, 西田直樹, 酒井正彦

情報処理学会第88回全国大会講演論文集頁： 251 - 252 2026年3月

Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems 査読有り国際誌 Open Access

Naoki Nishida, Misaki Kojima, and Yuto Nakamura

Proceedings of the 15th International Symposium on Frontiers of Combining Systems (FroCoS 2025), Lectures Notes in Computer Science 15979 巻頁： 247 - 266 2025年9月

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

Considering patterns as sets of their instances, a difference operator over patterns computes a finite set of two given patterns, which represents the difference between the dividend pattern and the divisor pattern. A complement of a pattern is a pattern set, the ground constructor instances of which comprise the complement of the ground constructor instances of the former pattern. Given finitely many unconstrained linear patterns, using a difference operator over linear patterns, a complement algorithm returns a finite set of linear patterns as a complement of the given patterns. In this paper, we extend the difference operator and complement algorithm to constrained linear patterns used in logically constrained term rewrite systems (LCTRSs, for short) that have no user-defined constructor term with a sort for built-in values. Then, as for left-linear term rewrite systems, using the complement algorithm, we show that quasi-reducibility is decidable for such LCTRSs with decidable built-in theories. For the single use of the difference operator over constrained patterns, only divisor patterns are required to be linear.

DOI： https://doi.org/10.1007/978-3-032-04167-8_14

Open Access

その他リンク： https://doi.org/10.48550/arXiv.2507.04080

Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms 査読有り国際共著国際誌

Kanta Takahata, Jonas Schöpf, Naoki Nishida, and Takahito Aoto

Proceedings of the 35th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2025), Lectures Notes in Computer Science 16117 巻頁： 180 - 195 2025年9月

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

Logically constrained term rewriting is a rewriting framework that supports built-in data structures such as integers and bit vectors. Recently, constrained terms play a key role in various analyses and applications of logically constrained term rewriting. A fundamental question on constrained terms arising there is how to characterize equivalence between them. However, in the current literature only limited progress has been made on this. In this paper, we provide several sound and complete solutions to tackle this problem. Our key idea is the introduction of a novel concept, namely existentially constrained terms, into which the original form of constrained terms can be embedded. We present several syntactic characterizations of equivalence between existentially constrained terms. In particular, we provide two different kinds of complete characterizations: one is designed to facilitate equivalence checking, while the other is intended for theoretical analysis.

DOI： https://doi.org/10.1007/978-3-032-04848-6_12

その他リンク： https://doi.org/10.48550/arXiv.2505.21986

Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations 査読有り国際共著国際誌 Open Access

Kanta Takahata, Jonas Schöpf, Naoki Nishida, and Takahito Aoto

Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming (PPDP 2025) 頁： 1 - 13 2025年9月

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

Logically constrained term rewriting is a relatively new rewriting formalism that naturally supports built-in data structures, such as integers and bit vectors. In the analysis of logically constrained term rewrite systems (LCTRSs), rewriting constrained terms plays a crucial role. However, this combines rewrite rule applications and equivalence transformations in a closely intertwined way. This intertwining makes it difficult to establish useful theoretical properties for this kind of rewriting and causes problems in implementations—namely, that impractically large search spaces are often required. To address this issue, we propose in this paper a novel notion of most general constrained rewriting, which operates on existentially constrained terms, a concept recently introduced by the authors. We define a class of left-linear, left-value-free LCTRSs that are general enough to simulate all left-linear LCTRSs and exhibit the desired key property: most general constrained rewriting commutes with equivalence. This property ensures that equivalence transformations can be deferred until after the application of rewrite rules, which helps mitigate the issue of large search spaces in implementations. In addition to that, we show that the original rewriting formalism on constrained terms can be embedded into our new rewriting formalism on existentially constrained terms. Thus, our results are expected to have significant implications for achieving correct and efficient implementations in tools operating on LCTRSs.

DOI： https://doi.org/10.1145/3756907.3756916

その他リンク： https://doi.org/10.48550/arXiv.2507.09326

On Transforming Prioritized Multithreaded Programs into Logically Constrained Term Rewrite Systems 査読有り

Misaki Kojima and Naoki Nishida

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

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

A transformation of multithreaded programs without priorities into logically constrained term rewrite systems (LCTRS, for short) has been proposed. In this paper, we extend it to prioritized threads by introducing a descending list of priorities into terms representing configurations. As a case study, we show a verification example in which a runtime-error verification method based on all-path reachability detects an assertion failure caused by the interrupt of a high-priority thread.

On Merging Constrained Rewrite Rules of Induction Hypotheses in Constrained Rewriting Induction 査読有り

Naoki Nishida and Nozomi Taira

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

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

In proving constrained equations by rewriting induction (RI, for short), the Expand rule which is one of the main inference rules of RI makes an orientable constrained equation a constrained rewrite rule, called an IH rewrite rule, which can be used as an induction hypothesis. Such an IH rewrite rule may be applied to constrained equations in order to simplify them. The broader the scope of the application of IH rewrite rules, the greater the possibilities for proving constrained equations. In this paper, we modify the Expand rule of RI in order to make the scope of the application of the IH rewrite rule broader. To be more precise, in orienting a constrained equation as an IH rewrite rule, if there already exists an IH rewrite rule having the same left- and right-hand sides, then we disjunct the constraint of the orienting equation with the constraint of the existing IH rewrite rule; otherwise, the orienting equation is added to the set of IH rewrite rules as a new IH rewrite rule. We show that this modification does not lose the proof power of RI.

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月

Confluence Competition 2024 国際共著

Raul Gutierrez, Aart Middeldorp, Naoki Nishida, Teppai Saito, and Rene Thiemann

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

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

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

Open Access

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 査読有り国際誌 Open Access

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

Open Access

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

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹