ORBi: Gerth Rob - Simple On-the-fly Automatic Verification of Linear Temporal Logic

Reference : Simple On-the-fly Automatic Verification of Linear Temporal Logic


	Document type :	Scientific congresses and symposiums : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/2268/116644

Title :	Simple On-the-fly Automatic Verification of Linear Temporal Logic
Language :	English
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 - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données) >]
Publication date :	1995
Main document title :	Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification
Editor :	Dembinski, Piotr
	Sredniawa, Marek
Publisher :	IFIP
Audience :	International
ISBN :	0-412-71620-8
Event name :	International Symposium on Protocol Specification, Testing and Verification
Event date :	June 1995
Event organizer :	IFIP WG6.1
Event place (city) :	Warsaw
Event country :	Poland
Keywords :	[en] 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.
Target :	Researchers
Permalink :	http://hdl.handle.net/2268/116644

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	GPVW95-pstv.pdf		Author postprint	137.37 kB	View/Open

All documents in ORBi are protected by a user license.

Dspace v1.5