×

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.

MSC:

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

References:

[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.; 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.; 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.; 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, (Proc. 21st Internat. Coll. Automata, Languages, and Programming (ICALP’94) Jerusalem, Israel, July 1994, Lecture Notes in Computer Science, vol. 820 (1994), Springer: Springer Berlin), 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, (Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), Lisbon, Portugal, March 1998, Lecture Notes in Computer Science, vol. 1384 (1998), Springer: Springer Berlin), 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, (Rozenberg, G.; Salomaa, A., Handbook of Formal Languages, vol. 1 (1997), Springer: Springer Berlin), 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, (Proc. Parallel Architectures and Languages Europe (PARLE’87), Eindhoven, NL, June 1987, vol. II, Parallel Languages, Lecture Notes in Computer Science, vol. 259 (1987), Springer: Springer Berlin), 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, (Proc. 16th Ann. Symp. Theoretical Aspects of Computer Science (STACS’99), Trier, Germany, March 1999, Lecture Notes in Computer Science, vol. 1563 (1999), Springer: Springer Berlin), 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.; 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, (Proc. 9th Internat. Conf. Computer Aided Verification (CAV’97), Haifa, Israel, June 1997, Lecture Notes in Computer Science, 1254 (1997), Springer: Springer Berlin), 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; 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, (Proc. 15th Internat. Conf. Applications and Theory of Petri Nets, Zaragoza, Spain, June 1994, Lecture Notes in Computer Science, vol. 815 (1994), Springer: Springer Berlin), 179-198
[23] Courcelle, B., Graph rewritingan algebraic and logic approach, (van Leeuwen, J., Handbook of Theoretical Computer Science, vol. B (1990), Elsevier: Elsevier Amsterdam), 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, (Proc. 25th Internat. Coll. Automata, Languages, and Programming (ICALP ’98), Aalborg, Denmark, July 1998, Lecture Notes in Computer Science, vol. 1443 (1998), Springer: Springer Berlin), 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.; 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.; 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.; 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, (Proc. 14th Internat. Coll. Automata, Languages, and Programming (ICALP’87), Karlsruhe, FRG, July 1987, Lecture Notes in Computer Science, vol. 267 (1987), Springer: Springer Berlin), 499-508
[30] A. Finkel, Well structured transition systems, Research Report 365, Lab. de Recherche en Informatique (LRI), Univ. Paris-Sud, Orsay, August 1987.; 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.; 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.; 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.; 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.; 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, (Applications and Theory of Petri Nets (Selected Papers from the First and Second European Workshop, Strasbourg, France, September 1980, Bad Honnef, Germany, September 1981) (1982), Springer: Springer Berlin), 187-192
[39] Henzinger, T. A., Hybrid automata with finite bisimulations, (Proc. 22nd Internat. Coll. Automata, Languages, and Programming (ICALP’95), Szeged, Hungary, July 1995, Lecture Notes in Computer Science, vol. 944 (1995), Springer: Springer Berlin), 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.; 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, (Proc. 4th Internat. Conf. Parallel Computing Technologies (PaCT’97), Yaroslavl, Russia, September 1997, Lecture Notes in Computer Science, vol. 1277 (1997), Springer: Springer Berlin), 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.; 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: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[50] Moller, F., Infinite results, (Proc. 7th Internat. Conf. Concurrency Theory (CONCUR’96), Pisa, Italy, August 1996, Lecture Notes in Computer Science, vol. 1119 (1996), Springer: Springer Berlin), 195-216 · Zbl 1514.68176
[51] Peterson, J. L., Petri Net Theory and the Modeling of Systems (1981), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ
[52] Reisig, W., Petri Nets. An Introduction, EATCS Monographs on Theoretical Computer Science, vol. 4 (1985), Springer: Springer Berlin · Zbl 0555.68033
[53] Revesz, P. Z., A closed form for Datalog queries with integer order, (Proc. 3rd Internat. Conf. Database Theory (ICDT’90), Paris, France, December 1990, Lecture Notes in Computer Science, vol. 470 (1990), Springer: Springer Berlin), 187-201 · Zbl 0789.68042
[54] Valk, R., Self-modifying nets, a natural extension of Petri nets, (Proc. 5th Internat. Coll. Automata, Languages, and Programming (ICALP’78), Udine, Italy, July 1978, Lecture Notes in Computer Science, vol. 62 (1978), Springer: Springer Berlin), 464-476 · Zbl 0415.68025
[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.; 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 \(̃\); P.A. Abdulla, A. Nylén, BQOs and Timed Petri Nets, Available at \(̃\)
[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.; 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.; 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.; 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.; 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.; 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.