A New Unfolding Approach to LTL Model Checking

Reference:

Javier Esparza and Keijo Heljanko. A new unfolding approach to LTL model checking. In Ugo Montanari, José D. P. Rolim, and Emo Welzl, editors, Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP'2000), volume 1853 of Lecture Notes in Computer Science, pages 475–486, Geneva, Switzerland, July 2000. Springer-Verlag.

Abstract:

A new unfolding approach to LTL model checking is presented, in which the model checking problem can be solved by direct inspection of a certain finite prefix. The techniques presented so far required to run an elaborate algorithm on the prefix.

Keywords:

net unfoldings, model checking, tableau systems, LTL, Petri nets

Suggested BibTeX entry:

@inproceedings{ultl,
    address = {Geneva, Switzerland},
    author = {Javier Esparza and Keijo Heljanko},
    booktitle = {Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP'2000)},
    editor = {Ugo Montanari and Jos{\'e} D. P. Rolim and Emo Welzl},
    month = {July},
    pages = {475--486},
    publisher = {Springer-Verlag},
    series = {Lecture Notes in Computer Science},
    title = {A New Unfolding Approach to {LTL} Model Checking},
    volume = {1853},
    year = {2000},
}