Abstract
We define and provide algorithms for computing a natural hierarchy of simulation relations on the state-spaces of ordinary transition systems, finite automata, and Büchi automata. These simulations enrich ordinary simulation and can be used to obtain greater reduction in the size of automata by computing the automaton quotient with respect to their underlying equivalence. State reduction for Büchi automata is useful for making explicit-state model checking run faster ([EH00], [SB00], [EWS01]).
We define k-simulations, where 1-simulation corresponds to ordinary simulation and its variants for Büchi automata ([HKR97], [EWS01]), and k- simulations, for k > 1, generalize the game definition of 1-simulation by allowing the Duplicator to use k pebbles instead of 1 (to “hedge its bets”) in response to the Spoiler’s move of a single pebble. As k increases, k- simulations are monotonically non-decreasing relations. Indeed, when k reaches n, the number of states of the automaton, the n-simulations defined for finite-automata and for labeled transition systems correspond precisely to language containment and trace containment, respectively. But for each fixed k, the maximal k-simulation relation is computable in polynomial time: nO(k).
This provides a mechanism with which to trade off increased computing time for larger simulation relation size, and more potential reduction in automaton size. We provide algorithms for computing k-simulations using a natural generalization of a prior efficient algorithm based on parity games ([EWS01]) for computing various simulations.Last ly, we observe the relationship between k-simulations and a k-variable interpretation of modal logic.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
S. Abiteboul, P. Buneman, and D. Suciu. Data on the Web.Morgan Kaufmann, 1999.
K. Etessami and G. Holzmann. Optimizing Büchi automata.In Proc. of 11th Int. Conf on Concurrency Theory (CONCUR), pages 153–167, 2000.
K. Etessami, T. Wilke, and R. Schuller. Fair simulation relations, parity games, and state space reduction for Büchi automata.In Proc. of ICALP’2001, pages 694–707, 2001.
T. Henzinger, O. Kupferman, and S. Rajamani. Fair simulation. In Proc. of 9th Int. Conf. on Concurrency Theory (CONCUR’97), number 1243 in LNCS, pages 273–287, 1997.
M. Hennessey and R. Milner. Algebraic laws for nondeterminism and concurrency. J. of the ACM, 32(1):137–161, 1985.
G.J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, 1997.
T. Henzinger and S. Rajamani. Fair bisimulation. In 6th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS’2000), LNCS 1785, pages 299–314, 2000.
N. Immerman and K. Kozen. Definability with bounded number of bound variables. Inform. and Comput., 83:121–139, 1989.
M. Jurdziński. Small progress measures for solving parity games. In Proc. 17th Symp. Theoretical Aspects of Comp. Sci. (STACS), pages 290–301, 2000.
R. Kaushik, P. Shenoy, P. Bohannon, and E. Gudes. Explointing local similarity for indexing of paths in graph structured data.In Proc. of 18th Int. Conf. on Data Engineering (ICDE), 2002.
S. Safra. On the complexity of ω-automata. In Proc. of 29th Ann. Symp. on Foundations of Comp. Sci., pages 319–327, 1988.
F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In Proceedings of 12th Int. Conf. on Computer Aided Verification, 2000.
M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st Symp. on Logic in Comp. Sci. (LICS), pages 322–331, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Etessami, K. (2002). A Hierarchy of Polynomial-Time Computable Simulations for Automata. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds) CONCUR 2002 — Concurrency Theory. CONCUR 2002. Lecture Notes in Computer Science, vol 2421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45694-5_10
Download citation
DOI: https://doi.org/10.1007/3-540-45694-5_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44043-7
Online ISBN: 978-3-540-45694-0
eBook Packages: Springer Book Archive