# zbMATH — the first resource for mathematics

A generic framework for checking semantic equivalences between pushdown automata and finite-state automata. (English) Zbl 1378.68106
Summary: For a given process equivalence, we say that a process $$g$$ is fully equivalent to a process $$f$$ of a transition system $$\mathcal{T}$$ if $$g$$ is equivalent to $$f$$ and every reachable state of $$g$$ is equivalent to some state of $$\mathcal{T}$$. We propose a generic method for deciding full equivalence between pushdown processes and finite-state processes applicable to every process equivalence satisfying certain abstract conditions. Then, we show that these conditions are satisfied by bisimulation-like equivalences (including weak and branching bisimilarity), weak simulation equivalence, and weak trace equivalence, which are the main conceptual representatives of the linear/branching time spectrum. The list of particular results obtained by applying our method includes items which are first of their kind, and the associated upper complexity bounds are essentially optimal.

##### MSC:
 68Q45 Formal languages and automata 68Q60 Specification and verification (program logics, model checking, etc.) 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
##### Keywords:
pushdown automata; semantic equivalences; bisimulation
Full Text:
##### References:
 [1] Abdulla, P. A.; Čerāns, K., Simulation is decidable for one-counter nets, (Proceedings of CONCUR’98, Lecture Notes in Computer Science, vol. 1466, (1998), Springer), 253-268 · Zbl 0940.68055 [2] Alur, R.; Etessami, K.; Madhusudan, P., A temporal logic of nested calls and returns, (Proceedings of TACAS 2004, Lecture Notes in Computer Science, vol. 2988, (2004), Springer), 467-481 · Zbl 1126.68466 [3] Alur, R.; Etessami, K.; Yannakakis, M., Analysis of recursive state machines, (Proceedings of CAV 2001, Lecture Notes in Computer Science, vol. 2102, (2001), Springer), 207-220 · Zbl 0991.68535 [4] 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, 3, 653-682, (1993) · Zbl 0801.68102 [5] Baeten, J. C.M.; Weijland, W. P., Process algebra, Cambridge Tracts in Theoretical Computer Science, vol. 18, (1990), Cambridge University Press · Zbl 0716.68002 [6] Benedikt, M.; Göller, S.; Kiefer, S.; Murawski, A., Bisimilarity of pushdown automata is nonelementary, (Proceedings of LICS 2013, (2013), IEEE Computer Society Press), 488-498 · Zbl 1366.68136 [7] Böhm, S.; Göller, S.; Jančar, P., Bisimilarity of one-counter processes is PSPACE-complete, (Proceedings of CONCUR 2010, Lecture Notes in Computer Science, vol. 6269, (2010), Springer), 177-191 · Zbl 1287.68122 [8] Böhm, S.; Göller, S.; Jančar, P., Equivalence of deterministic one-counter automata is NL-complete, (Proceedings of STOC 2013, (2013), ACM Press), 131-140 · Zbl 1293.68181 [9] Bouajjani, A., Languages, rewriting systems, and verification of infinite-state systems, (Proceedings of ICALP’2001, Lecture Notes in Computer Science, vol. 2076, (2001), Springer), 24-39 · Zbl 0986.68517 [10] Bouajjani, A.; Esparza, J.; Maler, O., Reachability analysis of pushdown automata: application to model checking, (Proceedings of CONCUR’97, Lecture Notes in Computer Science, vol. 1243, (1997), Springer), 135-150 [11] Burkart, O.; Caucal, D.; Moller, F.; Steffen, B., Verification on infinite structures, (Handbook of Process Algebra, (2001)), 545-623 · Zbl 1035.68067 [12] Burkart, O.; Caucal, D.; Steffen, B., An elementary decision procedure for arbitrary context-free processes, (Proceedings of MFCS’95, Lecture Notes in Computer Science, vol. 969, (1995), Springer), 423-433 · Zbl 1193.68172 [13] Carayol, A.; Hague, M., Saturation algorithms for model-checking pushdown systems, Electron. Proc. Theor. Comput. Sci., 151, 1-24, (2014) [14] Caucal, D., Graphes canoniques des graphes algébriques, RAIRO Theor. Inform. Appl., 24, 4, 339-352, (1990) · Zbl 0701.68082 [15] Caucal, D.; Huynh, D. T.; Tian, L., Deciding branching bisimilarity of normed context-free processes in $$\operatorname{\Sigma}_2^p$$, Inf. Comput., 118, 2, 306-315, (1995) · Zbl 0826.68043 [16] Christensen, S.; Hüttel, H.; Stirling, C., Bisimulation equivalence is decidable for all context-free processes, Inf. Comput., 121, 143-148, (1995) · Zbl 0833.68074 [17] Czerwiński, W.; Jančar, P., Branching bisimilarity of normed BPA processes is in NEXPTIME, (Proceedings of LICS 2015, (2015)), 168-179 · Zbl 1392.68292 [18] Esparza, J., Decidability of model checking for infinite-state concurrent systems, Acta Inform., 34, 85-107, (1997) · Zbl 0865.68046 [19] Esparza, J.; Hansel, D.; Rossmanith, P.; Schwoon, S., Efficient algorithms for model checking pushdown systems, (Proceedings of CAV 2000, Lecture Notes in Computer Science, vol. 1855, (2000), Springer), 232-247 · Zbl 0974.68116 [20] Esparza, J.; Knoop, J., An automata-theoretic approach to interprocedural data-flow analysis, (Proceedings of FoSSaCS’99, Lecture Notes in Computer Science, vol. 1578, (1999), Springer), 14-30 [21] Esparza, J.; Kučera, A.; Schwoon, S., Model-checking LTL with regular valuations for pushdown systems, Inf. Comput., 186, 2, 355-376, (2003) · Zbl 1078.68081 [22] Esparza, J.; Schwoon, S., A BDD-based model checker for recursive programs, (Proceedings of CAV 2001, Lecture Notes in Computer Science, vol. 2102, (2001), Springer), 324-336 · Zbl 0991.68539 [23] Friedman, E. P., The inclusion problem for simple languages, Theor. Comput. Sci., 1, 4, 297-316, (1976) · Zbl 0349.68032 [24] Fu, Y., Checking equality and regularity for normed BPA with silent moves, (Proceedings of ICALP 2013, Part II, Lecture Notes in Computer Science, vol. 7966, (2013), Springer), 238-249 · Zbl 1335.68171 [25] Göller, S.; Mayr, R.; To, A. W., On the computational complexity of verifying one-counter processes, (Proceedings of LICS 2009, (2009), IEEE Computer Society Press), 235-244 [26] Groote, J. F., A short proof of the decidability of bisimulation for normed BPA processes, Inf. Process. Lett., 42, 167-171, (1992) · Zbl 0779.68029 [27] He, C.; Huang, M., Branching bisimilarity on normed BPA is EXPTIME-complete, (Proceedings of LICS 2015, (2015)), 180-191 · Zbl 1392.68302 [28] Hirshfeld, Y.; Jerrum, M.; Moller, F., A polynomial algorithm for deciding bisimilarity of normed context-free processes, Theor. Comput. Sci., 158, 1-2, 143-159, (1996) · Zbl 0871.68086 [29] Hofman, P.; Lasota, S.; Mayr, R.; Totzke, P., Simulation problems over one-counter nets, Log. Methods Comput. Sci., 1, 6, (2016) · Zbl 1448.68342 [30] Hopcroft, J. E.; Ullman, J. D., Introduction to automata theory, languages, and computation, (1979), Addison-Wesley · Zbl 0196.01701 [31] Hüttel, H., Silence is Golden: branching bisimilarity is decidable for context-free processes, (Proceedings of CAV’91, Lecture Notes in Computer Science, vol. 575, (1992), Springer), 2-12 [32] Hüttel, H.; Stirling, C., Actions speak louder than words: proving bisimilarity for context-free processes, J. Log. Comput., 8, 4, 485-509, (1998) · Zbl 0904.68129 [33] Jančar, P., Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof), Log. Methods Comput. Sci., 9, 1, (2012) [34] Jančar, P., Bisimulation equivalence of first-order grammars, (Proceedings of ICALP 2014, Part II, Lecture Notes in Computer Science, vol. 8573, (2014), Springer), 232-243 · Zbl 1410.68192 [35] Jančar, P., Equivalences of pushdown systems are hard, (Proceedings of FoSSaCS 2014, Lecture Notes in Computer Science, vol. 8412, (2014), Springer), 1-28 · Zbl 1407.68258 [36] Jančar, P.; Kučera, A.; Moller, F., Simulation and bisimulation over one-counter processes, (Proceedings of STACS 2000, Lecture Notes in Computer Science, vol. 1770, (2000), Springer), 334-345 · Zbl 0962.68121 [37] Jančar, P.; Moller, F., Techniques for decidability and undecidability of bisimilarity, (Proceedings of CONCUR’99, Lecture Notes in Computer Science, vol. 1664, (1999), Springer), 30-45 · Zbl 0940.68087 [38] Jančar, P.; Moller, F.; Sawa, Z., Simulation problems for one-counter machines, (Proceedings of SOFSEM’99, Lecture Notes in Computer Science, vol. 1725, (1999), Springer), 404-413 · Zbl 0963.68094 [39] Kiefer, S., BPA bisimilarity is EXPTIME-hard, Inf. Process. Lett., 113, 4, 101-106, (2013) · Zbl 1259.68145 [40] Kučera, A., On finite representations of infinite-state behaviours, Inf. Process. Lett., 70, 1, 23-30, (1999) · Zbl 1002.68093 [41] Kučera, A., The complexity of bisimilarity-checking for one-counter processes, Theor. Comput. Sci., 304, 1-3, 157-183, (2003) · Zbl 1044.68099 [42] Kučera, A.; Esparza, J., A logical viewpoint on process-algebraic quotients, J. Log. Comput., 13, 6, 863-880, (2003) · Zbl 1093.68066 [43] Kučera, A.; Jančar, P., Equivalence-checking on infinite-state systems: techniques and results, Theory Pract. Log. Program., 6, 3, 226-264, (2006) · Zbl 1101.68700 [44] Kučera, A.; Mayr, R., Simulation preorder over simple process algebras, Inf. Comput., 173, 2, 184-198, (2002) · Zbl 1009.68083 [45] Kučera, A.; Mayr, R., Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time, Theor. Comput. Sci., 270, 1-2, 677-700, (2002) · Zbl 0988.68118 [46] Kučera, A.; Mayr, R., On the complexity of checking semantic equivalences between pushdown processes and finite-state processes, Inf. Comput., 208, 7, 772-796, (2010) · Zbl 1194.68162 [47] Kučera, A.; Schnoebelen, Ph., A general approach to comparing infinite-state systems with their finite-state specifications, Theor. Comput. Sci., 358, 2-3, 315-333, (2006) · Zbl 1097.68075 [48] Mayr, R., Undecidability of weak bisimulation equivalence for 1-counter processes, (Proceedings of ICALP 2003, Lecture Notes in Computer Science, vol. 2719, (2003), Springer), 570-583 · Zbl 1039.68084 [49] Moller, F., Infinite results, (Proceedings of CONCUR’96, Lecture Notes in Computer Science, vol. 1119, (1996), Springer), 195-216 [50] Park, D. M.R., Concurrency and automata on infinite sequences, (Proceedings 5th GI Conference, Lecture Notes in Computer Science, vol. 104, (1981), Springer), 167-183 [51] Sénizergues, G., L(A)=L(B)? decidability results from complete formal systems, Theor. Comput. Sci., 251, 1-2, 1-166, (2001) · Zbl 0957.68051 [52] Sénizergues, G., The bisimulation problem for equational graphs of finite out-degree, SIAM J. Comput., 34, 5, 1025-1106, (2005) · Zbl 1079.68066 [53] Srba, J., Roadmap of infinite results, Bull. Eur. Assoc. Theor. Comput. Sci., 78, 163-175, (2002) · Zbl 1169.68554 [54] Srba, J., Undecidability of weak bisimilarity for pushdown processes, (Proceedings of CONCUR 2002, Lecture Notes in Computer Science, vol. 2421, (2002), Springer), 579-593 · Zbl 1012.68138 [55] Stirling, C., Decidability of DPDA equivalence, Theor. Comput. Sci., 255, 1-31, (2001) · Zbl 0974.68056 [56] van Glabbeek, R., What is branching time semantics and why to use it?, Bull. Eur. Assoc. Theor. Comput. Sci., 53, 191-198, (1994) · Zbl 0810.68093 [57] van Glabbeek, R., The linear time—branching time spectrum, (Handbook of Process Algebra, (2001)), 3-99 · Zbl 1035.68073 [58] van Glabbeek, R. J., The linear time—branching time spectrum II: the semantics of sequential systems with silent moves, (Proceedings of CONCUR’93, Lecture Notes in Computer Science, vol. 715, (1993), Springer), 66-81 [59] 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 [60] Yin, Q.; Fu, Y.; He, C.; Huang, M.; Tao, X., Branching bisimilarity checking for PRS, (Proceedings of ICALP 2014, Part II, Lecture Notes in Computer Science, vol. 8573, (2014), Springer), 363-374 · Zbl 1409.68190
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.