Model Checking Large Finite-State Systems and Beyond

• Authors: BRIM Luboš; KŘETÍNSKÝ Mojmír
• Year of publication: 2007
• Type: Article in Proceedings
• Conference: 33rd Conference on Current Trends in Theory and Practice of Computer Science
• MU Faculty or unit: Faculty of Informatics
• Field: Informatics
• Keywords: finite and infinite-state systems; reachability; linear time logic; model checking; decidability
• Description: We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS), possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based Linear Temporal Logic (LTL) a Hennessy-Milner branching time logic.

Related projects

• Techniques for automatic verification and validation of software nad hardware systems
• Institute for Theoretical Computer Science
• Highly Parallel and Distributed Computing Systems
• Automated software verification