×

zbMATH — the first resource for mathematics

Simulation preorder over simple process algebras. (English) Zbl 1009.68083
Summary: We consider the problem of simulation preorder/equivalence between infinite-state processes and finite-state ones. First, we describe a general method how to utilize the decidability of bisimulation problems to solve (certain instances of) the corresponding simulation problems. For certain process classes, the method allows us to design effective reductions of simulation problems to their bisimulation counterparts and some new decidability results for simulation have already been obtained in this way. Then we establish the decidability border for the problem of simulation preorder/equivalence between infinite-state processes and finite-state ones w.r.t. the hierarchy of process rewrite systems. In particular, we show that simulation preorder (in both directions) and simulation equivalence are decidable in EXPTIME between pushdown processes and finite-state ones. On the other hand, simulation preorder is undecidable between PA and finite-state processes in both directions. These results also hold for those PA and finite-state processes which are deterministic and normed, and thus immediately extend to trace preorder. Regularity (finiteness) w.r.t. simulation and trace equivalence is also shown to be undecidable for PA. Finally, we prove that simulation preorder (in both directions) and simulation equivalence are intractable between all classes of infinite-state systems (in the hierarchy of process rewrite systems) and finite-state ones. This result is obtained by showing that the problem whether a BPA (or BPP) process simulates a finite-state one is PSPACE-hard and the other direction is co\(\mathcal{NP}\)-hard; consequently, simulation equivalence between BPA (or BPP) and finite-state processes is also co\(\mathcal{NP}\)-hard.
Reviewer: Reviewer (Berlin)

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P. A., and Čerāns, K.1998, Simulation is decidable for one-counter nets, inProceedings of CONCUR’98, Lecture Notes in Computer Science, Vol. 1466, pp. 253-268, Springer-Verlag, Berlin.
[2] Baeten, J. C. M, and, Weijland, W. P. 1990, Process Algebra, Cambridge Tracts in Theoretical Computer Science, No. 18, Cambridge Univ. Press, Cambridge, UK. · Zbl 0716.68002
[3] Bouajjani, A., Esparza, J., and Maler, O.1997, Reachability analysis of pushdown automata: Application to model checking, inProceedings of CONCUR’97, Lecture Notes in Computer Science, Vol. 1243, pp. 135-150, Springer-Verlag, Berlin.
[4] Burkart, O., Caucal, D., Moller, F., and Steffen, B.2001, Verification on infinite structures, inHandbook of Process AlgebraJ. A. Bergstra, A. Ponse, and S. A. Smolka, Eds., pp. 545-623, Elsevier, Amsterdam. · Zbl 1035.68067
[5] Burkart, O., Caucal, D., and Steffen, B.1996, Bisimulation collapse and the process taxonomy, inProceedings of CONCUR’96, Lecture Notes in Computer Science, Vol. 1119, pp. 247-262, Springer-Verlag, Berlin.
[6] Caucal, D., On the regular structure of prefix rewriting, Theoret. comput. sci., 106, 61-86, (1992) · Zbl 0780.68077
[7] Christensen, S., Hirshfeld, Y., and Moller, F.1993, Bisimulation is decidable for all basic parallel processes, inProceedings of CONCUR’93, Lecture Notes in Computer Science, Vol. 715, pp. 143-157, Springer-Verlag, Berlin.
[8] 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
[9] Groote, J.F.; Hüttel, H., Undecidable equivalences for basic process algebra, Inform. and comput., 115, 353-371, (1994) · Zbl 0834.68069
[10] Hopcroft, J. E, and, Ullman, J. D. 1979, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, MA. · Zbl 0426.68001
[11] Hüttel, H.1994, Undecidable equivalences for basic parallel processes, inProceedings of TACS’94, Lecture Notes in Computer Science, Vol. 789, pp. 454-464, Springer-Verlag, Berlin.
[12] Jančar, P., Decidability of bisimilarity for one-counter processes, Inform. and comput., 158, 1-17, (2000) · Zbl 1046.68621
[13] Jančar, P., and Esparza, J.1996, Deciding finiteness of Petri nets up to bisimilarity, inProceedings of ICALP’96, Lecture Notes in Computer Science, Vol. 1099, pp. 478-489, Springer-Verlag, Berlin.
[14] Jančar, P.; Kučera, A.; Mayr, R., Deciding bisimulation-like equivalences with finite-state processes, Theoret. comput. sci., 258, 409-433, (2001) · Zbl 0974.68131
[15] Jančar, P., Kučera, A., and Moller, F.2000, Simulation and bisimulation over one-counter processes, inProceedings of STACS 2000, Lecture Notes in Computer Science, Vol. 1770, pp. 334-345, Springer-Verlag, Berlin.
[16] Jančar, P., and Moller, F.1995, Checking regular properties of Petri nets, inProceedings of CONCUR’95, Lecture Notes in Computer Science, Vol. 962, pp. 348-362, Springer-Verlag, Berlin.
[17] Jančar, P., Moller, F., and Sawa, Z.1999, Simulation problems for one-counter machines, inProceedings of SOFSEM’99, Lecture Notes in Computer Science, Vol. 1725, pp. 404-413, Springer-Verlag, Berlin.
[18] Kozen, D., Results on the propositional μ-calculus, Theoret. comput. sci., 27, 333-354, (1983) · Zbl 0553.03007
[19] Kučera, A.1996, Regularity is decidable for normed PA processes in polynomial time, inProceedings of FST&TCS’96, Lecture Notes in Computer Science, Vol. 1180, pp. 111-122, Springer-Verlag, Berlin.
[20] Kučera, A.2000, Efficient verification algorithms for one-counter processes, inProceedings of ICALP 2000, Lecture Notes in Computer Science, Vol. 1853, pp. 317-328, Springer-Verlag, Berlin.
[21] Kučera, A.2000, On simulation-checking with sequential systems, inProceedings of ASIAN 2000, Lecture Notes in Computer Science, Vol. 1961, pp. 133-148, Springer-Verlag, Berlin.
[22] Kučera, A.; Mayr, R., Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time, Theoret. comp. sci., 270, 667-700, (2002) · Zbl 0988.68118
[23] Kučera, A., and Mayr, R.1999, Weak bisimilarity with infinite-state systems can be decided in polynomial time, inProceedings of CONCUR’99, Lecture Notes in Computer Science, Vol. 1664, pp. 368-382, Springer-Verlag, Berlin.
[24] Mayr, R.2000, On the complexity of bisimulation problems for pushdown automata, inProceedings of IFIP TCS’2000, Lecture Notes in Computer Science, Vol. 1872, pp. 474-488, Springer-Verlag, Berlin. · Zbl 0998.68088
[25] Mayr, R., Process rewrite systems, Inform. and comput., 156, 264-286, (2000) · Zbl 1046.68566
[26] Milner, R. 1989, Communication and Concurrency, Prentice Hall, New York. · Zbl 0683.68008
[27] Minsky, M. L. 1967, Computation: Finite and Infinite Machines, Prentice Hall, New York. · Zbl 0195.02402
[28] Muller, D.E.; Schupp, P.E., The theory of ends, pushdown automata, and second order logic, Theoret. comput. sci., 37, 51-75, (1985) · Zbl 0605.03005
[29] Reisig, W. 1985, Petri Nets—An Introduction, Springer-Verlag, Berlin. · Zbl 0555.68033
[30] van Glabbeek, R. J.1990, The linear time—branching time spectrum, inProceedings of CONCUR’90, Lecture Notes in Computer Science, Vol. 458, pp. 278-297, Springer-Verlag, Berlin.
[31] Walukiewicz, I., Pushdown processes: games and model-checking, Inform. and comput., 164, 234-263, (2001) · Zbl 1003.68072
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.