Senescent Ground Tree Rewrite Systems

被引：0

作者：

Hague, M. ^{[1
]}

机构：

[1] Royal Holloway Univ London, Egham, Surrey, England

来源：

PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) | 2014年

基金：

英国工程与自然科学研究理事会;

关键词：

Ground tree rewrite systems; ground term rewrite systems; automata; concurrency; scope-bounding; bounded-context switches; under-approximation; reachability; petri-nets; reset petri-nets; Ackermann-hard; pushdown systems; MODEL CHECKING; LTL;

D O I：

10.1145/2603088.2603112

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Ground Tree Rewrite Systems with State are known to have an undecidable control state reachability problem. Taking inspiration from the recent introduction of scope-bounded multi-stack pushdown systems, we define Senescent Ground Tree Rewrite Systems. These are a restriction of ground tree rewrite systems with state such that nodes of the tree may no longer be rewritten after having witnessed an a priori fixed number of control state changes. As well as generalising scope-bounded multi-stack pushdown systems, we show - via reductions to and from reset Petri-nets - that these systems have an Ackermann-complete control state reachability problem. However, reachability of a regular set of trees remains undecidable.

引用

页数：10

共 50 条

[21] BOTTOM-UP TREE PUSHDOWN-AUTOMATA AND REWRITE SYSTEMS
COQUIDE, JL
DAUCHET, M
GILLERON, R
VAGVOLGYI, S
LECTURE NOTES IN COMPUTER SCIENCE, 1991, 488 : 287 - 298
[22] REWRITE ORDERINGS AND TERMINATION OF REWRITE SYSTEMS
LESCANNE, P
LECTURE NOTES IN COMPUTER SCIENCE, 1991, 520 : 17 - 27
[23] DECIDING CONFLUENCE AND NORMAL FORM PROPERTIES OF GROUND TERM REWRITE SYSTEMS EFFICIENTLY
Felgenhauer, Bertram
LOGICAL METHODS IN COMPUTER SCIENCE, 2018, 14 (04) : 1 - 35
[24] A total, ground path ordering for proving termination of AC-rewrite systems
Kapur, D
Sivakumar, G
REWRITING TECHNIQUES AND APPLICATIONS, 1997, 1232 : 142 - 156
[25] Process rewrite systems
Mayr, R
INFORMATION AND COMPUTATION, 2000, 156 (1-2) : 264 - 286
[26] BOTTOM-UP TREE PUSHDOWN-AUTOMATA - CLASSIFICATION AND CONNECTION WITH REWRITE SYSTEMS
COQUIDE, JL
DAUCHET, M
GILLERON, R
VAGVOLGYI, S
THEORETICAL COMPUTER SCIENCE, 1994, 127 (01) : 69 - 98
[27] PRIORITY REWRITE SYSTEMS
BAETEN, JCM
BERGSTRA, JA
KLOP, JW
JOURNAL OF SYMBOLIC LOGIC, 1986, 51 (02) : 482 - 482
[28] Synchronized Tree Languages for Reachability in Non-right-linear Term Rewrite Systems
Boichut, Yohan
Pelletier, Vivien
Rety, Pierre
REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2016, 2016, 9942 : 64 - 81
[29] COMPUTING WITH REWRITE SYSTEMS
DERSHOWITZ, N
INFORMATION AND CONTROL, 1985, 65 (2-3): : 122 - 157
[30] Verification of Rewrite Rules for Computation Tree Logics
McCabe-Dansted, John C.
Reynolds, Mark
2014 21ST INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING (TIME 2014), 2014, : 142 - 151

← 1 2 3 4 5 →