Abstract
We compute reachability sets of counter automata. Even if the reachability set is not necessarily recursive, we use symbolic representation and acceleration to increase convergence. For functions defined by translations over a polyhedral domain, we give a new acceleration algorithm which is polynomial in the size of the function and exponential in its dimension, while the more generic algorithm is exponential in both the size of the function and its dimension. This algorithm has been implemented in the tool Fast. We apply it to a complex industrial protocol, the TTP membership algorithm. This protocol has been widely studied. For the first time, the protocol is automatically proved to be correct for 1 fault and N stations, and using abstraction we prove the correctness for 2 faults and N stations also.
Chapter PDF
Similar content being viewed by others
References
Annichini, A., Asarin, E., Bouajjani, A.: Symbolic techniques for parametric reasoning about counter and clock systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 419–434. Springer, Heidelberg (2000)
alv homepage, http://www.cs.ucsb.edu/~bultan/composite/
Bartzis, C., Bultan, T.: Efficient symbolic representations for arithmetic constraints in verification. Technical Report ucsb cs:TR-2002-16, University of California, Santa Barbara, Computer Science (2002)
Bartzis, 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)
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)
Bouajjani, A., Merceron, A.: Parametric verification of a group membership algorithm. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 311–330. Springer, Heidelberg (2002)
Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Université de Liège (1998)
Boigelot, B., Wolper, P.: Symbolic verification with periodic sets, vol. 2725, pp. 55–67 (1994)
Delzanno, G.: Home Page – Giorgio Delzanno, http://www.disi.unige.it/person/DelzannoG/
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)
Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proc. 14th IEEE Symp. Logic in Computer Science (LICS 1999), Trento, Italy, July 1999, pp. 352–359. IEEE Comp. Soc. Press, Los Alamitos (1999)
Fast homepage, http://www.lsv.ens-cachan.fr/fast/
Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 145–156. Springer, Heidelberg (2002)
Kopetz, H., Grünsteidl, G.: A time trigerred protocol for fault-tolerant real-time systems. In: IEEE computer, Volume January, pp. 14–23 (1994)
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, École Normale Supérieure de Cachan (December 12, 2003)
Leroux, J.: The affine hull of a binary automaton is computable in polynomial time (2003)
The MONA project, http://www.brics.dk/mona/
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
Bardin, S., Finkel, A., Leroux, J. (2004). FASTer Acceleration of Counter Automata in Practice. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_42
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive