State-based versus transition-based acceptance

[adl]

The format currently allow both states and transitions to be put into acceptance sets, and those acceptance sets can be complemented in the acceptance condition.

We need to make the semantics crystal clear as one may wonder what is the complement of a set that contains states and transitions...

The mathematical view is that we have only acceptance sets of transitions. We then pretend that a state belongs to the acceptance set S iff all its outgoing transitions belong to S. In this view, the syntax

State: 1 {2}
  [0] 2
  [!0] 1

is just syntactic sugar for

State: 1
  [0] 2 {2}
  [!0] 1 {2}

When a complement is considered in the acceptance conditions, it is with respect to all the transitions. However since if the automaton is only using state-based acceptance, it would be equivalent to make to complement with respect to the states.

We should probably also mention that our support for a mix of state-based or transition-based acceptance is inspired from the format of LBTT.

[adl]

Another related point: acceptance sets should either be ignored or disallowed on states without transitions.

The reason is that if we apply the suggested equivalence:

a state belongs to the acceptance set S iff all its outgoing transitions belong to S

then a state without outgoing transitions belongs to any acceptance set. However in practice such a membership is useless since the state is never going to support an infinite run.

[xblahoud]

Another related point: acceptance sets should either be ignored or disallowed on states without transitions.

I suggest to ignore it. And then using the suggested equivalence all works fine.

[adl]

Commit 8b3a80b shows my attempt at formalizing this. I have probably failed at being concise. Let me know what you think.

The definition of automata would need to be edited to support alternation when #2 is merged, but I'd prefer to merge this change first.

[strejcek]

I comment the side issue about acceptance of states without any outgoing edge first: in general, our police is to be restrictive only when necessary. And in this case, it is clearly not the case. So I would admit acceptance sets on arbitrary states. Moreover, I would not even say that we ignore some acceptance sets on some states. The point of the format is to establish a notation for automata with clear interpretation. Our goal is not to say "how to make an automaton to get a complement of the original language".

And now to the relation between acceptance on states and transitions:

a state belongs to the acceptance set S iff all its outgoing transitions belong to S

I do not like the "iff". Clearly, we can also have

State: 1 {2}
  [0] 2 
  [!0] 1 {2}

So the "iff" clearly does not hold. I see basically two solutions

1. Define a formalism that uses both accepting states and transitions at the same time (it should be easy and I prefer this solution). We should mention that it is very easy to translate it into pure transition-based acceptance.
2. Clearly state that the underlying formalism is a transition-based automaton and that an accepting state is just a syntactic sugar saying that all its outgoing transitions are in the corresponding acceptance set. We should also mention that if one uses only acceptance on states, than the underlying transition-based automaton accepts the same as the original automaton seen as a state-based.

[adl]

Jan, did you look at the proposed commit 8b3a80b ? (Where it seems I took your solution 2, and where I don't think I used iff.) It might help to comment and suggest modifications to some of these changes directly, unless you think this is completely off.

I'm not sure I understand your comment about complementation. Explaining how to complement the acceptance condition of an automaton is indeed out of scope. The complementation issue we have is that our definition of acceptance condition allow acceptance sets to be complemented.

[strejcek]

Yes, removing the parenthesis should help.

And yes, I've read commit 8b3a80b completely - it contains the following "iff" sentence:

In some way, we can consider a state to belong to Sᵢ iff all its outgoing transitions belong to Sᵢ.

Anyway, it seems that my brain was in a weekend-mode today in the morning (You are right, I was completely lost in the complementation). Sorry for that.

Thinking about it once again, my first solution (both accepting states and transitions) can work reasonably only if we forbid complementation of acceptance sets. If we want to keep it, the solution 2 is much more reasonable indeed.

The only disadvantage of the second solution is that presenting all automata as transition-based could discourage some (state-based thinking) people from using our format. We should really take care of the presentation to prevent this.

BTW: there is a typo in 8b3a80b: complented -> complemented

[xblahoud]

Moreover, I would not even say that we ignore some acceptance sets on some states

The problem is that such states then are in every acceptance set and also in every complement of the acceptance sets. So we may mention that we can ignore this inconsistency because the states cannot appear in any infinite run.

[xblahoud]

Overall I think the formalization is done well. As Jan mentioned, we have to be careful in explanation of why we use transition-based automata only.

[strejcek]

The problem is that such states then are in every acceptance set and also in every complement of the acceptance sets.

If you look at accepting states as syntactic sugar, that complement of an acceptance set cannot contain any state at all (the official model is transition-based automaton).

[adl]

The problem is that such states then are in every acceptance set and also in every complement of the acceptance sets.

If you look at accepting states as syntactic sugar, that complement of an acceptance set cannot contain any state at all (the official model is transition-based automaton).

The official model is transition-based, so in a state-based input the following two states

State: 1 {1}
/* no transition */
State: 2
/* no transition */

would both have the same transition-based interpretation, silently ignoring the (useless) acceptance of state 1 since there is no transition to carry it. So far so good. The problem is if we try to explain to people using state-based automata that our transition-based semantics is just a device to generalize the format to both transition-based and state-based automata, but that if they use only state-based automata it's equivalent to work with acceptance sets of states. With our semantics there is no way to encode the membership of a dead state to some acceptance set.

This is mainly a problem with the sentence

In some way, we can consider a state to belong to Sᵢ iff all its outgoing transitions belong to Sᵢ.

which we have to reword anyway. With this equivalence all dead states necessarily belong to all acceptance sets, since all their 0 outgoing transitions are accepting.

I think we should change the wording to specify only the transition-based semantics, explain that the syntax for state-based acceptance is syntactic sugar, and have a whole section discussing the use of the format in a state-based acceptance context. Fortunately, the fact is that a transition-based tool and a state-based tool would handle acceptance of dead state differently has no impact on to semantics of omega automata.

BTW, I noticed that "support for transition-based acceptance" is missing from the list of goals of the format.

[strejcek]

The problem is if we try to explain to people using state-based automata that our transition-based semantics is just a device to generalize the format to both transition-based and state-based automata, but that if they use only state-based automata it's equivalent to work with acceptance sets of states.

OK, let's define the semantics twice: one for automata with pure state-based acceptance (where the formal model will be also state-based) and second for all other automata (where the formal model will be purely transition-based). We can mention that these two are equivalent (with a little insignificant formal difference in acceptance of terminal states).

[adl]

Commit 9da522e is my new proposal, with the state-based semantics discussed at the end of the document.