Abstract
We consider the framework of regular tree model checking where sets of configurations of a system are represented by regular tree languages and its dynamics is modeled by a term rewriting system (or a regular tree transducer). We focus on the computation of the reachability set R* (L) where R is a regular tree transducer and L is a regular tree language. The construction of this set is not possible in general. Therefore, we present a general acceleration technique, called regular tree widening which allows to speed up the convergence of iterative fixpoint computations in regular tree model checking. This technique can be applied uniformly to various kinds of transformations.
We show the application of our framework to different analysis contexts: verification of parametrized tree networks and data-flow analysis of multithreaded programs. Parametrized networks are modeled by relabeling tree transducers, and multithreaded programs are modeled by term rewriting rules encoding transformations on control structures. We prove that our widening technique can emulate many existing algorithms for special classes of transformations and we show that it can deal with transformations beyond the scope of these algorithms.
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
Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. Partial-order reduction in symbolic state space exploration. In Computer Aided Verification, pages 340–351, 1997.
P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In CAV’98. LNCS 1427, 1998.
P. A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling global conditions in parametrized system verification. Lecture Notes in Com-puter Science, 1633:134–150, 1999.
A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model Checking. In CONCUR’ 97. LNCS 1243, 1997.
A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In CAV’00. LNCS, 2000.
A. Bouajjani, A. Muscholl, and T. Touili. Permutation Rewriting and Algorithmic Verification. In LICS’01. IEEE, 2001.
A. Bouajjani. Languages, Rewriting systems, and Verification of Infinte-State Systems. In ICALP’01. LNCS 2076, 2001. invited paper.
A. Bouajjani and T. Touili. Extrapolating tree transformations. Technical report, LIAFA, May 2002. http://verif.liafa.jussieu.fr/~touili.
P. Cousot and R. Cousot. Static Determination of Dynamic Properties of Recursive Procedures. In IFIP Conf. on Formal Description of Programming Concepts. North-Holland Pub., 1977.
H. Comon, V. Cortier, and J. Mitchell. Tree automata with one memory, set constraints and ping-pong protocols. In ICALP’2001. LNCS 2076, 2001.
H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata, 1997.
E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterised networks using abstraction and regular languages. Lecture Notes in Computer Science, 962:395–407, 1995.
Patrick Cousot and Nicholas Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL’78. ACM, 1978.
Dennis Dams, Yassine Lakhnech, and Martin Steffen”. Iterating transducers. In CAV’01. LNCS, 2001.
J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data-flow analysis. In FOSSACS’99, volume LNCS 1578, 1999.
Joost Engelfriet. Bottom-up and top-down tree transformations-a comparison. In Mathematical Systems Theory, volume 9(3), 1975.
Javier Esparza and Andreas Podelski. Efficient algorithms for pre * and post * on interprocedural parallel flow graphs. In Symposium on Principles of Programming Languages, pages 1–11, 2000.
L. Fribourg and H. Olsen. Reachability sets of parametrized rings as regular languages. In Infinity’97. volume 9 of Electronical Notes in Theoretical Computer Science. Elsevier Science, 1997.
J. Goubault-Larrecq. A method for automatic cryptographic protocol verification. In 15th IPDPS 2000 Workshops. LNCS 1800, 2000.
R. Gilleron and S. Tison. Regular tree languages and rewrite systems. In Fundamenta Informaticae, volume 24, pages 157–175, 1995.
B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In TACAS’00. LNCS, 2000.
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Proc. CAV’97, volume 1254 of LNCS, pages 424–435. Springer, 1997.
D. Lugiez and Ph. Schnoebelen. The regular viewpoint on PA-processes. In Proc. 9th Int. Conf. Concurrency Theory (CONCUR’98), Nice, France, Sep. 1998, volume 1466, pages 50–66. Springer, 1998.
R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Systems. Phd. thesis, TUM, 1998.
D. Monniaux. Abstracting cryptographic protocols with tree automata. Science of Computer Programming, 2002.
A. Pnueli and E. Shahar. Liveness and acceleration in parametrized verification. In CAV’00. LNCS, 2000.
T. Touili. Widening Techniques for Regular Model Checking. In Vepas Workshop. Volume 50 of Electronic Notes in TCS, 2001.
Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular stae spaces. In CAV’98. LNCS 1254, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouajjani, A., Touili, T. (2002). Extrapolating Tree Transformations. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_46
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive