On the construction of automata from linear arithmetic constraints

Wolper, Pierre; Boigelot, Bernard

doi:10.1007/3-540-46419-0_1

Request a copy

Paper published in a journal (Scientific congresses and symposiums)

On the construction of automata from linear arithmetic constraints

Wolper, Pierre; Boigelot, Bernard

2000 • In Lecture Notes in Computer Science, 1785, p. 1-19

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

DOI
10.1007/3-540-46419-0_1

Files (2)Send to Details Statistics Bibliography Similar publications

Files

Full Text

BW-TACAS2000.pdf

Publisher postprint (275.69 kB)

Request a copy

Full Text Parts

BW-TACAS2000.pdf

Author postprint (225.22 kB)

Download

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 :

linear constraints; automata

Abstract :

[en] This paper presents an overview of algorithms for constructing automata from linear arithmetic constraints. It identifies one case in which the special structure of the automata that are constructed allows a linear-time determinization procedure to be used. Furthermore, it shows through theoretical analysis and experiments that the special structure of the constructed automata does, in quite a general way, render the usual upper bounds on automata operations vastly overpessimistic.

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)

Boigelot, Bernard ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique

Language :

English

Title :

On the construction of automata from linear arithmetic constraints

Publication date :

March 2000

Event name :

Tools and Algorithms for the Construction and Analysis of Systems 6th International Conference, TACAS 2000

Event place :

Berlin, Germany

Event date :

March 25 – April 2, 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 :

Tools and Algorithms for the Construction and Analysis of Systems

Volume :

1785

Pages :

1-19

Available on ORBi :

since 01 December 2009

Statistics

Number of views

96 (13 by ULiège)

Number of downloads

188 (9 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

Bibliography

B. Boigelot, L. Bronne, and S. Rassart. An improved reachability analysis method for strongly linear hybrid systems. In Proc. 9th Int. Conf. on Computer Aided Verification, Volume 1254 of Lecture Notes in Computer Science, pages 167-178, Haifa, June 1997. Springer-Verlag. (Pubitemid 127088974)
A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In Proceedings of CAAP'96, number 1059 in Lecture Notes in Computer Science, pages 30-43. Springer-Verlag, 1996. (Pubitemid 126064261)
V. Bruyère, G. Hansel, C. Michaux, and R. Villemaire. Logic and p-recognizable sets of integers. Bulletin of the Belgian Mathematical Society, 1(2):191-238, March 1994.
B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Université de Liège, 1998.
Bernard Boigelot, Stéphane Rassart, and Pierre Wolper. On the expressiveness of real and integer arithmetic automata. In Proc. 25th Colloq. on Automata, Programming, and Languages (ICALP), Volume 1443 of Lecture Notes in Computer Science, pages 152-163. Springer-Verlag, July 1998. (Pubitemid 128111111)
R.E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293-318, 1992.
J. R. Büchi. Weak second-order arithmetic and finite automata. Zeitschrift Math. Logik und Grundlagen der Mathematik, 6:66-92, 1960.
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 automatatheoretic 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.
Bernard Boigelot and Pierre Wolper. Symbolic verification with periodic sets. In Computer Aided Verification, Proc. 6th Int. Conference, Volume 818 of Lecture Notes in Computer Science, pages 55-67, Stanford, California, June 1994. Springer-Verlag.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, January 1986. (Pubitemid 16633197)
A. Cobham. On the base-dependence of sets of numbers recognizable by finite automata. Mathematical Systems Theory, 3:186-192, 1969.
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. (Pubitemid 14566074)
H. B. Enderton. A mathematical introduction to logic. Academic Press, 1972.
Rob Gerth, Doron Peled, Moshe Y. Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. 15th Work. Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.
Jesper G. Henriksen, Jakob L. Jensen, Michael E. Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. Mona: Monadic secondorder logic in practice. In Ed Brinksma, Rance Cleaveland, Kim Guldstrand Larsen, Tiziana Margaria, and Bernhard Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems, Volume 1019 of Lecture Notes in Computer Science, pages 89-110. Springer-Verlag, 1995. (Pubitemid 126004023)
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. (Pubitemid 127828295)
The Liège Automata-based Symbolic Handler (LASH). Available at http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.
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.
W. Pugh. A practical algorithm for exact array dependency analysis. Comm. of the ACM, 35(8):102, August 1992.
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.
A. L. Semenov. Presburgerness of predicates regular in two number systems. Siberian Mathematical Journal, 18:289-299, 1977.
R. K. Ranjan T. R. Shiple, J. H. Kukula. A comparison of Presburger engines for EFSM reachability. In Proc. 10th Int. Conf. on Computer Aided Verification, Volume 1427 of Lecture Notes in Computer Science, pages 280-292, Vancouver, July 1998. Springer-Verlag. (Pubitemid 128092346)
Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposi um 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 and Bernard Boigelot. An automata-theoretic approach to Presburger arithmetic constraints. In Proc. Static Analysis Symposium, Volume 983 of Lecture Notes in Computer Science, pages 21-32, Glasgow, September 1995. Springer-Verlag.
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.