Well-structured transition systems everywhere! (English) Zbl 0973.68170

Summary: Well-Structured Transition Systems (WSTSs) are a general class of infinite-state systems for which decidability results rely on the existence of a well-quasi-ordering between states that is compatible with the transitions. In this article, we provide an extensive treatment of the WSTS idea and show several new results. Our improved definitions allow many examples of classical systems to be seen as instances of WSTSs.


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI


[1] P.A. Abdulla, K. C̆erāns, B. Jonsson, T. Yih-Kuen, General decidability theorems for infinite-state systems, Proc. 11th IEEE Symp. Logic in Computer Science (LICS’96), New Brunswick, NJ, USA, July 1996, pp. 313-321.
[2] P.A. Abdulla, K. C̆erāns, B. Jonsson, T. Yih-Kuen, Algorithmic analysis of programs with well quasi-ordered domains, Inform. and Comput., to appear. · Zbl 1046.68567
[3] P.A. Abdulla, B. Jonsson, Verifying programs with unreliable channels, Proc. 8th IEEE Symp. Logic in Computer Science (LICS’93), Montreal, Canada, June 1993, pp. 160-170. · Zbl 0856.68096
[4] Abdulla, P.A.; Jonsson, B., Undecidability of verifying programs with unreliable channels, (), 316-327 · Zbl 1418.68123
[5] Abdulla, P.A.; Jonsson, B., Ensuring completeness of symbolic verification methods for infinite-state systems, Theor. comput. sci., 256, this Vol., 145-167, (2001) · Zbl 0973.68146
[6] Abdulla, P.A.; Jonsson, B., Verifying networks of timed processes, (), 298-312
[7] Alur, R.; Dill, D.L., A theory of timed automata, Theoret. comput. sci., 126, 183-235, (1994) · Zbl 0803.68071
[8] Araki, T.; Kasami, T., Some decision problems related to the reachability problem for Petri nets, Theoret. comput. sci., 3, 1, 85-104, (1977) · Zbl 0352.68083
[9] Arnold, A.; Latteux, M., Récursivité et cônes rationnels fermés par intersection, Calcolo, XV(IV), 381-394, (1978) · Zbl 0421.68075
[10] Autebert, J.-M.; Berstel, J.; Boasson, M., Context-free languages and pushdown automata, (), 111-174, (Chapter 3)
[11] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.A., Decidability of bisimulation equivalence for processes generating context-free languages, (), 94-111 · Zbl 0635.68014
[12] von Bochmann, G., Finite state description of communication protocols, Comput. networks ISDN systems, 2, 361-372, (1978)
[13] Bouajjani, A.; Mayr, R., Model checking lossy vector addition systems, (), 323-333 · Zbl 0926.03035
[14] Brand, D.; Zafiropulo, P., On communicating finite-state machines, J. ACM, 30, 2, 323-342, (1983) · Zbl 0512.68039
[15] Browne, M.C.; Clarke, E.M.; Grumberg, O., Characterizing finite Kripke structures in propositional temporal logic, Theoret. comput. sci., 59, 1-2, 115-131, (1988) · Zbl 0677.03011
[16] Burch, J.R.; Clarke, E.M.; McMillan, K.L.; Dill, D.L.; Hwang, L.J., Symbolic model checking: 10^{20} states and beyond, Inform. and comput., 98, 2, 142-170, (1992) · Zbl 0753.68066
[17] G. Gécé, Etat de l’art des techniques d’analyse des automates finis communicants, Rapport de DEA, Université de Paris-Sud, Orsay, France, September 1993.
[18] Gécé, G.; Finkel, A., Programs with quasi-stable channels are effectively recognizable, (), 304-315
[19] Cécé, G.; Finkel, A.; Purushothaman Iyer, S., Unreliable channels are easier to verify than perfect channels, Inform. and comput., 124, 1, 20-31, (1995) · Zbl 0844.68035
[20] K.C̆erāns, Deciding properties of integral automata, in: Proc. 21st Internat. Coll. Automata, Languages, and Programming (ICALP’94), Jerusalem, Israel, July 1994, Lecture Notes in Computer Science, vol. 820, Springer, Berlin, 35-46
[21] Christensen, S.; Hirshfeld, Y.; Moller, F., Decidable subsets of CCS, Comput. J., 37, 4, 233-242, (1994)
[22] Ciardo, G., Petri nets with marking-dependent arc cardinalityproperties and analysis, (), 179-198
[23] Courcelle, B., Graph rewritingan algebraic and logic approach, (), 193-242 · Zbl 0900.68282
[24] Dickson, L.E., Finiteness of the odd perfect and primitive abundant numbers with r distinct prime factors, Amer. J. math., 35, 413-422, (1913) · JFM 44.0220.02
[25] Dufourd, D.; Finkel, A., Ph. schnoebelen. reset nets between decidability and undecidability, (), 103-115 · Zbl 0909.68124
[26] J. Esparza, More infinite results, in: Proc. 1st Internat. Workshop on Verification of Infinite State Systems (INFINITY ’96), Pisa, Italy, August 30-31, 1996, Electronic Notes in Theoretical Computer Science, vol. 5, Elsevier, Amsterdam, 1997. · Zbl 1049.68093
[27] A. Finkel, About monogeneous fifo Petri nets, Proc. 3rd Eur. Workshop on Applications and Theory of Petri Nets, Varenna, Italy, September (1982) 175-192.
[28] A. Finkel, Structuration des Systèmes de Transitions, Applications au Contrôle du Parallélisme par Files FIFO, Thèse de Docteur d’Etat, Université de Paris-Sud, Orsay, France, June 1986.
[29] Finkel, A., A generalization of the procedure of karp and Miller to well structured transition systems, (), 499-508
[30] A. Finkel, Well structured transition systems, Research Report 365, Lab. de Recherche en Informatique (LRI), Univ. Paris-Sud, Orsay, August 1987.
[31] A. Finkel, A new class of analyzable CFSMs with unbounded FIFO channels, Prelim in: Proc. 8th IFIP WG 6.1 Internat. Symp. Protocol Specification, Testing and Verification, Atlantic City, New Jersey, USA, June 1988.
[32] Finkel, A., Reduction and covering of infinite reachability trees, Inform. and comput., 89, 2, 144-179, (1990) · Zbl 0753.68073
[33] Finkel, A., Decidability of the termination problem for completely specified protocols, Distributed comput., 7, 129-135, (1994)
[34] Finkel, A.; Choquet, A., FIFO nets without order deadlock, Acta inform., 25, 1, 15-36, (1987) · Zbl 0614.68050
[35] A. Finkel, P. McKenzie, C. Picaronny, A well-structured framework for analysing Petri nets extensions, Research Report LSV-99-2, Lab. Specification and Verification, ENS de Cachan, Cachan, France, February 1999.
[36] R.J. van Glabbeek, W.P. Weijland, Branching time and abstraction in process algebra, in: G. X. Ritter (Ed.), Information Processing 89, North-Holland, Amsterdam, August 1989, 613-618.
[37] M.G. Gouda, L.E. Rosier, Synchronizable networks of communicating finite state machines, unpublished manuscript, 1985. · Zbl 0563.68021
[38] Heinemann, B., Subclasses of self-modifying nets, (), 187-192
[39] Henzinger, T.A., Hybrid automata with finite bisimulations, (), 324-335 · Zbl 1412.68130
[40] Higman, G., Ordering by divisibility in abstract algebras, Proc. London math. soc. (3), 2, 7, 326-336, (1952) · Zbl 0047.03402
[41] Jonsson, B.; Parrow, J., Deciding bisimulation equivalences for a class on non-finite-state programs, Inform. and comput., 107, 2, 272-302, (1993) · Zbl 0799.68133
[42] Karp, R.M.; Miller, R.E., Parallel program schemata, J. comput. system sci., 3, 2, 147-195, (1969) · Zbl 0198.32603
[43] O. Kouchnarenko, Ph. Schnoebelen, A model for recursive-parallel programs, in: Proc. 1st Internat. Workshop on Verification of Infinite State Systems (INFINITY’96), Pisa, Italy, August 1996, Electronic Notes in Theoretical Computer Science, vol. 5, Elsevier, Amsterdam, 1997. · Zbl 0912.68131
[44] Kruskal, J.B., The theory of well-quasi-ordering: a frequently discovered concept, J. combin. theory ser. A, 13, 3, 297-305, (1972) · Zbl 0244.06002
[45] Kushnarenko, O.; Schnoebelen, Ph., A formal framework for the analysis of recursive-parallel programs, (), 45-59
[46] Mäkinen, E., On permutative grammars generating context-free languages, Bit, 25, 604-610, (1985) · Zbl 0582.68045
[47] R. Mayr, Lossy counter machines, Technical Report TUM-19830, Institut für Informatik, TUM, Munich, Germany, October 1998.
[48] Memmi, G.; Finkel, A., An introduction to FIFO nets-monogeneous nets: a subclass of FIFO nets, Theoret. comput. sci., 35, 2-3, 191-214, (1985) · Zbl 0566.68054
[49] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[50] Moller, F., Infinite results, (), 195-216
[51] Peterson, J.L., Petri net theory and the modeling of systems, (1981), Prentice-Hall Englewood Cliffs, NJ
[52] Reisig, W., Petri nets. an introduction, EATCS monographs on theoretical computer science, vol. 4, (1985), Springer Berlin
[53] Revesz, P.Z., A closed form for Datalog queries with integer order, (), 187-201 · Zbl 0789.68042
[54] Valk, R., Self-modifying nets, a natural extension of Petri nets, (), 464-476
[55] P.A. Abdulla, A. Nylén, Better is better than well: On efficient verification of infinite-state systems, in: Proc. 15th IEEE Symp. Logic in Computer Science (LICS’2000), Santa Barbara, CA, USA, June 2000.
[56] P.A. Abdulla, A. Nylén, BQOs and Timed Petri Nets, Available at \( ̃\), March 2000.
[57] M. Bozzano, G. Delzanno, M. Martelli, A bottom-up semantics for LO, in: Proc. 2nd Int. Conf. Principles and Practice of Declarative Programming (PPDP’2000), Montreal, Canada, Sep. 2000, to appear. · Zbl 0987.68857
[58] G. Delzanno, J.-F. Raskin, Symbolic representation of upward-closed sets, in: Proc. 6th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’2000), Berlin, Germany, Mar.-Apr. 2000, vol. 1785 of Lecture Notes in Computer Science, Springer, 2000, pp. 426-440. · Zbl 0961.68096
[59] E.A. Emerson, K.S. Namjoshi, Verification of a parameterized bus arbitration protocol, in: Proc. 10th Int. Conf. Computer Aided Verification (CAV’98), Vancouver, BC, Canada, June-July 1998, vol. 1427 of Lecture Notes in Computer Science, Springer, 1998, pp. 452-463.
[60] T.A. Henzinger, R. Majumdar, A classification of symbolic transition systems. In Proc. 17th Ann. Symp. Theoretical Aspects of Computer Science (STACS’2000), Lille, France, Feb. 2000, vol. 1770 of Lecture Notes in Computer Science, Springer, 2000, pp. 13-34. · Zbl 0959.68093
[61] Jančar, P., A note onn well quasi-orderings for powersets, Information processing letters, 72, 155-161, (1999) · Zbl 0998.06002
[62] M. Leuschel, H. Lehmann, Coverability of Reset Petri nets and other well-structured transition systems by partial deduction, in: Proc. 14th Int. Workshop Computer Science Logic (CSL’2000), Fischbachau, Germany, Aug. 2000, Lecture Notes in Computer Science, Springer, 2000, to appear. · Zbl 0983.68135
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.