TCS / Research / Publications / On Stubborn Sets in the Verification of Linear Time Temporal Properties
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

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. Formal Methods in System Design, 26(1):45–67, January 2005. 2005 Springer Science + Business Media, Inc. (Norwell, MA, USA; Dordrecht, The Netherlands; Berlin, Germany).

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 article is concentrated on the verification of nexttime-less LTL (linear time temporal logic) formulas with the aid of the stubborn set method. The essential contribution is a theorem that gives us a way to utilize the structure of the checked formula when the stubborn set method is used and there is no fairness assumption. The theorem also applies to verification under fairness assumptions, including those which allow a predefined subset of actions to be treated unfairly.

Keywords:

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

Suggested BibTeX entry:

@article{VarpaaniemiKimmo-VrpFMSD,
    author = {Kimmo Varpaaniemi},
    journal = {Formal Methods in System Design},
    month = {January},
    note = { 2005 Springer Science + Business Media, Inc. (Norwell, MA, USA; Dordrecht, The Netherlands; Berlin, Germany)},
    number = {1},
    pages = {45--67},
    title = {{O}n Stubborn Sets in the Verification of Linear Time Temporal Properties},
    volume = {26},
    year = {2005},
}

See www.springerlink.com ...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.