Profile trees for Büchi word automata, with application to determinization
From MaRDI portal
Publication:897653
DOI10.1016/J.IC.2014.12.021zbMATH Open1336.68155arXiv1307.4471OpenAlexW1495139601MaRDI QIDQ897653FDOQ897653
Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, Thomas Wilke
Publication date: 7 December 2015
Published in: Information and Computation (Search for Journal in Brave)
Abstract: The determinization of Buchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by McNaughton, Safra, Piterman, Schewe, and others. Despite the proliferation of solutions, they are all essentially ad-hoc constructions, with little theory behind them other than proofs of correctness. Since Safra, all optimal constructions employ trees as states of the deterministic automaton, and transitions between states are defined operationally over these trees. The operational nature of these constructions complicates understanding, implementing, and reasoning about them, and should be contrasted with complementation, where a solid theory in terms of automata run DAGs underlies modern constructions. In 2010, we described a profile-based approach to Buchi complementation, where a profile is simply the history of visits to accepting states. We developed a structural theory of profiles and used it to describe a complementation construction that is deterministic in the limit. Here we extend the theory of profiles to prove that every run DAG contains a profile tree with at most a finite number of infinite branches. We then show that this property provides a theoretical grounding for a new determinization construction where macrostates are doubly preordered sets of states. In contrast to extant determinization constructions, transitions in the new construction are described declaratively rather than operationally.
Full work available at URL: https://arxiv.org/abs/1307.4471
Recommendations
Cites Work
- Alternating-time temporal logic
- The complexity of probabilistic verification
- Title not available (Why is that?)
- Observations on determinization of Büchi automata
- Title not available (Why is that?)
- Testing and generating infinite sequences by a finite automaton
- Tighter Bounds for the Determinisation of Büchi Automata
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- Weak alternating automata are not that weak
- Büchi Complementation Made Tight
- Title not available (Why is that?)
- Decision problems forω-automata
- Complementation, Disambiguation, and Determinization of Büchi Automata Unified
- Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
- Improved Algorithms for the Automata-Based Approach to Model-Checking
- Efficient Büchi Universality Checking
- Unifying B\"uchi Complementation Constructions
- BÜCHI COMPLEMENTATION MADE TIGHTER
Cited In (11)
- Projection for Büchi Tree Automata with Constraints between Siblings
- From Muller to parity and Rabin qutomata: optimal transformations preserving (history) determinism
- Projection for Büchi tree automata with constraints between siblings
- On the power of finite ambiguity in Büchi complementation
- Modular mix-and-match complementation of Büchi automata
- Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition
- Congruence Relations for Büchi Automata
- New Optimizations and Heuristics for Determinization of Büchi Automata
- From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
- Towards a grand unification of Büchi complementation constructions
- Proof systems for the modal \(\mu \)-calculus obtained by determinizing automata
This page was built for publication: Profile trees for Büchi word automata, with application to determinization
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q897653)
