A note on on-the-fly verification algorithms

Stefan Schwoon; Javier Esparza

doi:10.1007/978-3-540-31980-1_12

A note on on-the-fly verification algorithms

Stefan Schwoon, Javier Esparza

Universität Stuttgart

Publikation: Beitrag in Fachzeitschrift › Konferenzartikel › Begutachtung

92 Zitate (Scopus)

Abstract

The automata-theoretic approach to LTL verification relies on an algorithm for finding accepting cycles in a Büchi automaton. Explicit-state model checkers typically construct the automaton "on the fly" and explore its states using depth-first search. We survey algorithms proposed for this purpose and identify two good algorithms, a new algorithm based on nested DPS, and another based on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.

Originalsprache	Englisch
Seiten (von - bis)	174-190
Seitenumfang	17
Fachzeitschrift	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Jahrgang	3440
DOIs	https://doi.org/10.1007/978-3-540-31980-1_12
Publikationsstatus	Veröffentlicht - 2005
Extern publiziert	Ja
Veranstaltung	11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, Großbritannien/Vereinigtes Königreich Dauer: 4 Apr. 2005 → 8 Apr. 2005

Zugriff auf Dokument

10.1007/978-3-540-31980-1_12

Andere Dateien und Links

Verknüpfung zur Publikation in Scopus

Dieses zitieren

@article{4bcf6f4d51234446b049c5826a688d79,

title = "A note on on-the-fly verification algorithms",

abstract = "The automata-theoretic approach to LTL verification relies on an algorithm for finding accepting cycles in a B{\"u}chi automaton. Explicit-state model checkers typically construct the automaton {"}on the fly{"} and explore its states using depth-first search. We survey algorithms proposed for this purpose and identify two good algorithms, a new algorithm based on nested DPS, and another based on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.",

author = "Stefan Schwoon and Javier Esparza",

year = "2005",

doi = "10.1007/978-3-540-31980-1_12",

language = "English",

volume = "3440",

pages = "174--190",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

note = "11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 ; Conference date: 04-04-2005 Through 08-04-2005",

}

TY - JOUR

T1 - A note on on-the-fly verification algorithms

AU - Schwoon, Stefan

AU - Esparza, Javier

PY - 2005

Y1 - 2005

N2 - The automata-theoretic approach to LTL verification relies on an algorithm for finding accepting cycles in a Büchi automaton. Explicit-state model checkers typically construct the automaton "on the fly" and explore its states using depth-first search. We survey algorithms proposed for this purpose and identify two good algorithms, a new algorithm based on nested DPS, and another based on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.

AB - The automata-theoretic approach to LTL verification relies on an algorithm for finding accepting cycles in a Büchi automaton. Explicit-state model checkers typically construct the automaton "on the fly" and explore its states using depth-first search. We survey algorithms proposed for this purpose and identify two good algorithms, a new algorithm based on nested DPS, and another based on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.

UR - http://www.scopus.com/inward/record.url?scp=24644509013&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-31980-1_12

DO - 10.1007/978-3-540-31980-1_12

M3 - Conference article

AN - SCOPUS:24644509013

SN - 0302-9743

VL - 3440

SP - 174

EP - 190

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005

Y2 - 4 April 2005 through 8 April 2005

ER -

A note on on-the-fly verification algorithms

Abstract

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Dieses zitieren