Constrained properties, semilinear systems, and Petri nets. (English) Zbl 1514.68125
Montanari, Ugo (ed.) et al., CONCUR ‘96: Concurrency theory. 7th international conference, Pisa, Italy, August 26–29, 1996. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1119, 481-497 (1996).
Summary: We investigate the verification problem of two classes of infinite state systems w.r.t. nonregular properties (i.e., nondefinable by finite-state \(\Omega \)-automata). The systems we consider are Petri nets as well as semilinear systems including pushdown systems and PA processes. On the other hand, we consider properties expressible in the logic CLTL which is an extension of the linear-time temporal logic LTL allowing two kinds of constraints: pattern constraints using finite-state automata and counting constraints using Presburger arithmetics formulas. While the verification problem of CLTL is undecidable even for finite-state systems, we identify a fragment called CLTL\textsubscript{\(\square\)} for which the verification problem is decidable for pushdown systems as well as for Petri nets. This fragment is strictly more expressive than finite-state \(\omega \)-automata. We show that, however, the verification problem of semilinear systems (PA processes in particular) is undecidable even w.r.t. LTL formulas. Therefore, we identify another fragment (a restriction of LTL extended with counting constraints) covering a significant class of properties and for which the verification problem is decidable for all PA processes.
For the entire collection see [Zbl 0915.00046].
For the entire collection see [Zbl 0915.00046].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68Q45 | Formal languages and automata |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | P. Abdulla and B. Jonsson. Verifying Programs with Unreliable Channels. In LICS’93. IEEE, 1993. |
| [2] | J. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of Bisimulation Equivalence for Processes Generating Context-Free Languages. T.R. CS-R8632, 1987. CWI. |
| [3] | J.A. Bergstra and J.W. Klop. Process Theory based on Bisimulation Semantics. In REX School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, 1988. LNCS 354. |
| [4] | A. Bouajjani, R. Echahed, and P. Habermehl. On the Verification Problem of Nonregular Properties for Nonregular Processes. In LICS’95. IEEE, 1995. |
| [5] | A. Bouajjani, R. Echahed, and P. Habermehl. Verifying Infinite State Processes with Sequential and Parallel Composition. In POPL’95. ACM, 1995. |
| [6] | O. Burkart and B. Steffen. Pushdown Processes: Parallel Composition and Model Checking. In CONCUR’94, 1994. LNCS 836. |
| [7] | S. Christensen. Decidability and Decomposition in Process Algebra. PhD thesis, University of Edinburgh, 1993. |
| [8] | S. Christensen and H. Hüttel. Decidability Issues for Infinite State Processes — A Survey. Bull. of the EATCS, 51, 1993. · Zbl 0783.68042 |
| [9] | S. Christensen, H. Hüttel, and C. Stirling. Bisimulation Equivalence is Decidable for all Context-Free Processes. Information and Computation, 121, 1995. · Zbl 0833.68074 |
| [10] | R.S. Cohen and A.Y. Gold. Theory of \(Ω\)-Languages. I: Characterizations of \(Ω\)-Context-Free Languages. J.C.S.S., 15, 1977. · Zbl 0363.68113 |
| [11] | J. Esparza and A. Kiehn. On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes. In CAV’95. LNCS 939, 1995. |
| [12] | Javier Esparza. On the Decidability of Model-Checking for Several Mu-calculi and Petri Nets. In CAAP’94. LNCS 787, 1994. · Zbl 0938.03537 |
| [13] | R. Howell, L. Rosier, and H.C. Yen. A Taxonomy of Fairness and Temporal Logic Problems for Petri Nets. T.C.S., 82, 1991. · Zbl 0728.68090 |
| [14] | P. Jancar. Decidability of a Temp. Logic Problem for Petri Nets. T.C.S., 74, 1990. · Zbl 0701.68081 |
| [15] | E. Mayr. An Algorithm for the General Petri Net Reachability Problem. SIAM J. on Comput., 13, 1984. · Zbl 0563.68057 |
| [16] | A. Pnueli. The Temporal Logic of Programs. In FOCS’77. IEEE, 1977. |
| [17] | W. Thomas. Star-Free Regular Sets of \(Ω\)-Sequences. Inform. and Cont., 42, 1979. · Zbl 0411.03031 |
| [18] | R. Valk and M. Jantzen. The Residue of Vector Sets with Applications to Decidability Problems in Petri Nets. Acta Informatica, 21, 1985. · Zbl 0545.68051 |
| [19] | M.Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. In LICS’86. IEEE, 1986. |
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.
