Name
Title | ||
|---|---|---|
Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective. |
Abstract | ||
|---|---|---|
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 (nondeterministic) Buechi automata the notion of fair simulation has been introduced by Henzinger, Kupferman and Rajamani. We contribute generalization of fair simulation in two different directions: one for nondeterministic tree automata (this has been studied previously by Bomhard); and the other for probabilistic word automata (with a finite state space), both under the Buechi acceptance condition. The former (nondeterministic) definition is formulated in terms of systems of fixed-point equations, hence is readily translated to parity games and then amenable to Jurdzinski'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 Buechi automata; the proofs of soundness (i.e. that a simulation indeed witnesses language inclusion) are based on these coalgebraic observations, too. |
Year | Venue | DocType |
|---|---|---|
2017 | Logical Methods in Computer Science | Journal |
Volume | Issue | Citations |
abs/1606.04680 | 3 | 0 |
PageRank | References | Authors |
0.34 | 13 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Natsuki Urabe | 1 | 14 | 4.69 |
| Shunsuke Shimizu | 2 | 0 | 0.34 |
| Ichiro Hasuo | 3 | 260 | 26.13 |