Abstract
Formal methods based on symbolic representations have been found to be very effective. In the case of infinite state systems, there has been a great deal of interest in accelerations - a technique for characterizing the result of iterating an execution sequence an arbitrary number of times, in a sound, but not necessarily complete, way. We propose the use of abstractions as a general framework to design accelerations. We investigate SemiLinear Regular Expressions (SLREs) as symbolic representations for FIFO automata. In particular, we show that SLREs are easy to manipulate (inclusion between two SLREs is in NP∩coNP), they form the core of known FIFO symbolic representations (SLREs = QDDs∩CQDDs), and they are usually sufficient since for FIFO automata with one channel, an arbitrary iteration of a loop is LRE representable.
Supported in part by FORMA, a project funded by DGA, CNRS and MENSER.
Supported in part by ARO under grant DAAG55-98-1-03093.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
P. Abdulla, A. Annichini, and A. Bouajjani. Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol. Lecture Notes in Computer Science, 1579:208–222, 1999.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.
B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In Proc. 4th Int. Symp. Static Analysis, Paris, France, September 1997, volume 1302, pages 172–186. Springer-Verlag, 1997.
A. Bouajjani and P. Habermehl. Symbolic reachability analysis of FIFO channel systems with nonregular sets of configurations. In Proc. 24th Int. Coll. Automata, Languages, and Programming (ICALP’97), Bologna, Italy, July 1997, volume 1256 of Lecture Notes in Computer Science, pages 560–570. Springer-Verlag, 1997.
Janusz A. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11(4):481–494, October 1964.
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323–342, April 1983.
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual Symposium on Principles of Programming Languages, pages 238–252. ACM SIGACT and SIGPLAN, ACM Press, 1977.
G. Cécé. Vérification, analyse et approximations symboliques des automates communicants. Thèse ENS de Cachan, January 1998.
H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. In Proc. 10th Int. Conf. Computer Aided Verification (CAV’98), Vancouver, BC, Canada, June–July 1998, volume 1427 of Lecture Notes in Computer Science, pages 268–279. Springer, 1998.
A. Finkel, S. P. Iyer, and G. Sutre. Well-abstracted transition systems: application to fifo automata. Research Report LSV-2000-6, Lab. Specification and Verification, ENS de Cachan, Cachan, France, June 2000.
A. Finkel and O. Marcé. A minimal symbolic coverability graph for infinite-state comunicating automata. Technical report, LIFAC, 1996.
A. Finkel and G. Sutre. Decidability of reachability problems for classes of two counters automata. In Proc. 17th Ann. Symp. Theoretical Aspects of Computer Science (STACS’2000), Lille, France, Feb. 2000, volume 1770 of Lecture Notes in Computer Science, pages 346–357. Springer, 2000.
Thierry Jéron and Claude Jard. Testing for unboundedness of fifo channels. Theoretical Computer Science, 113(1):93–117, 1993.
J. K. Pachl. Protocol description and analysis based on a state transition model with channel expressions. In Proc. of Protocol Specification, Testing and Verification, VII, 1987.
Wuxu Peng and S. Purushothaman. Data flow analysis of communicating finite state machines. ACM Transactions on Programming Languages and Systems, 13(3):399–442, July 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Finkel, A., Iyer, P., Sutre, G. (2000). Well-Abstracted Transition Systems. In: Palamidessi, C. (eds) CONCUR 2000 — Concurrency Theory. CONCUR 2000. Lecture Notes in Computer Science, vol 1877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44618-4_40
Download citation
DOI: https://doi.org/10.1007/3-540-44618-4_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67897-7
Online ISBN: 978-3-540-44618-7
eBook Packages: Springer Book Archive