Publication details
Model Checking Large Finite
-State Systems and Beyond
| Basic information | |
|---|---|
| Original title: | Model Checking Large Finite-State Systems and Beyond |
| Authors: | Luboš Brim, Mojmír Křetínský |
| Further information | |
|---|---|
| Citation: | BRIM, Luboš - KŘETÍNSKÝ, Mojmír. Model Checking Large Finite-State Systems and Beyond. In 33rd Conference on Current Trends in Theory and Practice of Computer Science. Berlin : Springer-Verlag, 2007. ISBN 978-3-540-69506-6, pp. 9-28. 2007, Harrachov. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | finite and infinite-state systems; reachability; linear time logic; model checking; decidability |
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
