Senescent ground tree rewrite systems

DOI10.1145/2603088.2603112MaRDI QIDQ4635633zbMATH OpenOpenAlexFDO

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)

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

zbMATH Keywords

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

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)

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.

Recommendations

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)