Paper published in a book (Scientific congresses and symposiums)
Simple On-the-fly Automatic Verification of Linear Temporal Logic
Gerth, Rob; Peled, Doron; Vardi, Moshe Y et al.
1995In Dembinski, Piotr; Sredniawa, Marek (Eds.) Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification
Peer reviewed
 

Files


Full Text
GPVW95-pstv.pdf
Author postprint (140.67 kB)
Download

All documents in ORBi are protected by a user license.

Send to



Details



Keywords :
Model Checking; linear temporal logic; Büchi automata; automatic verification
Abstract :
[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.
Disciplines :
Computer science
Author, co-author :
Gerth, Rob;  Technical University of Eindhoven
Peled, Doron;  AT&T Bell Laboratories
Vardi, Moshe Y;  Rice University > Department of Computer Science
Wolper, Pierre  ;  Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)
Language :
English
Title :
Simple On-the-fly Automatic Verification of Linear Temporal Logic
Publication date :
1995
Event name :
International Symposium on Protocol Specification, Testing and Verification
Event organizer :
IFIP WG6.1
Event place :
Warsaw, Poland
Event date :
June 1995
Audience :
International
Main work title :
Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification
Editor :
Dembinski, Piotr
Sredniawa, Marek
Publisher :
IFIP
ISBN/EAN :
0-412-71620-8
Peer reviewed :
Peer reviewed
Available on ORBi :
since 15 April 2012

Statistics


Number of views
820 (2 by ULiège)
Number of downloads
1756 (5 by ULiège)

Bibliography


Similar publications



Contact ORBi