multiple transitions with same source/label/destination, but different acceptance

[adl]

If we ignore alternation, the semantic we give for omega automata with transition-based acceptance assume that the set of transitions and the acceptance sets are subsets of Q*B(AP)*Q where B(AP) is the set of Boolean functions. However our syntax allows automata that cannot easily fit into this constraint.

Consider this:

/* ... */
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0) & Inf(1)
--BODY--
State: 0
[0] 0 {0}
[0] 0 {1}
--END--

this declare two transitions (0)-a->(0), each of them in a different acceptance set. But our semantics do not support distinguishing these transitions. Of course we could interpret this situation as a single transition that belongs to both sets: indeed if one of these transitions appear infinitely often in a run, the other transition can be used infinitely often as well. So this automaton is equivalent to the following:

/* ... */
Start: 0
AP: 1 "a"
Acceptance: 2 Inf(0) & Inf(1)
--BODY--
State: 0
[0] 0 {0 1}
--END--

(Shameless plug: Spot's autfilt --merge-transitions will do this simplification if you need it.) However this reduction is only correct because we are using Inf acceptance. For instance consider again the first automaton, but negating the acceptance condition:

/* ... */
Start: 0
AP: 1 "a"
Acceptance: 2 Fin(0) | Fin(1)
--BODY--
State: 0
[0] 0 {0}
[0] 0 {1}
--END--

The above non-deterministic automaton is accepting since we can decide to stop using one of the two transitions at some point. We cannot consider the two transitions as being a single transition that belongs to both sets, otherwise the automaton would be non-accepting. If fact, because the sets are Fin-accepting, we could declare the (0)-a->(0) transition in their intersection if we want to avoid duplicate transitions.

Using intersection of Fin sets, and union for Inf sets fail when the same set number is used both with Fin and Inf. Consider for instance the same automaton with:

Acceptance: 2 (Fin(0)&Inf(1)) | (Inf(0)&Fin(1))    /* = Inf(0) xor Inf(1) */

I believe we have to change the semantics to support duplicate transitions in different acceptance sets to ensure that they work for any automaton we can represent with HOAF.

Here are two ideas for a possible fix:

• Change Q*B(AP)*Q to something like Q*B(AP)*2^F*Q where F is a set of /acceptance numbers/. Then change the acceptance of a run to extract the set of acceptance numbers seen infinitely often and make sure this set is compatible with the acceptance formula.
• Change Q*B(AB)*Q to something like Q*B(AB)*N*Q where N are just natural numbers to allow us to duplicate transitions, but are not used for any other purpose. In this case F can remain a set of subsets of transitions.

I like the second option better because it still makes it clear we think in terms of acceptance sets of transitions.

[strejcek]

Wow, very interesting bug indeed. (Nice catch.)

I can see one more solution: we can replace the set of transitions, which is a subset of Q*B(AP)*Q, by a multiset of transitions, where each transition is an element of Q*B(AP)*Q. With this solution, no other changes in the definitions are needed. Or not? I like it more than introducing artificial transition numberings by Q*B(AP)*N*Q.

[adl]

@strejcek I don't get the multiset idea. If R={(0,a,0),(0,a,0)} contains (0,a,0) twice, how to you define the acceptance sets to refer to specific copies of a transition?

[strejcek]

OK, I have to change F a bit: instead of defining F as a set of sets of transitions, I define it as a function assigning to each element of the multiset of transitions a set of naturel numbers (meaning to which acceptance sets the transition belongs).

Hmm, it is probably not as elegant as it seemed to be during the last night.

[adl]

My proposal is in commit d83e171. Let me know what you think.

In particular, distinguishing transitions is not a problem with state-based acceptance, so I've opted to keep the definition of R as a set of triplets. It this OK? This creates a new difference between the transition-based and state-based semantics that I am not very fond of. It is not just the definition of S that is different, but now also the definition of R. Because R is different, one could also argue that the interpretation of the run should be redefined. Do we really want that, or can we agree that it is easy to infer from the previous definition?

The other option is to keep R as a set of quadruplets, but then someone reading only this semantic will wonder what is the purpose of this unused n.

Also, do we need an example to illustate this subteltly? Another option is to simply link to this issue when we define n.

[JanKretinsky]

I'm fine with having simpler semantics for state-based acceptance, but then the simpler case should be presented first and the more complex (with N) only later and together with an example.

[adl]

Joachim told me (privately) that he favored Q*B(AP)*2^F*Q, because it better matches how we declare transitions in the format. The disadvantage I see here is that we cannot declare F as a set of sets of transitions, which seems odd if F is a set of sets of states in the state-based semantics.

I would like to make a third proposal in that direction.

Let m be the number of acceptance sets, and let [m] denote {0,1,...,m-1}.

We set R = Q*B(AP)*2^[m]*Q. This clearly matches the way we declare transitions in the format too. Then we define F={F_0,F_1,F_{m-1}} where F_i = { (s,l,M,d) ∈ R | i ∈ M }. Then F is a set of sets of transitions and those can easily be matched against the transitions that occur infinitely or finitely in a run as we already do.

[strejcek]

I like the proposal!

[kleinj]

I agree, that's a very good idea, giving us a clean formalism that easily maps to the format. Thanks, Alexandre!

[adl]

Can someone proof-read commit 3796273?
(Please ignore d0f1e1d and 8197315 listed above, these are earlier attempts superceeded by 3796273.)