Urabe, Natsuki and Hasuo, Ichiro - Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective

lmcs:3907 - Logical Methods in Computer Science, September 6, 2017, Volume 13, Issue 3
Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective

Authors: Urabe, Natsuki and Hasuo, Ichiro

Notions of simulation, among other uses, provide a computationally tractable and sound (but not necessarily complete) proof method for language inclusion. They have been comprehensively studied by Lynch and Vaandrager for nondeterministic and timed systems; for Büchi automata the notion of fair simulation has been introduced by Henzinger, Kupferman and Rajamani. We contribute to a generalization of fair simulation in two different directions: one for nondeterministic tree automata previously studied by Bomhard; and the other for probabilistic word automata with finite state spaces, both under the Büchi acceptance condition. The former nondeterministic definition is formulated in terms of systems of fixed-point equations, hence is readily translated to parity games and is then amenable to Jurdzi\'{n}ski's algorithm; the latter probabilistic definition bears a strong ranking-function flavor. These two different-looking definitions are derived from one source, namely our coalgebraic modeling of Büchi automata. Based on these coalgebraic observations, we also prove their soundness: a simulation indeed witnesses language inclusion.


Source : oai:arXiv.org:1606.04680
DOI : 10.23638/LMCS-13(3:20)2017
Volume: Volume 13, Issue 3
Published on: September 6, 2017
Submitted on: September 6, 2017
Keywords: Computer Science - Logic in Computer Science


Share

Browsing statistics

This page has been seen 86 times.
This article's PDF has been downloaded 22 times.