ε-labelled transitions

[sickert]

For my construction I need to output an ω-automaton with ε-transitions and I want to use the HOA format. Unfortunately the specification does not mention ε-transitions explicitly and now I'm wondering how to properly do it. I talked to @JanKretinsky in person, but he was also unsure how to do it. It would be great, if the specification either explains why ε-transitions are not supported or how to express them.

[kleinj]

This is a good point, we had not considered ε-transitions before. Just so we are talking about the same thing, you mean the usual "silent" transitions that can be taken without reading a letter, right?

One option would be for us to add explicit support in the upcoming 1.1 version. Possible syntax might be

State: 0
[] 1
[epsilon] 1
epsilon 1

This would make the definition of the automaton semantics a bit more complicated, but we could probably first describe the usual semantics and provide a "specialization" in the presence of ε-transitions. We'd also have to be careful how to handle ε-divergence, i.e., runs consisting eventually only of epsilon transitions, which should probably be rejecting.

I haven't thought about it too deeply, but I guess the standard ε-removal would be compatible with our acceptance definition, i.e., just gather all the acceptance sets that are seen on the invisible edges/states and add them to the visible edge.

Another way, without having explicit support would be the following encoding:

HOA: v1
AP: 3 "a" "b" "epsilon"
Epsilon: 2     /* mark AP 2 as epsilon */
Alias: @epsilon 2 & !1 & !0
...
---BODY---
[0&1]  ....
[@epsilon] ...
---END---

The Epsilon header, as it starts with an upper case letter, should inhibit other tools that don't know about the epsilon-semantics from working with such an automaton. On the other hand, you could recognize this and perform the correct conversions. In an alphabet-based setting, a similar encoding would work.

If I remember correctly, for jhoafparser there should be a mechanism to tell the parser to accept such non-standard, semantic-changing headers. But as the format is still quite fresh, it's probably not yet thoroughly tested. E.g., which parts actually care about the semantics and which can just pass along everything.

[adl]

Regarding a possible introduction in 1.1, I'd suggest using e as a third constant, just like we have t or f for true and false. That would allow transitions labeled by [e] but also [e | 0&1].

I think the hard part would indeed be to update all the semantics and automata properties.

[adl]

Hmmm... but [e&0] would not make any sense. Maybe it's best to force epsilon transitions to be listed by themselves, in which case Joachim's [] seems fine to me.

[sickert]

This is a good point, we had not considered ε-transitions before. Just so we are talking about the same thing, you mean the usual "silent" transitions that can be taken without reading a letter, right?

Yes, same thing. :)

I think [] looks like the best option. [e] may be already taken by issue #20.

[JanKretinsky]

I like the [ ] syntax

[kleinj]

Good point, Alexandre, I hadn't thought about the properties.

I guess there are two views of such automata, i.e., the "as is" view where the epsilon transitions are simply treated as normal transitions (for the structural properties such as state-acc...) and the "collapsed" view, where the epsilon transitions have been collapsed. E.g., a state might be viewed as "complete" in the later if some epsilon successor provides the missing transition labels. Mmmh, tricky.

[adl]

Note that a generalization of this would be to think directly in term of translations labeled by (finite) words. I.e., instead of choosing labels in an alphabet A, or in A∪{ε}, we choose them in A*.

For instance, using ; for concatenation [0&1; 0&!1; !0&1] could be a label that matches a 3-letter word, and [] is naturally the empty word.

This can probably wait until someone needs it, but it might help to think about the definition of the properties in this context.

[strejcek]

Does it pay to support epsilon-transitions? (Especially considering that their elimination does not add any single state.) Their support would make the format more complex: besides mentioned complications in semantics and properties, we should also decide whether/how to support these transitions in implicitly labelled transitions.

If we decide to support it, I vote for [] notation (in explicit labels).

For properties and semantics, I suggest to present it as a syntactic sugar: describe the procedure that eliminates epsilon-transitions and say that the automaton is formally seen as the one after this elimination.

Regarding Alexandre's suggestion for word-labelled transitions: maybe we should directly jump to transitions labelled by regular expressions. (Seriously.)

[adl]

Has any of you encountered alternating automata with ε-transitions? Is there some literature about it?

Removal of ε-transitions in alternating automata sounds like something tricky to define because existential and universal ε-transitions can be chained. Is the following correct?

What if the input automaton does not include state 3? The result would have no valid successor for 0?

Note that in existential automata we can remove ε-transitions by doing either a forward or a backward closure. It does not seem we have that choice for alternating automata.

[sickert]

Does it pay to support epsilon-transitions? (Especially considering that their elimination does not add any single state.) Their support would make the format more complex: besides mentioned complications in semantics and properties, we should also decide whether/how to support these transitions in implicitly labelled transitions.

In my particular case, I use it to separate the initial and accepting components/parts of an limit-deterministic automaton and later make use of this to reduce the number of additional transitions I have to create during the build of a product by propagating the ε.

[sickert]

Has any of you encountered alternating automata with ε-transitions? Is there some literature about it?

This may be a bit far of, but in the context of Alternating timed automata adding ε-transitions makes some things undecidable.

[strejcek]

I haven't met any alternating automaton with ε-transitions so far. But I think that if we want to support ε-transitions, then we should support them also in alternating automata.

I agree that removing the ε-transitions from alternating automaton is a bit tricky, but I think that it can be done. I found Alexandre's example correct. And yes, if there is no state 3, then the resulting automaton has no successor of state 0.

If we agree that looking at ε-transitions as a syntactic sugar is the right way to go, I can write down the formal transformation to include it in the format description.

Anyway, we should more forward to v1.1.

[xblahoud]

My point of view is similar to Jan's. I thing ε-transitions should be treated as syntactic sugar and this is because a situation when there is a cycle of ε-transitions and some such transitions has some acceptance mark (what would be the semantics in the infinite world anyway?). Further, if we support it, we should define it for alternating automata too.