M. Hague
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 push-down 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.
- P. A. Abdulla, B. Jonsson, P. Mahata, and J. d'Orso. Regular tree model checking. In CAV, 2002. Google Scholar
Digital Library
- A. Annichini, A. Bouajjani, and M. Sighireanu. Trex: A tool for reachability analysis of complex systems. In CAV, 2001. Google ScholarDigital Library
- T. Araki and T. Kasami. Some Decision Problems Related to the Reachability Problem for Petri Nets. TCS, 3(1), 1977.Google Scholar
- M. F. Atig, B. Bollig, and P. Habermehl. Emptiness of multi-pushdown automata is 2etime-complete. In DLT, 2008. Google ScholarDigital Library
- M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. LMCS, 7(4), 2011.Google Scholar
- T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking with slam. Commun. ACM, 54(7), 2011. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN, 2000. Google ScholarDigital Library
- S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. Fast: acceleration from theory to practice. STTT, 10(5), 2008. Google ScholarDigital Library
- A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, 1997. Google ScholarDigital Library
- L. Bozzelli, M. Kretínský, V. Rehák, and J. Strejcek. On decidability of ltl model checking for process rewrite systems. Acta Inf., 46(1), 2009. Google ScholarDigital Library
- W. S. Brainerd. Tree generating regular systems. Information and Control, 14(2), 1969.Google Scholar
- L. Breveglieri, A. Cherubini, C. Citrini, and S. Crespi-Reghizzi. Multi-push-down languages and grammars. Int. J. Found. Comput. Sci., 7(3), 1996.Google ScholarCross Ref
- A. Cyriac, P. Gastin, and K. N. Kumar. MSO decidability of multi-pushdown systems via split-width. In CONCUR, 2012. Google ScholarDigital Library
- M. Dauchet, T. Heuillard, P. Lescanne, and S. Tison. Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems. Inf. Comput., 88(2), 1990. Google ScholarDigital Library
- M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In LICS, 1990.Google ScholarCross Ref
- J. Esparza, A. Kucera, and S. Schwoon. Model checking ltl with regular valuations for pushdown systems. Inf. Comput., 186(2), 2003. Google ScholarDigital Library
- A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In INFINITY, 1997.Google Scholar
- S. Ginsburg and E. H. Spanier. Semigroups, presburger formulas, and languages. Pacific Journal of Mathematics, 16, 1966.Google Scholar
- S. Göller and A. W. Lin. Refining the process rewrite systems hierarchy via ground tree rewrite systems. In CONCUR, 2011.Google ScholarCross Ref
- C. Haase. Subclasses or presburger arithmetic and the weak exponential-time hierarchy. Under submission.Google Scholar
- Matthew Hague. Senescent ground tree rewrite systems, 2013. arXiv:1311.4915 {cs.FL}.Google Scholar
- N. D. Jones and S. S. Muchnick. Even simple programs are hard to analyze. J. ACM, 24(2), 1977. Google ScholarDigital Library
- R. M. Karp and R. E. Miller. Parallel program schemata: A mathematical model for parallel computation. In SWAT (FOCS), 1967. Google ScholarDigital Library
- S. La Torre and M. Napoli. Reachability of multistack pushdown systems with scope-bounded matching relations. In CONCUR, 2011. Google ScholarDigital Library
- S. La Torre and M. Napoli. A temporal logic for multi-threaded programs. In IFIP TCS, 2012. Google ScholarDigital Library
- S. La Torre and G. Parlato. Scope-bounded multistack pushdown systems: Fixed-point, sequentialization, and tree-width. In FSTTCS, 2012.Google Scholar
- A. W. Lin. Weakly-synchronized ground tree rewriting - (with applications to verifying multithreaded programs). In MFCS, 2012. Google ScholarDigital Library
- C. Löding. Infinite Graphs Generated by Tree Rewriting. PhD thesis, RWTH Aachen, 2003.Google Scholar
- P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL, 2011. Google ScholarDigital Library
- M. Maidl. The common fragment of ctl and ltl. In FOCS, 2000. Google ScholarDigital Library
- R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, TU-München, 1998.Google Scholar
- K. McAloon. Petri nets and large finite sets. Theoretical Computer Science, 32, 1984.Google Scholar
- R. Piskac. Decision Procedures for Program Synthesis and Verification. PhD thesis, Laboratoire d'Analyse et de Raisonnement Authomatisés, École Polytechnique Fédérale de Lausanne, 2011.Google Scholar
- L. Pottier. Minimal solutions of linear diophantine systems: Bounds and algorithms. In RTA, 1991. Google ScholarDigital Library
- S. Qadeer. The case for context-bounded verification of concurrent programs. In SPIN, 2008. Google ScholarDigital Library
- R. Büchi. Regular canonical systems. Archiv fur Math. Logik und Grundlagenforschung 6, 1964.Google Scholar
- T. W. Reps, S. Schwoon, S. Jha, and D. Melski. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program., 58(1-2), 2005. Google ScholarDigital Library
- S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, 2005. Google ScholarDigital Library
- Sylvain Schmitz. Complexity hierarchies beyond elementary, 2013. arXiv:1312.5686 {cs.CC}.Google Scholar
- P. Schnoebelen. Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett., 83(5), 2002. Google ScholarDigital Library
- P. Schnoebelen. Revisiting ackermann-hardness for lossy counter machines and reset petri nets. In MFCS, 2010. Google ScholarDigital Library
- S. Schwoon. Model-checking Pushdown Systems. PhD thesis, Technical University of Munich, 2002.Google Scholar
- A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD thesis, LFCS, School of Informatics, University of Edinburgh, 2010.Google Scholar
- S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In LICS, 2007. Google ScholarDigital Library
Index Terms
- Senescent ground tree rewrite systems
Recommendations
The Complexity of Verifying Ground Tree Rewrite Systems
LICS '11: Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer ScienceGround tree rewrite systems (GTRS) are an extension of pushdown systems with the ability to spawn new sub threads that are hierarchically structured. In this paper, we study the following problems over GTRS:(1) model checking EF-logic, (2)weak bi ...
On ground tree transformations and congruences induced by tree automata
For a tree automaton A over a ranked alphabet , we study the ground tree transformation (A) induced by A and the restriction (A) of the congruence A to terms over . We define a congruence relation A A on A, called the determiner of A, and the quotient ...
Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems
In his seminal paper, Mayr introduced the well-known process rewrite systems (PRS) hierarchy, which contains many well-studied classes of infinite-state systems including pushdown systems (PDS), Petri nets, and PA-processes. A separate development in ...
Comments