Abstract
Regular languages have proved useful for the symbolic state exploration of infinite state systems. They can be used to represent infinite sets of system configurations; the transitional semantics of the system consequently can be modeled by finite-state transducers. A standard problem encountered when doing symbolic state exploration for infinite state systems is how to explore all states in a finite amount of time.When representing the one-step transition relation of a system by a finite-state transducer T, this problem boils down to finding an appropriate finite-state representation T ** for its transitive closure.
In this paper we give a partial algorithm to compute a finite-state transducer T ** for a general class of transducers. The construction builds a quotient of an underlying infinite-state transducer T w, using a novel behavioural equivalence that is based past and future bisimulations computed on finite approximations of T w. The extrapolation to T w of these finite bisimulations capitalizes on the structure of the states of T w, which are strings of states of T. We show how this extrapolation may be rephrased as a problem of detecting confluence properties of rewrite systems that represent the bisimulations. Thus, we can draw upon techniques that have been developed in the area of rewriting.
A prototype implementation has been successfully applied to various examples.
Chapter PDF
References
P. A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded lossy Fifo-channels. In Hu and Vardi [12], pages 305–318.
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In Emerson and Sistla [7], pages 135–145.
E. M. Clarke and R. P. Kurshan, editors. Computer Aided Verification 1990, volume 531 of Lecture Notes in Computer Science. Springer-Verlag, 1991.
D. Dams, Y. Lakhnech, and M. Steffen. Iterating transducers. Technical Report TR-ST-01-03, Lehrstuhl für Software-Technologie, Institut für Informatik und praktische Mathematik, Christian-Albrechts-Universität Kiel, Jan. 2001. A preliminary version is available on-line at http://radon.ics.ele.tue.nl/~vires/public/results.htm (reports section).
P. Deussen, editor. Fifth GI Conference on Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science. Springer-Verlag, 1981.
E. A. Emerson and A. P. Sistla, editors. CAV’ 00, Proceedings of the 12th International Conference on Computer-Aided Verification, Chicago IL, volume 1855 of Lecture Notes in Computer Science. Springer-Verlag, 2000.
J. Fernandez. An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13:219–236, 1989.
S. Graf and M. Schwartzbach, editors. Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), volume 1785 of Lecture Notes in Computer Science. Springer-Verlag, 2000.
S. Graf and B. Steffen. Compositional minimization of finite state systems. In Clarke and Kurshan [4].
O. Grumberg, editor. CAV’ 97, Proceedings of the 9th International Conference on Computer-Aided Verification, Haifa. Israel, volume 1254 of Lecture Notes in Computer Science. Springer, June 1997.
A. J. Hu and M. Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, 10th International Conference, Vancouver, BC, Canada, Proceedings, volume 1427 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
B. Jonsson and M. Nilsson. Transitive closures for regular relations for verifying infinite-state systems. In Graf and Schwartzbach [9].
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In Grumberg [11].
D. E. Knuth and P. B. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
R. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dams, D., Lakhnech, Y., Steffen, M. (2001). Iterating Transducers. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_27
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive