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

Closed
adl opened this Issue Feb 28, 2015 · 9 comments

Comments

Projects
None yet
4 participants
@adl
Owner

adl commented Feb 28, 2015

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.

@adl adl added the bug label Feb 28, 2015

@strejcek

This comment has been minimized.

Show comment
Hide comment
@strejcek

strejcek Mar 5, 2015

Collaborator

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.

Collaborator

strejcek commented Mar 5, 2015

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

This comment has been minimized.

Show comment
Hide comment
@adl

adl Mar 6, 2015

Owner

@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?

Owner

adl commented Mar 6, 2015

@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

This comment has been minimized.

Show comment
Hide comment
@strejcek

strejcek Mar 6, 2015

Collaborator

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.

Collaborator

strejcek commented Mar 6, 2015

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

This comment has been minimized.

Show comment
Hide comment
@adl

adl Mar 7, 2015

Owner

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.

Owner

adl commented Mar 7, 2015

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

This comment has been minimized.

Show comment
Hide comment
@JanKretinsky

JanKretinsky Mar 7, 2015

Collaborator

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.

Collaborator

JanKretinsky commented Mar 7, 2015

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

This comment has been minimized.

Show comment
Hide comment
@adl

adl Apr 16, 2015

Owner

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.

Owner

adl commented Apr 16, 2015

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

This comment has been minimized.

Show comment
Hide comment
@strejcek

strejcek Apr 16, 2015

Collaborator

I like the proposal!

Collaborator

strejcek commented Apr 16, 2015

I like the proposal!

@kleinj

This comment has been minimized.

Show comment
Hide comment
@kleinj

kleinj Apr 16, 2015

Collaborator

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

Collaborator

kleinj commented Apr 16, 2015

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

adl added a commit that referenced this issue Apr 16, 2015

deal with duplicate transition in different accepting sets
In the semantics, distinguish transitions with identical src/label/dst
but belonging to difference acceptance sets.  This fixes #38.

adl added a commit that referenced this issue Apr 16, 2015

deal with duplicate transition in different accepting sets
In the semantics, distinguish transitions with identical src/label/dst
but belonging to difference acceptance sets.  This fixes #38.
@adl

This comment has been minimized.

Show comment
Hide comment
@adl

adl Apr 16, 2015

Owner

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

Owner

adl commented Apr 16, 2015

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

@adl adl closed this in 3796273 Apr 17, 2015

adl added a commit that referenced this issue Apr 17, 2015

@adl adl referenced this issue Jan 6, 2016

Closed

Edges or transitions? #57

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment