Class NbaDet


  • public final class NbaDet
    extends Object
    This class provides a conversion from non-deterministic Büchi automata into deterministic parity automata. It is based on the following two papers: https://doi.org/10.4230/LIPIcs.ICALP.2019.120 https://doi.org/10.1007/978-3-030-31784-3_18
    • Method Detail

      • main

        public static void main​(String... args)
                         throws IOException
        Entry point for nbadet tool.
        Parameters:
        args - arguments from environment
        Throws:
        IOException - on failure to parse the input file
      • restoreLogLevel

        public static void restoreLogLevel​(Map<Handler,​Level> oldLogLevels)
      • determinizeNbaTopo

        public static <S> Automaton<Pair<Integer,​NbaDetState<S>>,​ParityAcceptance> determinizeNbaTopo​(NbaDetConf<S> conf)
        Determinize automaton, utilizing "topological" optimization, i.e. determinize each SCC of the powerset structure of the NBA separately and prune the partial DPAs (keep one bottom SCC of the partial DPAs).
        Parameters:
        conf - prepared determinization config (which includes the input NBA)
        Returns:
        resulting DPA
      • determinizeNbaAlongScc

        public static <S> Pair<Automaton<NbaDetState<S>,​ParityAcceptance>,​Map<BitSet,​NbaDetState<S>>> determinizeNbaAlongScc​(Automaton<BitSet,​?> refScc,
                                                                                                                                               NbaDetConf<S> conf)
        Determinize provided NBA partially, while not leaving some automaton refScc. Returns partial DPA and a mapping from all reference states to some representative DPA state. refScc should be some kind of powerset SCC (i.e. deterministic structure) of the NBA. The exploration starts from the unique initial state of that powerset SCC automaton.
      • createPowerSetAutomaton

        public static <S> Automaton<BitSet,​AllAcceptance> createPowerSetAutomaton​(NbaAdjMat<S> adjMat)
        Create a powerset automaton of NBA where state sets are represented by BitSets.
        Type Parameters:
        S - state type of underlying NBA
        Parameters:
        adjMat - BitSet-based transitions for underlying NBA
        Returns:
        the resulting powerset automaton