Add Support for Generalized Büchi Automata to Ultimate

[Heizmann]

Yong and Yu-Fang are going to implement generalized Büchi automata in Ultimate.

The question is now how this should be done. Currently, I see three possibilities.

1. Extend our existing interfaces INwaOutgoingLetterAndTransitionProvider (or INwaBasis or INestedWordAutomaton) by a new acceptance condition. The method for the classical acceptance condition boolean isFinal(STATE state) has to throw an UnsupportedOperationException.
2. Parameterize all our automata by an acceptance condition.
3. Remove the acceptance condition from all our interfaces and introduce two additional versions of each interface. One that has the classical acceptance condition and one that has the acceptance condition of generalized Büchi automata.

[danieldietsch]

How does the automata library currently handle the difference between Büchi automata and finite automata?

EDIT: To be precise, I am getting at the following. If a change is needed because of the different types of the acceptance condition (sets of sets vs. sets) we should chose a change that does not obscure this. If we would use (3), i.e., new interfaces, it may look strange for a potential user because he/she might expect that this is due to different semantics and not just for technical reasons. Without thinking too much, I would favour (1) and add the exception for methods that do not support sets (perhaps even going so far as not throwing exceptions for singleton sets).

[schillic]

There are different operations that interpret the automaton in a different way (such as IsEmpty and BuchiIsEmpty). The user is responsible for calling the correct operation.

[Heizmann]

Some more thoughts:

• It is probably safe to go for Possibility 1 (above) because we can change that later.
• We should probably think about how we can make the NestedWordAutomaton (resp. NestedWordAutomatonCache) class more modular. As a first step you can just extend it.
• I would prefer to have a list (and not a set) of accepting sets. Then our on-demand construction can ask a state about its acceptance and it can return a set of integers.
• It seems to me that our algorithm for the removal of non-live states can be relatively easy adapted to generalized Büchi automata.
• It seems that for an emptiness check that also returns a counterexample it is not that easy if the counterexample should be small. We would need an algorithm that find a short route through the accepting SCC that visits a state of each set (NP-hard?)

[danieldietsch]

@Heizmann : I also think that shortest path through SCC which visits every node at least once is NP-hard (reduction to finding a hamilton path). But there exist usable approximations that are polynomial and produce -- I believe -- sufficiently short paths.

[Heizmann]

@danieldietsch I agree. But please note that this is currently only a minor problem. @duckly and @guluchen are going to implement an algorithm that implicitly checks emptiness while computing the difference of a generalized Büchi automaton and a module (aka Büchi interpolant automaton). For practical applications (termination analysis) we need the standalone emptiness check only for debugging.

[schillic]

@danieldietsch @Heizmann: I don't see how you can reduce from the Hamiltonian path problem. However, your intuition is correct: The problem is NP-hard. https://doi.org/10.1007/978-3-642-13089-2_22

Note that there is no efficient approximation algorithm.

[danieldietsch]

@Heizmann : ok @schillic: cool that you found something about it.

[guluchen]

Hi, from the discussion, it seems that option 1 is the current decision. But we still need to decide which one to extend. I guess maybe INwaOutgoingLetterAndTransitionProvider since it is the subclass of the other two so should have less impact to other parts of the programs.

[liyong31]

My idea is to add an interfance IGeneralizedNwaOutgoingLetterAndTransitionProvider which extends INwaOutgoingLetterAndTransitionProvider in the following:

1. int getAcceptanceSize(); to get the number of acceptance sets

2. boolean isFinal(STATE state, int i); to check whether state is in the i-th set of generalized acceptance

3. Set<Integer> getAcceptanceSet(STATE state); to get the labels (the index of acceptance set) of state.

4. overrides boolean isFinal(final STATE state) { throw new UnsupportedOperationException("Generalized Buchi automata donot support isFinal operation"); }

It is easy to add a class GeneralizedBuchiIntersectNwa which has two kinds of operands, namely the first operand is an instance of IGeneralizedNwaOutgoingLetterAndTransitionProvider and the second operand is an instance of INwaOutgoingLetterAndTransitionProvider.

The remaining problem is I should also create some class, say GeneralizedAcceptingComponentsAnalysis like AcceptingComponentsAnalysis to get the possible accepting run and word from generalized Buchi automata.

[danieldietsch]

Perhaps a naive question: Why not boolean isInAcceptanceSet(STATE state) and Set<Set<STATE>> getAcceptanceSets(STATE state)?

• You get the empty set if state does not belong to any accepting set
• You get the accepting sets if state belongs to some accepting sets

[schillic]

Why not boolean isInAcceptanceSet(STATE state)

Because you want to know this for a fixed set. The information "is in some acceptance set" is not interesting (at least I do not see an application).

Indeed, in generalized Buchi automata, knowing a state is in some acceptance set is not very helpful.

[Heizmann]

@duckly I think what you propose makes sense.

The question about AcceptingComponentsAnalysis is difficult. This class provides its information for two purposes. 1. Removal of non-live states 2. Provides information for an emptiness check.

A bunch of comments

1. Effectively, we are not doing an emptiness check at the beginning of an iteration of our termination analysis. We just readout the information from the non-live state analysis (I forgot this in our discussions via Skype)
2. This class is horrible. It looks like I never finished it. I am absolutely fine with refactoring it.
3. Refactoring this class id dangerous. I think I remember some bugs that only occurred on very few examples.
4. Maybe NestedWordAutomatonReachableStates should be parameterized with an AcceptingComponentsAnalysis.
5. For NWAs, the AcceptingComponentsAnalysis relies on the AcceptingSummariesComputation. The AcceptingSummariesComputation uses fields of the StateContainer for its computation. For the gerneralized automata these fields are not sufficient. We should not add more fields because the memory consumption of these objects is critical. We could extend this class to a special StateContainer for generalized NWAs or (maybe better) store the information that is needed additionally in a map.
6. Generalized NWAs are very intricate. Maybe a paper for itself.

[liyong31]

@danieldietsch I am sorry to have deleted your comments accidentally (I tried to make my answer be in a better form) If I remember correctly you propose to use function List<Set<STATE>> getAcceptance(STATE state). Actually we could have a function like List<Set<STATE>> getAcceptance() to get the list of acceptance set of states from a generalized Buchi automata. Any accepting run should visit at least one state of each acceptance set in the list and checking that by function Set<Integer> getAcceptanceSet(STATE state) is very convenient