An efficient simulation algorithm on Kripke structures. (English) Zbl 1301.68189
Summary: A number of algorithms for computing the simulation preorder (and equivalence) on Kripke structures are available. Let \(\varSigma\) denote the state space, \(\rightarrow\) the transition relation and \(P_{\mathrm{sim}}\) the partition of \(\varSigma\) induced by simulation equivalence. While some algorithms are designed to reach the best space bounds, whose dominating additive term is \(| P_{\mathrm{sim}}|^2\), other algorithms are devised to attain the best time complexity \(O(| P_{\mathrm{sim}}\|\rightarrow |)\). We present a novel simulation algorithm which is both space and time efficient: it runs in \(O(| P_{\mathrm{sim}}|^2\log| P_{\mathrm{sim}}| +|\varSigma|\log|\varSigma| )\) space and \(O(| P_{\mathrm{sim}}\|\rightarrow|\log|\varSigma|)\) time. Our simulation algorithm thus reaches the best space bounds while closely approaching the best time complexity.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68W05 | Nonnumerical algorithms |
References:
| [1] | Abdulla, P.A., Bouajjani, A., Holík, L., Kaati, L., Vojnar, T.: Computing simulations over tree automata. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), LNCS 4963, pp. 93-108. Springer, Berlin (2008) · Zbl 1134.68391 |
| [2] | Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008) · Zbl 1179.68076 |
| [3] | Bloom, B.: Ready Simulation, Bisimulation, and the Semantics of CCS-Like Languages. Ph.D. thesis, Massachusetts Institute of Technology (1989) · Zbl 1255.68100 |
| [4] | Bloom, B., Paige, R.: Transformational design and implementation of a new efficient solution to the ready simulation problem. Sci. Comp. Program. 24(3), 189-220 (1995) · Zbl 0832.68050 · doi:10.1016/0167-6423(95)00003-B |
| [5] | Bustan, D., Grumberg, O.: Simulation-based minimization. ACM Trans. Comput. Log. 4(2), 181-204 (2003) · Zbl 1365.68319 · doi:10.1145/635499.635502 |
| [6] | Cécé, G.: Three Simulation Algorithms for Labelled Transition Systems (preprint) http://arxiv.org/abs/1301.1638 (2013) |
| [7] | Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Informatics—10 Years Back, 10 Years Ahead. LNCS 2000, pp. 176-194. Springer, Berlin (2001) |
| [8] | Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999) |
| [9] | Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: a semantics based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36-72 (1993) · doi:10.1145/151646.151648 |
| [10] | Cleaveland, R., Sokolsky, O.: Equivalence and preorder checking for finite-state systems. In: Handbook of Process Algebra, chapter 6, pp. 391-424. Elsevier, Amsterdam (2001) · Zbl 1020.68062 |
| [11] | Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd ed. The MIT Press/McGraw-Hill, Cambridge/New York (2001) · Zbl 1047.68161 |
| [12] | Crafa, S., Ranzato, F., Tapparo, F.: Saving space in a time efficient simulation algorithm. Fundam. Inform. 108(1-2), 23-42 (2011) · Zbl 1255.68100 |
| [13] | Fan, W., Wang, X., Wu, Y.: Incremental graph pattern matching. ACM Trans. Database Syst. 38(3), article no. 18 (2013) · Zbl 1321.68243 |
| [14] | Fisler, K., Vardi, M.Y.: Bisimulation minimization in an automata-theoretic verification framework. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Verification, LNCS 1522, pp. 115-132. Springer, Berlin (1998) |
| [15] | Fisler, K., Vardi, M.Y.: Bisimulation minimization and symbolic model checking. Formal Methods Syst. Des. 21(1), 39-78 (2002) · Zbl 1018.68052 · doi:10.1023/A:1016091902809 |
| [16] | Gentilini, R., Piazza, C., Policriti, A.: Simulation as coarsest partition problem. In: Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02), LNCS 2280, pp. 415-430. Springer, Berlin (2002) · Zbl 1043.68590 |
| [17] | Gentilini, R., Piazza, C., Policriti, A.: From bisimulation to simulation: coarsest partition problems. J. Autom. Reason. 31(1), 73-103 (2003) · Zbl 1081.68052 · doi:10.1023/A:1027328830731 |
| [18] | Gentilini, R., Piazza, C., Policriti, A.: Rank and simulation: the well-founded case. J. Logic Comput. (to appear) (2014) · Zbl 1328.68147 |
| [19] | Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Proceedings of the 17th ICALP, LNCS 443, pp. 626-638. Springer, Berlin (1990) · Zbl 0765.68125 |
| [20] | Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proceedings of the 36th IEEE FOCS, pp. 453-462. IEEE Press, New York (1995) · Zbl 0938.68538 |
| [21] | Holík, L., S̆imác̆ek, J.: Optimizing an LTS-simulation algorithm. Comput. Inform. 29(6+), 1337-1348 (2010) · Zbl 1399.65139 |
| [22] | Hopcroft, J.E.: A \[n \log n\] nlogn algorithm for minimizing states in a finite automaton. In: Kohavi, Z., Paz, A. (eds.) Theory of Machines and Computations, pp. 189-176. Academic Press, London (1971) · Zbl 1365.68319 |
| [23] | Markovski, J.: Saving time in a space-efficient simulation algorithm. In: Proceedings of the 11th International Conference on Quality Software, pp. 244-251. IEEE Press, New York (2011) |
| [24] | Nisar, M.U., Fard, A., Miller, J.A.: Techniques for graph analytics on big data. In: Proceedings of the 2013 IEEE International Congress on Big Data, pp. 255-262. IEEE Press, New York (2013) |
| [25] | Ranzato, F.: A more efficient simulation algorithm on Kripke structures. In: Proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS’13), LNCS 8087, pp. 753-764. Springer, Berlin (2013) · Zbl 1400.68143 |
| [26] | Ranzato, F., Tapparo, F.: A new efficient simulation equivalence algorithm. In: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS’07), pp. 171-180. IEEE Press, New York (2007) |
| [27] | Ranzato, F., Tapparo, F.: A time and space efficient simulation algorithm. In: Short Talk at 24th Annual IEEE Symposium on Logic in Computer Science (LICS’09) (2009) · Zbl 1188.68197 |
| [28] | Ranzato, F., Tapparo, F.: An efficient simulation algorithm based on abstract interpretation. Inf. Comput. 208(1), 1-22 (2010) · Zbl 1188.68197 · doi:10.1016/j.ic.2009.06.002 |
| [29] | Tan, L., Cleaveland, R.: Simulation revisited. In: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), LNCS 2031, pp. 480-495. Springer, Berlin (2001) · Zbl 0986.68165 |
| [30] | van Glabbeek, R.J.: The linear time-branching time spectrum I; the semantics of concrete, sequential processes. In: Handbook of Process Algebra, chapter 1, pp. 3-99. Elsevier, Amsterdam (2001) · Zbl 1035.68073 |
| [31] | van Glabbeek, R., Ploeger, B.: Correcting a space-efficient simulation algorithm. In: Proceedings of the 20th International Conference on Computer Aided Verification (CAV’08), LNCS 5123, pp. 517-529. Springer, Berlin (2008) · Zbl 1155.68450 |
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.
