Publication details

<< back
 

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š and Mojmír KŘETÍNSKÝ. 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. p. 9-28, 20 pp. ISBN 978-3-540-69506-6.Export BibTeX
@inproceedings{710390,
author = {Brim, Luboš and Křetínský, Mojmír},
address = {Berlin},
booktitle = {33rd Conference on Current Trends in Theory and Practice of Computer Science},
keywords = {finite and infinite-state systems; reachability; linear time logic; model checking; decidability},
language = {eng},
location = {Berlin},
isbn = {978-3-540-69506-6},
pages = {9-28},
publisher = {Springer-Verlag},
title = {Model Checking Large Finite-State Systems and Beyond},
year = {2007}
}
Original language:English
Field:Informatics
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:

 
 
top