Abstract
Finite state automata with counters are useful for modelling systems with discrete parameters. The calculation of state invariants is an important tool in the analysis of such systems. Previous authors have presented techniques for the calculation of state invariants based on their approximation by convex polyhedra or periodic sets.
In this paper we present a new method for the calculation of invariants for finite state automata with counters, based on their representation by gap-order constraints. This method differs from previous approaches by exploiting existing techniques for the calculation of least fixed points. The use of least fixed points reduces the need for approximation and allows the generation of non-convex invariants. We do not need to specify the initial inputs to the automaton, but can leave them as uninstantiated parameters, or partially specify them using gap-order constraints. Our method not only provides a new tool for program analysis, but is also an interesting application of logic programming techniques.
This work was performed while the second author was a visiting research fellow at the Ecole Normale Supérieure, funded by EC HCM grants Compulog ERBCHBGCT 930365 and Logic Program Synthesis and Transformation CHRX.CT.93 0414.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proceedings of 5th IEEE LICS, pages 414–425. IEEE, 1990.
B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proceedings of conference on Computer-Aided Verification, 1994, pages 55–67, 1994.
L. Fribourg and H. Olsén. Datalog programs with arithmetical constraints: hierarchic, periodic and spiralling least fixed points. Research report 95-26, Laboratoire Informatique, École Normale Supérieure, Paris, November 1995.
L. Fribourg and J. D. C. Richardson. Symbolic verification with gap-order constraints. Report LIENS — 96 — 3, Laboratoire d'Informatique, École Normale Supérieure (LIENS), Paris, February 1996. Available by ftp from host ftp.ens.fr in directory /pub/reports/liens.
L. Fribourg and M. Veloso Peixoto. Bottom-up evaluation of Datalog programs with arithmetic constraints. In Alan Bundy, editor, 12th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 814, pages 311–325, Nancy, France, 1994. Springer-Verlag.
N. Halbwachs. Delay analysis in synchronous programs. In Proceedings of conference on Computer-Aided Verification, 1993, pages 333–346, 1993.
T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proceedings 7th LICS Symposium, Santa Cruz, pages 394–406, 1992.
A. Kerbrat. Méthodes Symboliques pour la Vérification des Processus Communicants: étude et mise en oeuvre. PhD thesis, L'Université Joseph Fourier — Grenoble I, November 1994. In French.
A. Kerbrat. Reachable state space analysis of LOTOS specifications. In Proceedings of the 7th international conference on formal description techniques, pages 161–176, 1994.
P. Z. Revesz. A closed-form evaluation for Datalog queries with integer (gap)-order constraints. Theoretical Computer Science, 1993. vol. 116, pages 117–149.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fribourg, L., Richardson, J. (1997). Symbolic verification with gap-order constraints. In: Gallagher, J. (eds) Logic Program Synthesis and Transformation. LOPSTR 1996. Lecture Notes in Computer Science, vol 1207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62718-9_2
Download citation
DOI: https://doi.org/10.1007/3-540-62718-9_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62718-0
Online ISBN: 978-3-540-68494-7
eBook Packages: Springer Book Archive