×
Finkel, A.; Schnoebelen, P.

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

Theor. Comput. Sci. 256, No. 1-2, 63-92 (2001).
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.

Cited in 1 Review
Cited in 152 Documents

MSC:

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

Keywords:

infinite systems; verification; well-quasi-ordering
PDF BibTeX XML Cite
\textit{A. Finkel} and \textit{P. Schnoebelen}, Theor. Comput. Sci. 256, No. 1--2, 63--92 (2001; Zbl 0973.68170)
Full Text: DOI

References:

[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
[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
[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
[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
[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
[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
[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
[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
[61] Jančar, P., A note onn well quasi-orderings for powersets, Information Processing Letters, 72, 155-161 (1999) · Zbl 0998.06002
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.