on the semantics of parity acceptance #46
(This is my attempt to summarize an issue that Joachim reported to me by email.)
First, in a parity automaton every state is labeled by exactly one number and what
The problem is that in HOA we do not define parity automata. We only define parity acceptance, and in our context, the numbers are set numbers. So we have to give to
We could for instance decide that
But (this was Joachim's natural interpretation) we could also decide that it means "no acceptance set is visited infinitely often, or the maximum set visited infinitely often is odd". This gives the following encodings:
I believe these two semantics are equally valid, or maybe equally invalid...
In case of parity automata (i.e., with the guaranty that each state belong to exactly one set) the two views are equivalent (even for case 0, because the only parity automaton we can build without using any acceptance set is the empty automaton). So we basically have to choose what we want for the case where parity acceptance is used without that extra constraint.
What I do not like in these two semantic is the following. If we assume that some acceptance set has to be visited (first semantic) for all combinations of
If we take the other semantic, we get
I find both unsatisfactory, because they show no duality between
For this to work, we could decide for instance that
Joachim also suggested adding a
The text was updated successfully, but these errors were encountered:
I think I have way to decide what semantic we should use such that it behaves correctly even in the case where some state do not belong to any state.
The trick (for the
This implies that for
So that would give the following encodings:
Notice the perfect duality between
This would give the following encodings:
and I'm happy with those. What about you?
For the specification document, I would suggest to display all the above examples, and justify them with something like this:
I think in your
There is then (as should be expected) quite a nice regular structure and the duality is apparent, as well.
Hmm. If the discussion is whether to choose a more complicated semantics for the sake of universal duality between even and odd (which is the current proposal), or to choose a simpler semantics breaking the duality in some cases, then I slightly prefer the simpler semantics (I would say that an accepting run has to visit some acceptance set infinitely often).
I guess that parity acceptance without
@strejcek I agree with your second paragraph, but I'm not sure where you see the complication.
From what I can tell, the current text is underspecified, as it does explain how the acceptance is extended to corner cases like 0 acceptance sets, or whether an path that do not visit any set infinitely often should be accepting. Since we want to have clear semantics so that tools can rely on
Now there is also the implementation complexity. I've implemented both semantics, and generating a parity acceptance condition with the the one suggested is here is slightly easier because you do not have to wonder whether set 0 or n-1 should appear in the condition: they always do. The Acceptance conditions with the current proposal are actually very straightforward to generate, as all sets always used, and they degenerate very naturally to 't' and 'f' in the case of 0 sets. The justification for
I think anybody looking at these patterns (even without the superfluous
I realize that for the
So with all that I conclude that the proposal diminishes the complexity of our format, and makes it more elegant (because we preserve duality between odd and even).
BTW, this paper is an example of construction of automata with transition-based parity acceptance, where a transition may naturally belong to no acceptance set. So this stuff do appear in practice. Unfortunately, the
Alexandre Lewkowicz, one of our students who is implementing some variant of the above paper, pointed out to me that because of the min(∅)=n assumption, if we take an automaton with
I cannot see any easy fix. But I don't think that this is a big issue. What matters is the "Acceptance:" definition and I like the current formulation of canonical Acceptance conditions for parity automata.
What I'm not completely happy with is the definition of