Here is a picture of the class of alternating automata, containing dual the subclasses of existential automata (a.k.a. non-deterministic automata) and universal automata.
Currently, HOA v1 uses no-univ-branch to indicate existential automata, and deterministic to indicate universal automata. This is unfortunate, because it makes no-univ-branch the dual of deterministic.
Since we have already renamed no-univ-branch into !univ-branch, I would like to propose that we rename the actual deterministic property as !exist-branch, and that we define deterministic as syntactic-sugar for !univ-branch !exist-branch.
For tools that only work with automata without universal branching, this does not change the semantic of deterministic. The change of semantic of deterministic only matters to tools working with alternating automata, but I don't think any of them used deterministic (at least ltl3ba -H1 and ltl3dra -H1 never seems to output deterministic).
Spot 2.3 uses deterministic in the specified sense for alternating automata, but I'd really like to change that as suggested, to get in line with existing literature. In particular when complementing an automaton by dualization (See for instance Section 1.6 of Löding's Diploma Thesis), I'd really like that an exist-branch !univ-branch automaton becomes a !exist-branch univ-branch automaton.
strejcek
commented
7 years ago
Here is a picture of the class of alternating automata, containing dual the subclasses of existential automata (a.k.a. non-deterministic automata) and universal automata.
Currently, HOA v1 uses
no-univ-branchto indicate existential automata, anddeterministicto indicate universal automata. This is unfortunate, because it makesno-univ-branchthe dual ofdeterministic.Since we have already renamed
no-univ-branchinto!univ-branch, I would like to propose that we rename the actualdeterministicproperty as!exist-branch, and that we definedeterministicas syntactic-sugar for!univ-branch !exist-branch.For tools that only work with automata without universal branching, this does not change the semantic of
deterministic. The change of semantic ofdeterministiconly matters to tools working with alternating automata, but I don't think any of them useddeterministic(at leastltl3ba -H1andltl3dra -H1never seems to outputdeterministic).Spot 2.3 uses
deterministicin the specified sense for alternating automata, but I'd really like to change that as suggested, to get in line with existing literature. In particular when complementing an automaton by dualization (See for instance Section 1.6 of Löding's Diploma Thesis), I'd really like that anexist-branch !univ-branchautomaton becomes a!exist-branch univ-branchautomaton.