Abstract
The model checking of a counters system S often reduces to the effective computation of the set of predecessors \({\rm Pre}_S^*(X)\) of a set of integer vectors X. Because the exact computation of this set is not possible in general, we are interested in characterizing the minimal Number Decision Diagrams (NDD) [WB00] that represents the set Pre ≤ k(X). In particular, its size is proved to be just polynomially bounded in k when S is a counters system with a finite monoïd [FL02], explaining why there is no exponential blow up in k.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-thefly analysis of systems with unbounded, lossy FIFO channels. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 305–318. Springer, Heidelberg (1998)
Annichini, A., Bouajjani, A., Sighireanu, M.: TREX: A tool for reachability analysis of complex systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 368–372. Springer, Heidelberg (2001)
Alv homepage.: http://www.cs.ucsb.edu/~bultan/composite/
Babylon homepage: http://www.ulb.ac.be/di/ssd/lvbegin/CST/-index.html
Bartziz, C., Bultan, T.: Efficient image computation in infinite state model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 249–261. Springer, Heidelberg (2003)
Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 30–43. Springer, Heidelberg (1996)
Bouajjani, A., Esparza, J., Finkel, A., Maler, O., Rossmanith, P., Willems, B., Wolper, P.: An efficient automata approach to some problems on context-free grammars. Information Processing Letters 74(5–6), 221–227 (2000)
Bodeveix, J.-P., Filali, M.: FMona: a tool for expressing validation techniques over infinite state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 204–219. Springer, Heidelberg (2000)
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast acceleration of symbolic transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118–121. Springer, Heidelberg (2003)
Bultan, T., Gerber, R., Pugh, W.: Symbolic modelchecking of infinite state systems using Presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 400–411. Springer, Heidelberg (1997)
Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems 21(4), 747–789 (1999)
Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theoretical Computer Science 221(1–2), 211–250 (1999)
Bruyère, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. 1(2), 191–238 (1994)
Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 223–235. Springer, Heidelberg (2003)
Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theoretical Computer Science 309(2), 413–468 (2003)
Brain homepage, http://www.cs.man.ac.uk/voronkov/BRAIN/index.html
Bryant, R.E.: Symbolic boolean manipulation with ordered binarydecision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)
Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 53–68. Springer, Heidelberg (2000)
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)
Dufourd, C., Jančar, P., Schnoebelen, P.: Boundedness of Reset P/T nets. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 301–310. Springer, Heidelberg (1999)
Delzanno, G., Raskin, J.-F., Van Begin, L.: Attacking symbolic state explosion. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 298–310. Springer, Heidelberg (2001)
Allen Emerson, E., Namjoshi, K.S.: On model checking for nondeterministic infinite-state systems. In: Proc. 13th IEEE Symp. Logic in Computer Science (LICS 1998), Indianapolis, IN, USA, June 1998, pp. 70–80. IEEE Comp. Soc. Press, Los Alamitos (1998)
Fast homepage, http://www.lsv.ens-cachan.fr/fast/
Finkel, A., Leroux, J.: How to compose Presburgeraccelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)
Finkel, A., Leroux, J.: Polynomial time image computation with interval-definable counters system. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 182–197. Springer, Heidelberg (2004)
Fribourg, L., Olsén, H.: Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 213–227. Springer, Heidelberg (1997)
Finkel, A., Iyer, S.P., Sutre, G.: Well-abstracted transition systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 566–580. Springer, Heidelberg (2000)
Finkel, A., Schnoebelen, P.: Well structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)
Ginsburg, S., Spanier, E.H.: Semigroups, Presburger formulas and languages. Pacific J. Math. 16(2), 285–296 (1966)
Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. Int. J. of Foundations Computer Science 13(4), 571–586 (2002)
Lash homepage, http://www.montefiore.ulg.ac.be/~boigelot/research/lash/
Leroux, J.: Algorithmique de la vérification des systèmes à compteurs. Approximation et accélération. Implémentation de l’outil Fast. PhD thesis, Ecole Normale Supérieure de Cachan, Laboratoire Spécification et Vérification. CNRS UMR 8643, décembre (2003)
Mona homepage, http://www.brics.dk/mona/index.html
Mandel, A., Simon, I.: On finite semigroups of matrices. Theoretical Computer Science 5(2), 101–111 (1977)
Reutenauer, C.: Aspects Mathématiques des Réseaux de Petri, chapter 3. Collection Etudes et Recherches en Informatique. Masson, Paris (1989)
TReX homepage, http://www.liafa.jussieu.fr/~sighirea/trex/
Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 1–19. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Finkel, A., Leroux, J. (2004). Image Computation in Infinite State Model Checking. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27813-9_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-27813-9_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22342-9
Online ISBN: 978-3-540-27813-9
eBook Packages: Springer Book Archive