On Decidability of LTL+Past Model Checking for Process Rewrite Systems

• Authors: KŘETÍNSKÝ Mojmír; ŘEHÁK Vojtěch; STREJČEK Jan
• Year of publication: 2009
• Type: Article in Proceedings
• Conference: Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008)
• MU Faculty or unit: Faculty of Informatics
• Web: http://dx.doi.org/10.1016/j.entcs.2009.05.033
• Field: Informatics
• Keywords: process rewrite systems; LTL; infinite-state; model-checking; decidability
• Description: The Decidability Borderline for Model Checking of LTL+Past and Weakly--Extended Process Rewrite Systems is determined.

Related projects

• Techniques for automatic verification and validation of software nad hardware systems
• Institute for Theoretical Computer Science
• Highly Parallel and Distributed Computing Systems
• Formal verification: algorithms, properties of modelling formalisms amd temporal logics
• New possibilities in automatic verification of network protocols
• Verification and Analysis of Large-Scale Computer Systems