on the semantics of parity acceptance

[adl]

(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 max odd or min even means is unambiguous: the maximum (or minimum) of the numbers that occur infinitely often along a path has to be odd (or even). The same definition could be done with transition-based parity automata, that isn't an issue either.

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 max odd or min even some semantics that work even if a state belongs to multiple sets or none. In particular the case were no set is visited infinitely often is troublesome, because the max and min do not exist, so it is hard to claim it to be odd or even.

We could for instance decide that max odd means "some acceptance set is visited infinitely often, and the maximum set visited infinitely often is odd". This is the view currently reflected in the specifications (but only implicitly, because of the examples given), and it gives the following encodings:

parity max odd 0: f
parity max odd 1: f
parity max odd 2: Inf(1)
parity max odd 3: Fin(2) & Inf(1)
parity max odd 4: Inf(3) | (Fin(2) & Inf(1))
parity max odd 5: Fin(4) & (Inf(3) | (Fin(2) & Inf(1)))
parity max odd 6: Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & Inf(1))))
parity max odd 7: Fin(6) & (Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & Inf(1)))))

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:

parity max odd 0: t
parity max odd 1: Fin(0) 
parity max odd 2: Inf(1) | Fin(0)
parity max odd 3: Fin(2) & (Inf(1) | Fin(0))
parity max odd 4: Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))
parity max odd 5: Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0))))
parity max odd 6: Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))))
parity max odd 7: Fin(6) & (Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0))))))

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 max/min, odd/even, we get

parity max odd 0: f
parity max even 0: f
parity min odd 0: f
parity min even 0: f

If we take the other semantic, we get

parity max odd 0: t
parity max even 0: t
parity min odd 0: t
parity min even 0: t

I find both unsatisfactory, because they show no duality between odd and even. Switching odd into even in a deterministic parity automaton gives the complement automaton, and I would like it if switching odd into even in a deterministic automaton with parity acceptance (I'm not writing "parity automaton" here!) would give the complement automaton as well. The problem is very obvious in the case 0 shown above, but it also exist in other cases, as pointed out in the last paragraph added by b524fba5.

For this to work, we could decide for instance that max odd means "some acceptance set is visited infinitely often, and the maximum set visited infinitely often is odd", while max even means "no acceptance set is visited infinitely often, or the maximum set visited infinitely often is even". (Or we can switch the first part of this semantic if it matters.) What do you think?

Joachim also suggested adding a property: colored to denote the fact that a state (or transition) belongs to exactly one acceptance set. So a /parity automaton/ would be an automaton with parity acceptance and property: colored. I like this name.

[adl]

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 max case) is as follows: assume that in addition to all the acceptance sets declared in the automaton, there is an imaginary set numbered -1, that contains all the states. Thanks to this -1 set, the maximum number visited infinitely often is now always defined.

This implies that for max odd acceptance, we should accept runs that do not visit any (real) acceptance sets, since they all visit the imaginary acceptance set -1. Conversely, for max even acceptance, we should reject runs that do not visit any (real) acceptance sets.

So that would give the following encodings:

parity max odd 0: t
parity max odd 1: Fin(0) 
parity max odd 2: Inf(1) | Fin(0)
parity max odd 3: Fin(2) & (Inf(1) | Fin(0))
parity max odd 4: Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))

parity max even 0: f
parity max even 1: Inf(0) 
parity max even 2: Fin(1) & Inf(0)
parity max even 3: Inf(2) | (Fin(1) & Inf(0))
parity max even 4: Fin(3) & (Inf(2) | (Fin(1) & Inf(0)))

Notice the perfect duality between max odd and max even.

For the min case, we cannot use this -1 trick, because then the minimum would always be odd. In our case -1 act as a the neutral element for max, and it seems natural to pick the opposite end of the range, i.e., the number of acceptance sets n, as a neutral element for min.

Then, for min even a path that does not visit any set is accepting iff n is even. For min odd a path that does not visit any set is accepting iff n is odd.

This would give the following encodings:

parity min odd 0: f
parity min odd 1: Fin(0) 
parity min odd 2: Fin(0) & Inf(1)
parity min odd 3: Fin(0) & (Inf(1) | Fin(2))
parity min odd 4: Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))

parity min even 0: t
parity min even 1: Inf(0)
parity min even 2: Inf(0) | Inf(1)
parity min even 3: Fin(0) | (Inf(1) & Fin(2))
parity min even 4: Fin(0) | (Inf(1) & (Fin(2) | Inf(3)))

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:

