On Stubborn Sets in the Verification of Linear Time Temporal Properties

Reference:

Kimmo Varpaaniemi. On stubborn sets in the verification of linear time temporal properties. In Jörg Desel and Manuel Silva, editors, Application and Theory of Petri Nets 1998: 19th International Conference, ICATPN'98, Lisbon, Portugal, June 22–26, 1998, Proceedings, volume 1420 of Lecture Notes in Computer Science, pages 124–143. Springer-Verlag, Berlin, Germany, 1998. © Springer-Verlag Berlin Heidelberg 1998.

Abstract:

The stubborn set method is one of the methods that try to relieve the state space explosion problem that occurs in state space generation. This paper is concentrated on the verification of nexttime-less LTL (linear time temporal logic) formulas with the aid of the stubborn set method. The contribution of the paper is a theorem that gives us a way to utilize the structure of the formula when the stubborn set method is used and there is no fairness assumption. Connections to already known results are drawn by modifying the theorem to concern verification under fairness assumptions.

Keywords:

reachability analysis, reduced state space generation, stubborn sets, verification of LTL formulas

Suggested BibTeX entry:

@inproceedings{VarpaaniemiKimmo-Vrp98b,
    author = {Kimmo Varpaaniemi},
    booktitle = {{A}pplication and Theory of {P}etri Nets 1998: 19th International Conference, {I}{C}{A}{T}{P}{N}'98, {L}isbon, {P}ortugal, {J}une 22--26, 1998, Proceedings},
    editor = {J{\"{o}}rg Desel and Manuel Silva},
    note = {© Springer-Verlag Berlin Heidelberg 1998},
    pages = {124--143},
    publisher = {Springer-Verlag, Berlin, Germany},
    series = {Lecture Notes in Computer Science},
    title = {{O}n Stubborn Sets in the Verification of Linear Time Temporal Properties},
    volume = {1420},
    year = {1998},
}