×

zbMATH — the first resource for mathematics

Deciding bisimulation-like equivalences with finite-state processes. (English) Zbl 0974.68131
Summary: We show that characteristic formulae for finite-state systems up to bisimulation-like equivalences (e.g., strong and weak bisimilarity) can be given in the simple branching-time temporal logic \(EF.\) Since \(EF\) is a very weak fragment of the modal \(\mu\)-calculus, model checking with \(EF\) is decidable for many more classes of infinite state systems. This yields a general method for proving decidability of bisimulation-like equivalences between infinite-state processes and finite-state ones. We apply this method to the class of PAD processes, which strictly subsumes PA and pushdown (PDA) processes, showing that a large class of bisimulation-like equivalences (including, e.g., strong and weak bisimilarity) is decidable between PAD and finite-state processes. On the other hand, we also demonstrate that no ‘reasonable’ bisimulation-like equivalence is decidable between state-extended PA processes and finite-state ones. Furthermore, weak bisimilarity with finite-state processes is shown to be undecidable even for state-extended BPP (which are also known as ‘parallel pushdown processes’).

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.W., Decidability of bisimulation equivalence for processes generating context-free languages, J. assoc. comput. Mach., 40, 653-682, (1993) · Zbl 0801.68102
[2] Baeten, J.C.M.; Weijland, W.P., Process algebra, Cambridge tracts in theoretical computer science, Vol. 18, (1990), Cambridge University Press Cambridge · Zbl 0716.68002
[3] Bouajjani, A.; Esparza, J.; Maler, O., (), 135-150
[4] Caucal, D., On the regular structure of prefix rewriting, Theoret. comput. sci., 106, 61-86, (1992) · Zbl 0780.68077
[5] Černá, I.; Křetı́nský, M.; Kučera, A., Comparing expressibility of normed BPA and normed BPP processes, Acta inform., 36, 3, 233-256, (1999) · Zbl 0947.68109
[6] Christensen, S.; Hirshfeld, Y.; Moller, F., (), 143-157
[7] Christensen, S.; Hüttel, H.; Stirling, C., Bisimulation equivalence is decidable for all context-free processes, Inform. and comput., 121, 143-148, (1995) · Zbl 0833.68074
[8] Esparza, J., Decidability of model checking for infinite-state concurrent systems, Acta inform., 34, 85-107, (1997) · Zbl 0865.68046
[9] Jančar, P., Decidability of a temporal logic problem for Petri nets, Theoret. comput. sci., 74, 71-93, (1990) · Zbl 0701.68081
[10] Jančar, P., Undecidability of bisimilarity for Petri nets and some related problems, Theoret. comput. sci., 148, 2, 281-301, (1995) · Zbl 0873.68147
[11] Jančar, P.; Esparza, J., (), 478-489
[12] P. Jančar, A. Kučera, Bisimilarity of processes with finite-state systems, Electronic Notes in Theoretical Computer Science, Vol. 9, 1997.
[13] Jančar, P.; Moller, F., (), 348-362
[14] Kučera, A., Effective decomposability of sequential behaviours, Theoret. comput. sci., 242, 71-89, (2000) · Zbl 0944.68065
[15] Kučera, A.; Mayr, R., (), 503-512
[16] Kučera, A.; Mayr, R., (), 368-382
[17] Lugiez, D.; Schnoebelen, Ph., (), 50-66
[18] Mayr, R., (), 88-99
[19] Mayr, R., (), 332-346
[20] R. Mayr, Decidability and complexity of model checking problems for infinite-state systems, Ph.D. Thesis, TU-München, 1998. · Zbl 0912.68035
[21] R. Mayr, Strict lower bounds for model checking BPA, Electronic Notes in Theoretical Computer Science, Vol. 18 (1998).
[22] Mayr, R., Decidability of model checking with the temporal logic EF, Theoret. comput. sci., 256, 31-62, (2001) · Zbl 0973.68169
[23] Mayr, R., Process rewrite systems, Inform. and comput., 156, 264-286, (2000) · Zbl 1046.68566
[24] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[25] Minsky, M.L., Computation: finite and infinite machines, (1967), Prentice-Hall Englewood Cliffs, NJ · Zbl 0195.02402
[26] Moller, F., (), 195-216
[27] Muller, D.E.; Schupp, P.E., The theory of ends, pushdown automata, and second order logic, Theoret. comput. sci., 37, 1, 51-75, (1985) · Zbl 0605.03005
[28] Park, D.M.R., (), 167-183
[29] Reisig, W., Petri nets – an introduction, (1985), Springer Berlin · Zbl 0555.68033
[30] Schnoebelen, Ph., Decomposable regular languages and the shuffle operator, EATCS bull., 67, 283-289, (1999)
[31] Steffen, B.; Ingólfsdóttir, A., Characteristic formulae for processes with divergence, Inform. comput., 110, 1, 149-163, (1994) · Zbl 0804.68097
[32] Stirling, C., Decidability of bisimulation equivalence for normed pushdown processes, Theoret. comput. sci., 195, 113-131, (1998) · Zbl 0915.68119
[33] van Glabbeek, R.J.; Weijland, W.P., Branching time and abstraction in bisimulation semantics, J. assoc. comput. Mach., 43, 3, 555-600, (1996) · Zbl 0882.68085
[34] Walukiewicz, I., (), 62-74
[35] Stirling, C., (), 142-151
[36] Thomas, W., (), 559-568
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.