Reference : Simple On-the-fly Automatic Verification of Linear Temporal Logic
Scientific congresses and symposiums : Paper published in a book
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/116644
Simple On-the-fly Automatic Verification of Linear Temporal Logic
English
Gerth, Rob [Technical University of Eindhoven > > > > > >]
Peled, Doron [AT&T Bell Laboratories > > > > > >]
Vardi, Moshe Y [Rice University > Department of Computer Science > > >]
Wolper, Pierre mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données) >]
1995
Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification
Dembinski, Piotr
Sredniawa, Marek
IFIP
Yes
International
0-412-71620-8
International Symposium on Protocol Specification, Testing and Verification
June 1995
IFIP WG6.1
Warsaw
Poland
[en] Model Checking ; linear temporal logic ; Büchi automata ; automatic verification
[en] We present a tableau-based algorithm for obtaining an automaton from a temporal logic formula. The algorithm is geared towards being used in model checking in an “on-the-fly” fashion, that is the automaton can be constructed simultaneously with, and guided by, the generation of the model. In particular, it is possible to detect that a property does not hold by only constructing part of the model and of the automaton. The algorithm can also be used to check the validity of a temporal logic assertion. Although the general problem is PSPACE-complete, experiments show that our algorithm performs quite well on the temporal formulas typically encountered in verification. While basing linear-time temporal logic model-checking upon a transformation to
automata is not new, the details of how to do this efficiently, and in “on-the-fly” fashion have never been given.
Researchers
http://hdl.handle.net/2268/116644

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
GPVW95-pstv.pdfAuthor postprint137.37 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.