000K  utf8
1100  $c2006
1500  eng
2050  urn:nbn:de:gbv:8-diss-16446
3000  Fritz, Carsten
4000  Simulation-based simplification of omega-automata$hChristian-Albrechts-Universität zu Kiel  [Fritz, Carsten]
4030  Kiel$nChristian-Albrechts-Universität zu Kiel
4209  We analyze simulation relations as heuristics for the simplification of omega-automata, i.e., of finite automata working on infinite strings. Our focus is on alternating omega-automata. We introduce direct, delayed, and fair simulation for alternating Büchi automata (ABA) and show that these relations are preorders, they imply language containment, and they can be computed in polynomial time. We introduce quotient constructions for ABA suited for direct and delayed simulation, and we show that our notions of simulation are compatible with the standard translation of ABA to non-alternating automata. We apply these results to the problem of translating formulas of propositional linear-time temporal logic (LTL) to nondeterministic automata. We develop a translation algorithm from LTL to equivalent nondeterministic automata with an on-the-fly use of simulation relations for simplification, and we compare our approach to tableau-based translation algorithms. We extend our notion of delayed simulation to alternating parity automata (APA), introduce variants of this relation suited for quotienting of APA, and develop a simulation-based simplification algorithm for APA. We give a sketch of how to apply these results to a fragment of the modal mu-calculus.
4950  https://nbn-resolving.org/urn:nbn:de:gbv:8-diss-16446$xR$3Volltext$534
4961  https://macau.uni-kiel.de/receive/diss_mods_00001644
5051  004
5550  alternating automata
5550  automata minimization
5550  Büchi-Automat
5550  Büchi automata
5550  LTL
5550  parity automata
5550  simulation relations
5550  Zweipersonenspiel