A note on on-the-fly verification algorithms

Schwoon, Stefan; Esparza, Javier

A note on on-the-fly verification algorithms

dc.contributor.author	Schwoon, Stefan	de
dc.contributor.author	Esparza, Javier	de
dc.date.accessioned	2005-04-07	de
dc.date.accessioned	2016-03-31T07:58:30Z
dc.date.available	2005-04-07	de
dc.date.available	2016-03-31T07:58:30Z
dc.date.issued	2004	de
dc.date.updated	2013-07-05	de
dc.description.abstract	The automata-theoretic approach to verification of LTL relies on an algorithm for finding accepting cycles in the product of the system and a Büchi automaton for the negation of the formula. Explicit-state model checkers typically construct the product space "on the fly" and explore the states using depth-first search. We survey algorithms proposed for this purpose and propose two improved algorithms, one based on nested DFS, the other on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.	en
dc.identifier.other	117300632	de
dc.identifier.uri	http://nbn-resolving.de/urn:nbn:de:bsz:93-opus-22281	de
dc.identifier.uri	http://elib.uni-stuttgart.de/handle/11682/2561
dc.identifier.uri	http://dx.doi.org/10.18419/opus-2544
dc.language.iso	en	de
dc.relation.ispartofseries	Technischer Bericht / Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik;2004,6	de
dc.rights	info:eu-repo/semantics/openAccess	de
dc.subject.classification	Model checking , Tiefensuche	de
dc.subject.ddc	004	de
dc.subject.other	LTL	de
dc.subject.other	depth-first search	en
dc.title	A note on on-the-fly verification algorithms	en
dc.type	workingPaper	de
ubs.fakultaet	Fakultät Informatik, Elektrotechnik und Informationstechnik	de
ubs.institut	Institut für Formale Methoden der Informatik	de
ubs.opusid	2228	de
ubs.publikation.typ	Arbeitspapier	de
ubs.schriftenreihe.name	Technischer Bericht / Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik	de

Files

Original bundle

Now showing 1 - 1 of 1

Name:: TR_2004_06.pdf
Size:: 179.47 KB
Format:: Adobe Portable Document Format

Download

Collections

05 Fakultät Informatik, Elektrotechnik und Informationstechnik