Coping With Strong Fairness
| Autor: | Keijo Heljanko, Timo Latvala |
|---|---|
| Rok vydání: | 2000 |
| Předmět: |
Model checking
Coping (psychology) Algebra and Number Theory Theoretical computer science Efficient algorithm Petri net Theoretical Computer Science Automaton TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics Linear temporal logic Computer Science::Logic in Computer Science Computer Science::Formal Languages and Automata Theory Information Systems Counterexample Mathematics |
| Zdroj: | Keijo Heljanko Scopus-Elsevier University of Helsinki |
| ISSN: | 0169-2968 |
| DOI: | 10.3233/fi-2000-43123409 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|