Abstract
This work studies automata-based symbolic data structures for representing infinite sets. Such structures are used in particular by verification tools in order to represent the sets of configurations handled during symbolic exploration of infinite state spaces. Our goal is to develop an efficient projection operator for these representations. There are several needs for such an operator during state-space exploration; we focus here on projecting the set of reachable configurations obtained at the end of exploration. An interesting application is the state-space visualization problem, which consists in providing the user with a graphical picture of a relevant fragment of the reachable state space.
For theoretical reasons, the projection of automata-represented sets is inherently costly. The contribution of this paper is to introduce an improved automata-based data structure that makes it possible to reduce in several cases the effective cost of projection. The idea is twofold. First, our structure allows to apply projection to only a part of an automaton, in cases where a full computation is not necessary. Second, the structure is able to store the results of past projection operations, and to reuse them in order to speed up subsequent computations. We show how our structure can be applied to the state-space visualization problem, and discuss some experimental results.
This work is supported by the Interuniversity Attraction Poles program MoVES of the Belgian Federal Science Policy Office, and by the grant 2.4530.02 of the Belgian Fund for Scientific Research (F.R.S.-FNRS).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 1–12. Springer, Heidelberg (1996)
Bruyère, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and p-recognizable sets of integers. Bulletin of the Belgian Mathematical Society 1(2), 191–238 (1994)
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000)
Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Logic 6(3), 614–633 (2005)
Boigelot, B., Latour, L.: Counting the solutions of Presburger equations without enumerating them. Theoretical Computer Science 313, 17–29 (2004)
Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, University of Liége, Belgium (1998)
Boigelot, B., Wolper, P.: Representing arithmetic constraints with finite automata: An overview. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 1–19. Springer, Heidelberg (2002)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. International Congress on Logic, Methodoloy and Philosophy of Science, pp. 1–12. Stanford University Press, Stanford (1962)
Couvreur, J.-M.: A BDD-like implementation of an automata package. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds.) CIAA 2004. LNCS, vol. 3317, pp. 310–311. Springer, Heidelberg (2005)
Hopcroft, J.E.: An n logn algorithm for minimizing states in a finite automaton. Theory of Machines and Computation, 189–196 (1971)
Latour, L.: Presburger Arithmetic: From Automata to Formulas. PhD thesis, University of Liége, Belgium (2005)
Leroux, J.: A polynomial time Presburger criterion and synthesis for number decision diagrams. In: Proc. 20th LICS, pp. 147–156. IEEE Computer Society, Los Alamitos (2005)
Oppen, D.C.: A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences 16, 323–332 (1978)
Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du Premier Congrès des Mathématiciens des Pays Slaves, Warsaw, pp. 92–101 (1929)
Shiple, T.R., Kukula, J.H., Ranjan, R.K.: A comparison of presburger engines for EFSM reachability. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 280–292. Springer, Heidelberg (1998)
Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 21–32. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boigelot, B., Degbomont, JF. (2009). Partial Projection of Sets Represented by Finite Automata, with Application to State-Space Visualization. In: Dediu, A.H., Ionescu, A.M., Martín-Vide, C. (eds) Language and Automata Theory and Applications. LATA 2009. Lecture Notes in Computer Science, vol 5457. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00982-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-00982-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00981-5
Online ISBN: 978-3-642-00982-2
eBook Packages: Computer ScienceComputer Science (R0)