Complementation

This page shows how to use ROLL to complement a given Büchi automaton. Suppose the given input Büchi automaton is described in Hanoi format as follows.

HOA: v1
tool: "ROLL"
properties: explicit-labels state-acc trans-labels 
States: 2
Start: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
AP: 1 "b"
--BODY--
State: 0
  [!0] 0
  [0] 0
  [0] 1
State: 1 {0}
  [0] 1
--END--

This Büchi automaton is the smallest automaton recognizing the language specified by the LTL formula “F (G b)”.

As an example, one can use following command line to complement the given automaton.

java -jar ROLL.jar complement A.hoa -table -syntactic

It will give us a complement automaton described in the Hanoi format as follows.

HOA: v1
tool: "ROLL"
properties: explicit-labels state-acc trans-labels 
States: 4
Start: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
AP: 1 "b"
--BODY--
State: 0
[(!0)]  0
[(!0)]  1
[(!0)]  2
[(0)]  0
[(0)]  3
State: 1
[(!0)]  1
[(!0)]  2
[(0)]  1
[(0)]  2
State: 2 {0}
[(!0)]  1
[(0)]  3
State: 3
[(!0)]  1
[(!0)]  2
[(0)]  3
--END--

The complete log information is the following.

2018/11/12 14:46:35 [ info] ROLL for BA complementation...
HOA: v1
tool: "ROLL"
properties: explicit-labels state-acc trans-labels 
States: 2
Start: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
AP: 1 "b"
--BODY--
State: 0
[(!0)]  0
[(0)]  0
[(0)]  1
State: 1 {0}
[(0)]  1
--END--
HOA: v1
tool: "ROLL"
properties: explicit-labels state-acc trans-labels 
States: 4
Start: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
AP: 1 "b"
--BODY--
State: 0
[(!0)]  0
[(!0)]  1
[(!0)]  2
[(0)]  0
[(0)]  3
State: 1
[(!0)]  1
[(!0)]  2
[(0)]  1
[(0)]  2
State: 2 {0}
[(!0)]  1
[(0)]  3
State: 3
[(!0)]  1
[(!0)]  2
[(0)]  3
--END--
  #LT = 2                            // #number of letters
  #T.S = 2                           // #states of target
  #T.T = 4                           // #transitions of target
  #H.S = 4                           // #states of learned automaton
  #H.T = 14                          // #transitions of learned automaton
  #L.S = 1                           // #states of leading automaton or L$
  #P.S = [2, ]                       // #states of each progress automaton
  #F.S = 3                           // #L.S + #P.S
  #MQ = 4                            // #membership query
  #EQ = 1                            // #equivalence query
  #TMQ = 3 (ms)                      // time for membership queries
  #TEQ = 34 (ms)                     // time for equivalence queries
  #TLEQ = 34 (ms)                    // time for the last equivalence query
  #TTR = 0 (ms)                      // time for the translator
  #TLR = 16 (ms)                     // time for the learner
  #TLRL = 5 (ms)                     // time for the learning leading automaton
  #TLRP = 5 (ms)                     // time for the learning progress automata
  #TTO = 147 (ms)                    // total time for learning Buchi automata

Return to How to Use ROLL in Command Line.