Senescent ground tree rewrite systems

DOI10.1145/2603088.2603112zbMATH Open1401.68135arXiv1311.4915OpenAlexW2157976170MaRDI QIDQ4635633FDOQ4635633

Publication date: 23 April 2018

Published in: 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) (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1311.4915

Recommendations

zbMATH Keywords

reachability automata concurrency Petri nets pushdown systems under-approximation reset Petri nets Ackermann-hard bounded-context switches ground term rewrite systems ground tree rewrite systems scope-bounding

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Grammars and rewriting systems (68Q42) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (4)

This page was built for publication: Senescent ground tree rewrite systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635633)