WEKO3
アイテム
A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations
https://ipsj.ixsq.nii.ac.jp/records/233815
https://ipsj.ixsq.nii.ac.jp/records/23381544851332-c385-4d68-b136-6e14aca4ad30
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO1702002.pdf (478.9 kB)
2026年4月22日からダウンロード可能です。
|
Copyright (c) 2024 by the Information Processing Society of Japan
|
|
| 非会員：¥0, IPSJ:学会員：¥0, PRO:会員：¥0, DLIB:会員：¥0 | ||
| Item type | Trans(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2024-04-22 | |||||||||
| タイトル | ||||||||||
| タイトル | A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations | |||||||||
| 言語 | ||||||||||
| 言語 | eng | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | [通常論文] constrained rewriting, constrained narrowing, quasi-termination, all-path reachability | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||
| 資源タイプ | journal article | |||||||||
| 著者所属 | ||||||||||
| Graduate School of Informatics, Nagoya University | ||||||||||
| 著者所属 | ||||||||||
| Graduate School of Informatics, Nagoya University | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Graduate School of Informatics, Nagoya University | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Graduate School of Informatics, Nagoya University | ||||||||||
| 著者名 |
Misaki, Kojima
× Misaki, Kojima
× Naoki, Nishida
|
|||||||||
| 著者名(英) |
Misaki, Kojima
× Misaki, Kojima
× Naoki, Nishida
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | 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. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.32(2024) (online) ------------------------------ |
|||||||||
| 論文抄録(英) | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | 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. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.32(2024) (online) ------------------------------ |
|||||||||
| 書誌レコードID | ||||||||||
| 収録物識別子タイプ | NCID | |||||||||
| 収録物識別子 | AA11464814 | |||||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 17, 号 2, 発行日 2024-04-22 |
|||||||||
| ISSN | ||||||||||
| 収録物識別子タイプ | ISSN | |||||||||
| 収録物識別子 | 1882-7802 | |||||||||
| 出版者 | ||||||||||
| 言語 | ja | |||||||||
| 出版者 | 情報処理学会 | |||||||||
