complement
This is an old revision of the document!
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 to recognize the language specified by the LTL formula “F G b”.
The complete log information is the following.
2018/11/12 14:41:08 [ 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 = 5 (ms) // time for membership queries #TEQ = 48 (ms) // time for equivalence queries #TLEQ = 48 (ms) // time for the last equivalence query #TTR = 0 (ms) // time for the translator #TLR = 24 (ms) // time for the learner #TLRL = 7 (ms) // time for the learning leading automaton #TLRP = 7 (ms) // time for the learning progress automata #TTO = 332 (ms) // total time for learning Buchi automata
complement.1542005132.txt.gz · Last modified: 2018/11/12 14:45 by liyong