×

zbMATH — the first resource for mathematics

Reduction and covering of infinite reachability trees. (English) Zbl 0753.68073
The aim of this paper is to generalize the main decidability results concerning Petri nets to the framework of structured transition systems. The author defines the class of structured transition systems and its subclass of strictly structured transition systems, and then proves that the Finite Reachability Tree Problem (FRTP) is decidable for structured transition systems and that the Finite Reachability Set Problem (FRSP) is decidable for strictly structured transition systems. It is conjectured that the FRSP is undecidable for structured transition systems.
The author then considers the decidability of the Coverability Problem (CP). The following notions are defined: coverability set of a structured transition system, strictly structured labelled transition systems, generalized Karp and Miller tree, well structured labelled transition systems. The main result of this section is that the CP is decidable for well structured labelled transition systems.
Finally, the structured transition systems having a structured set of terminal states are considered. The two main results are: the FRTP for structured transition systems having a structured set of terminal states is decidable and so is the FRSP for strictly structured transition systems having a structured set of terminal states. Known results and open problems (most with a conjecture) are well summarized in a table.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B25 Decidability of theories and sets of sentences
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Birkhoff, G., (Lattice Theory (1967), Amer. Math. Soc: Amer. Math. Soc Providence, RI) · Zbl 0126.03801
[2] Bochmann, G., Finite state description of communication protocols, (Proceedings, Comp. Network Protocols Symp. (1978)), 361-371, Liège, Belgium
[3] Bochmann, G.; Finkel, A., (2nd International Symposium on Interoperable information Systems (ISIIS’88). 2nd International Symposium on Interoperable information Systems (ISIIS’88), Tokyo, Japan (10-11 November 1988))
[4] Brams, G. W., (Réseaux de Petri: Théorie et pratique, Vol. 1 (1983), Masson: Masson Paris)
[5] Brand, D.; Zafiropulo, P., On communicating finite state machines, J. Assoc. Comput. Mach., 2, 323-342 (1983) · Zbl 0512.68039
[6] (Brauer, W.; Reisig, W.; Rosenberg, G., Petri nets: Central models and their properties. Petri nets: Central models and their properties, Advances in Petri Nets 1986, Vol. 255 (1986), Springer-Verlag: Springer-Verlag Berlin), Part 1, “Proceedings, Advanced Course at Bad Honnef,” Lecture Notes in Computer Science
[7] Choquet, A., Analyse et propriétés des processus communiquant par files fifo: Réseaux à files à choix libre topologique et réseaux à files linéaires, (Thèse de 3-ième cycle (1987), Université Paris 11)
[8] Choquet, A.; Finkel, A., (Simulation of Linear Fifo Nets by Petri Nets Having a Structured Set of Terminal Markings (1987), Univ. Paris 11: Univ. Paris 11 Orsay), in “8th European Workshop on Appl. and Theo. of Petri Nets, Zaragoza, Spain.”
[9] Dickson, L. E., Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors, Amer. J. Math., 35, 413-422 (1913) · JFM 44.0220.02
[10] Finkel, A., Structuration des systèmes de transitions: Applications au contrôle du parallélisme par files Fifo, Thèse d’Etat Université d’Orsay (1986)
[11] Finkel, A., A generalization of the procedure of Karp and Miller to well structured transition systems, (14th International Colloquim Automata, Languages, Programming. 14th International Colloquim Automata, Languages, Programming, Karlsruhe, R.F.A.. 14th International Colloquim Automata, Languages, Programming. 14th International Colloquim Automata, Languages, Programming, Karlsruhe, R.F.A., Lectures Notes in Computer Science, Vol. 267 (1987), Springer-Verlag: Springer-Verlag Berlin), 409-508
[12] Finkel, A.; Gouda, M.; Gurari, E.; Lai, T.; Rosier, L., On deadlock detection in systems of communicating finite state machines, (A New Class of Analysable CFSMs with Unbounded Fifo Channels: Application to Communication Protocol and Distributed Solution of the Mutual Exclusion Problem (1988)). (Comput. Artificial Intelligence, 6 (1987)), 209-228, Internal Report of the University of Montréal, No. 639; (revised version) A new class of analyzable CFSMs with unbounded Fifo channels, in “8th International Symposium on Protocol Specification, Testing, and Verification, Atlantic City, New Jersey, USA,” IFIP WG 6.1 88 · Zbl 0639.68009
[13] Hack, M., (Petri Net Language (1975), Massachusetts Institute of Technology: Massachusetts Institute of Technology Cambridge, MA), Comp. Struct. Group Memo 124, Project MAC
[14] Hack, M., Decidability Questions for Petri Nets (1976), MIT, LCS, TR 161, Cambridge, MA
[15] Higman, G., Ordering by divisibility in abstract algebras, (Proceedings, London Math. Soc. 2 (1952)) · Zbl 0047.03402
[16] Hopcroft, J.; Ullman, J., (Introduction to Automata Theory, Languages, and Computation (1979), Addison-Wesley: Addison-Wesley Reading, MA) · Zbl 0426.68001
[17] Jensen, K., Coloured Petri nets and the invariants method, Theoret. Comput. Sci., 14, 3, 317-336 (1981) · Zbl 0475.68035
[18] Karp, R. M.; Miller, R. E., Parallel program schemata, J. Comput. System Sci., 4, 147-195 (1969) · Zbl 0198.32603
[19] Kasai, T.; Miller, R. E., Homomorphisms between models of parallel computation, J. Comput. System Sci., 25, 285-331 (1982) · Zbl 0506.68047
[20] Keller, R. M., (Vector Replacement Systems: A Formalism for Modeling Asynchronous Systems (1972), Princeton Univ), Tech. Rep. No. 117
[21] Keller, R. M., Formal verification of parallel program, Comm. ACM, 19, 7, 371-384 (1976) · Zbl 0329.68016
[22] Koenig, D., (Theorie der Endlichen und unendlichen Graphen (1936), Akademische Verlagsgesellschaft: Akademische Verlagsgesellschaft Leipzig) · JFM 62.0654.05
[23] Kosaraju, S. R., Decidability of reachability in vector addition systems, (Proceedings, 14th Ann. ACM Symp. on Theor. of Comp. (1982))
[24] Kruskal, J. B., The theory of well-quasi-ordering: A frequently rediscovered concept, J. Combin. Theory Ser. A, 13 (1972) · Zbl 0244.06002
[25] Mayr, E. W., An algorithm for the general Petri net reachability problem, (SIAM J. Computing, Vol. 13 (1984)), No. 3 · Zbl 0563.68057
[26] Memmi, G.; Finkel, A., An introduction to Fifo nets—monogeneous nets: A subclass of Fifo nets, Theoret. Comput. Sci., 35 (1985) · Zbl 0566.68054
[27] Pachl, J., Protocol description and analysis based on a state transition model with channel expressions, (6th Inter. Workshop on Protocol Specification, Testing, and Verification. 6th Inter. Workshop on Protocol Specification, Testing, and Verification, Montréal, Québec. 6th Inter. Workshop on Protocol Specification, Testing, and Verification. 6th Inter. Workshop on Protocol Specification, Testing, and Verification, Montréal, Québec, IFIP 86 (1986), North-Holland: North-Holland Amsterdam)
[29] Peterson, J. L., (Petri Net Theory and the Modelling of Systems (1981), Prentice-Hall: Prentice-Hall Princeton, NJ) · Zbl 0461.68059
[30] Rosier, L. E.; Gouda, M., On deciding progress for a class of communicating protocols, (Proceedings, 8th Ann. Conf. on Inf. Sci. and Syst.. Proceedings, 8th Ann. Conf. on Inf. Sci. and Syst., Princeton University (1984)), 663-667
[31] Rosier, L. E.; Yen, H. C., Boundedness, empty channel detection, and synchronisation for communicating finite automata, Theoret. Comput. Sci., 44, 1, 69-106 (1986) · Zbl 0614.68049
[32] Valk, R.; Jantzen, M., The residue of vector sets with applications to decidability problems in Petri nets, Acta Inform., 21 (1985) · Zbl 0613.68029
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.