Constructing Automata from Temporal Logic Formulas: A Tutorial

Wolper, Pierre

doi:10.1007/3-540-44667-2_7

Download

Paper published in a journal (Scientific congresses and symposiums)

Constructing Automata from Temporal Logic Formulas: A Tutorial

Wolper, Pierre

2001 • In Lecture Notes in Computer Science, 2090, p. 261-277

Permalink
https://hdl.handle.net/2268/18956

DOI
10.1007/3-540-44667-2_7

Files (2)Send to Details Statistics Bibliography Similar publications

Files

Full Text

Wol00-fmpa.pdf

Author postprint (337.98 kB)

Download

Full Text Parts

Wol00-fmpa.pdf

Publisher postprint (603.93 kB)

Request a copy

The original publication is available at www.springerlink.com

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

temporal logic; Buchi automata; model checking

Abstract :

[en] This paper presents a tutorial introduction to the construction of finite-automata on infinite words from linear-time temporal logic formulas. After defining the source and target formalisms, it describes a first construction whose correctness is quite direct to establish, but whose behavior is always equal to the worst-case upper bound. It then turns to the techniques that can be used to improve this algorithm in order to obtain the quite effective algorithms that are now in use.

Disciplines :

Computer science

Author, co-author :

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 :

Constructing Automata from Temporal Logic Formulas: A Tutorial

Publication date :

2001

Event name :

FORMAL METHODS AND PERFORMANCE ANALYSIS The first Euro Summerschool on Trends in Computer Science

Event place :

Nijmegen, Netherlands

Event date :

July 3-7, 2000

By request :

Yes

Audience :

International

Journal title :

Lecture Notes in Computer Science

ISSN :

0302-9743

eISSN :

1611-3349

Publisher :

Springer, Berlin, Germany

Special issue title :

Lectures on Formal Methods and Performance Analysis

Volume :

2090

Pages :

261-277

Available on ORBi :

since 18 August 2009

Statistics

Number of views

121 (12 by ULiège)

Number of downloads

2741 (6 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

106

Bibliography

J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, pages 1-12, Stanford, 1962. Stanford University Press.
Orna Bernholtz, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. In Computer Aided Verification, Proc. 6th Int. Workshop, volume 818 of Lecture Notes in Computer Science, pages 142-155, Stanford, California, June 1994. Springer-Verlag.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, January 1986.
M. Daniele, F. Giunchiglia, and M. Y. Vardi. Improved automata generation for linear temporal logic. In Computer-Aided Verification, Proc. 11th Int. Conference, volume 1633, pages 249-260, July 1999.
E.A. Emerson and E.M. Clarke. Using branching time logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241-266, 1982.
Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-thefly automatic verification of linear temporal logic. In Proc. 15th Work. Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.
G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991.
Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279-295, May 1997. Special Issue: Formal Methods in Software Practice.
O. Kupferman and M. Vardi. Weak alternating automata are not that weak. In Proc. 5th Israeli Symposium on Theory of Computing and Systems, pages 147-158. IEEE Computer Society Press, 1997.
Zohar Manna and Pierre Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems, 6(1):68-93, January 1984.
J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th Int’l Symp. on Programming, volume 137, pages 337-351. Springer-Verlag, Lecture Notes in Computer Science, 1981.
S. Safra. On the complexity of omega-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988.
F. Somenzi and R. Bloem. Efficient b¨uchi automata from ltl formulae. In Computer-Aided Verification, Proc. 12th Int. Conference, volume 1633, pages 247-263, 2000.
A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for B¨uchi automata with applications to temporal logic. Theoretical Computer Science, 49:217-237, 1987.
Wolfgang Thomas. Automata on infinite objects. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science - Volume B: Formal Models and Semantics, chapter 4, pages 133-191. Elsevier, Amsterdam, 1990.
Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322-331, Cambridge, June 1986.
Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, November 1994.
Pierre Wolper, Moshe Y. Vardi, and A. Prasad Sistla. Reasoning about infinite computation paths. In Proc. 24th IEEE Symposium on Foundations of Computer Science, pages 185-194, Tucson, 1983.