TCS / Research / Publications / Coping with Strong Fairness
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Coping with Strong Fairness

Reference:

Timo Latvala and Keijo Heljanko. Coping with strong fairness. Fundamenta Informaticae, 43(1–4):175–193, 2000.

Abstract:

We consider the verification of linear temporal logic (LTL) properties of Petri nets, where the transitions can have both weak and strong fairness constraints. Allowing the transitions to have weak or strong fairness constraints simplifies the modeling of systems in many cases. We use the automata theoretic approach to model checking. To cope with the strong fairness constraints efficiently we employ Streett automata where appropriate. We present memory efficient algorithms for both the emptiness checking and counterexample generation problems for Streett automata.

Keywords:

verification, model checking, fairness, Streett automata, counterexamples

Suggested BibTeX entry:

@article{LatHel:Fundamenta2000,
    author = {Timo Latvala and Keijo Heljanko},
    journal = {Fundamenta Informaticae},
    number = {1--4},
    pages = {175--193},
    publisher = {IOS Press},
    title = {Coping with Strong Fairness},
    volume = {43},
    year = {2000},
}

See www.tcs.hut.fi ...

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