A Hierarchy of Polynomial-Time Computable Simulations for Automata

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationCONCUR 2002 - Concurrency Theory
Subtitle of host publication13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings
PublisherSpringer Berlin Heidelberg
Pages131-144
Number of pages14
Volume2421
ISBN (Electronic)978-3-540-45694-0
ISBN (Print)978-3-540-44043-7
DOIs
Publication statusPublished - 2002

Fingerprint

Dive into the research topics of 'A Hierarchy of Polynomial-Time Computable Simulations for Automata'. Together they form a unique fingerprint.

Cite this