Model Checking Large Finite-State Systems and Beyond
| Authors | |
|---|---|
| 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 | |
| Citation | |
| 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: |