Those canonical encodings for parity acceptance have been chosen so they make sense even in automata where some transitions (or states) may belong to multiple sets or none. In particular if F is set of numbers of the acceptance set numbers visited infinitely often by a run of an automaton with n acceptance sets, we assume that min(∅)=n (resp. max(∅)=-1) for the purpose of deciding whether min(F) (resp. max(F)) is odd or even.

[kleinj]

Thanks, Alexandre, for paraphrasing the email-brainstorming. In a hurry, but I agree, the solution with min(∅)=n (resp. max(∅)=-1) looks like the sanest one, I'd be very happy with that.

[kleinj]

I think in your parity min even conditions there are typos, I think they should be:

parity min even 0: t
parity min even 1: Inf(0)
parity min even 2: Inf(0) |  Fin(1)
parity min even 3: Inf(0) | (Fin(1) &  Inf(2))
parity min even 4: Inf(0) | (Fin(1) & (Inf(2) | Fin(3)))

There is then (as should be expected) quite a nice regular structure and the duality is apparent, as well.

[adl]

@kleinj Yes, thanks. I typed those mistakes by hand.

[strejcek]

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 property: colored is a very rare combination and it does not pay to complicate the format just because of this. But if the duality even in this rare case is so important for you, I'm not going to fight against.

[adl]

@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 acc-name:, we have to be explicit and add a paragraph to discuss that, regardless of the semantic we choose. From a specification point of view, I see no complexity difference in saying "if F is empty then min=n, max=-1" or "paths with empty F are rejected".

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 f and t come from the observation that | and & alternate in the acceptance:

parity min odd 0: f
parity min odd 1: f | Fin(0)      /* the leading f | is just here to justify case 0 */
parity min odd 2: f | (Fin(0) & Inf(1))
parity min odd 3: f | (Fin(0) & (Inf(1) | Fin(2)))
parity min odd 4: f | (Fin(0) & (Inf(1) | (Fin(2) & Inf(3))))

parity min even 0: t
parity min even 1: t & Inf(0)    /* likewise with t & */
parity min even 2: t & (Inf(0) |  Fin(1))
parity min even 3: t & (Inf(0) | (Fin(1) &  Inf(2)))
parity min even 4: t & (Inf(0) | (Fin(1) & (Inf(2) | Fin(3))))

I think anybody looking at these patterns (even without the superfluous f| and t&) should be able to write a function that generate them for any n without even reading the semantics. (There is no need to know that min(∅)=n and max(∅)=-1 unless you want to justify the semantics.) This stuff is simple because it is very regular.

I realize that for the min case I have only shown the proposed encodings, but not the ones suggested by the current text, so here are some acceptance with the "empty F are rejecting" semantic:

parity min odd 0: f
parity min odd 1: f
parity min odd 2: Fin(0) & Inf(1)
parity min odd 3: Fin(0) & Inf(1)
parity min odd 4: Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
parity min odd 5: Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))

parity min even 0: f
parity min even 1: Inf(0)
parity min even 2: Inf(0)
parity min even 3: Inf(0) | (Fin(1) & Inf(2))
parity min even 4: Inf(0) | (Fin(1) & Inf(2))
parity min even 5: Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4))))

The min odd cases are somehow OK, but clearly the min even cases require some explanations. Why is min even 0 equal to f when from the look of grammar it should be t? (We want to stick t& in wrong of all these acceptance formulas to keep alternating | and &.) You need explanations here. I call this more complex and less natural.

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).

[strejcek]

OK, I'm convinced by your argumentation. Let's go for it.

[JanKretinsky]

At first, I had the same opinion as Jan had, but now I don't mind the complications in the corner case, which is not going to appear in practice anyway -> the proposed solution is fine

[adl]

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 min even semantic used in that paper implies that a path that visits no acceptance set should always be rejected, while with our new semantic, it is only the case for min even n when n is odd. (The good news is that if n is not odd, then the set n-1 is useless anyway, so it can be removed to ensure that n is odd.)

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 min even n acceptance, and just replace the acceptance by min even n+1, we are changing the language (the cycles that do not visit any acceptance set will be accepting in one case, and rejecting in the other), and that does not feel very natural. In the max case, adding more useless sets will not change the language. I'm not sure if that is bad and if there is an easy fix; I'm just reporting the remark for the next person willing to think about it.

[strejcek]

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 property: colored: it is not clear from the formulation whether automata combining transition- and state-based acceptance can be colored (I guess they can). But this is definitely not a big issue.