Saving Space in a Time Efficient Simulation Algorithm

• Autorzy: Crafa, S. , Ranzato, F. , Tapparo, F.
• Języki publikacji: EN

Abstrakty

EN

A number of algorithms for computing the simulation preorder on Kripke structures and on labelled transition systems are available. Among them, the algorithm by Ranzato and Tapparo [2007] has the best time complexity,while the algorithmby Gentilini et al. [2003] – successively corrected by van Glabbeek and Ploeger [2008] – has the best space complexity. Both space and time complexities are critical issues in a simulation algorithm, in particular memory requirements are crucial in the context of model checking when dealing with large state spaces. Here, we propose a new simulation algorithm that is obtained as a space saving modification of the time efficient algorithm by Ranzato and Tapparo: a symbolic representation of sets is embedded in this algorithm so that any set of states manipulated by the algorithm can be efficiently stored as a set of blocks of a suitable state partition. It turns out that this novel simulation algorithm has a space complexity comparable with Gentilini et al.’s algorithm while improving on Gentilini et al.’s time bound.

Słowa kluczowe

EN

simulation preorder; simulation algorithm; coarsest partition problem

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 108, nr 1/2
• Strony: 23-42
• Opis fizyczny: Bibliogr. 19 poz., tab.

Twórcy

autor

Crafa, S.

autor

Ranzato, F.

autor

Tapparo, F.

• Dipartimento di Matematica Pura ed Applicata, University of Padova, Via Trieste 63, 35121 Padova, Italy,

Bibliografia

• [1] P.A. Abdulla, A, Bouajjani, L. Hol´ık, L. Kaati and T. Vojnar. Computing simulations over tree automata. In Proc. 14th TACAS, LNCS 4963, pp. 93-108, 2008.
• [2] C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.
• [3] B. Bloom and R. Paige. Transformational design and implementation of a new efficient solution to the ready simulation problem. Sci. Comp. Program., 24(3):189-220, 1995.
• [4] D. Bustan and O. Grumberg. Simulation-based minimization. ACM Trans. Comput. Log., 4(2):181-204, 2003.
• [5] E.M. Clarke, O. Grumberg and D.A. Peled. Model Checking. The MIT Press, 1999.
• [6] R. Cleaveland and S Sims. The NCSU concurrency workbench. In Proc. 8th CAV, LNCS 1102, pp. 394-397, 1996. http://www.cs.sunysb.edu/∼cwb.
• [7] R. Cleaveland and O. Sokolsky. Equivalence and preorder checking for finite-state systems. In Handbook of Process Algebra, chapter 6, pp. 391-424, Elsevier, 2001.
• [8] S. Crafa, F. Ranzato and F. Tapparo. Saving space in a time efficient simulation algorithm. In Proc. 9th ACSD, pp. 60-69, IEEE Press, 2009.
• [9] A. Dovier, C. Piazza and A. Policriti. An efficient algorithm for computing bisimulation equivalence. Theor. Comput. Sci., 311(1-3):221-256, 2004.
• [10] R. Gentilini, C. Piazza and A. Policriti. From bisimulation to simulation: coarsest partition problems. J. Automated Reasoning, 31(1):73-103, 2003.
• [11] R. van Glabbeek and B. Ploeger. Correcting a space-efficient simulation algorithm. In Proc. 20th CAV, LNCS 5123, pp. 517-529, 2008.
• [12] J.F. Groote, A. Mathijssen, M.A. Reniers, Y.S. Usenko and M. van Weerdenburg. The formal specification language mCRL2. In Proc. Methods for Modelling Software Systems, Dagstuhl Seminar Proceedings, 2006. http://www.mcrl2.org.
• [13] M.R. Henzinger, T.A. Henzinger and P.W. Kopke. Computing simulations on finite and infinite graphs. In Proc. 36th FOCS, pp. 453-462, IEEE Press, 1995.
• [14] A. Kučera and P. Jančar. Equivalence-checking on infinite-state systems: Techniques and results. Theory Pract. Log. Program., 6(3):227-264, 2006.
• [15] F. Ranzato and F. Tapparo. An efficient simulation algorithm based on abstract interpretation. Inform. And Comput., 208(1):1-22, 2010. Preliminary version in Proc. 22nd IEEE LICS'07.
• [16] D. Sangiorgi and D. Walker. The Pi Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001.
• [17] R. Segala. The power of simulation relations. In Proc. 27th PODC, pp. 462-462, ACM Press, 2008.
• [18] L. Tan and R. Cleaveland. Simulation revisited. In Proc. 7th TACAS, LNCS 2031, pp. 480-495, 2001.
• [19] The VLTS Benchmark Suite. http://www.inrialpes.fr/vasy /cadp/resources/benchmark bcg.html