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

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

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
Citation
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