Buechi Automata & Rabin Automata
DBW deterministic Buchi automata
NBW non-deterministic Buchi automata
DRW Rabin automata
DGBW deterministic generalized Buchi automata
NGBW nondeterministic generalized Buchi automata
Working:
RW2BW: Rabin to Buchin automaton
BW2DRW: Buchin to deterministic Rabin automata
LTL2A
minimal Buchi: Buchi -> Rabin -> deterministic Rabin -> minimal Rabin -> Buchi (minimal ??)
| > |
Simple Example
| > | M_imp:=mkNBW({q0,q1,q2},{a,b,c},table([(q0,a)={q2}, (q0,b)={q1}, (q1,a)={q0}, (q1,b)={q2}, (q2,c)={q2}]),q0,{q1,q2}):
M_spec:=mkDBW({Q0,Q1},{a,b,c},table([(Q0,a)=Q0, (Q0,b)=Q0, (Q0,c)=Q1, (Q1,a)=Q1, (Q1,b)=Q1, (Q1,c)=Q1]),Q0,{Q1}): transitionGraph(M_imp); limNBW(M_imp); transitionGraph(M_spec); limNBW(M_spec); |
 |
 |
 |
 |
| > | nbw:=intersectNBW(M_imp,complementDBW(M_spec)):
transitionGraph(nbw); |
 |
| > | isEmptyNBW(nbw); |
 |
(18.1.1) |
| > | limNBW(nbw); |
![{{[q2, [q1, 0], 2]}, {[q0, [q0, 0], 2], [q1, [q0, 0], 2]}, {[q1, [q0, 1], 1], [q0, [q0, 1], 2]}}](images/FOLA-demo_2586.gif){kind=small} |
(18.1.2) |
First Example
| > |
Second Example
| > |
Complement of DBW
| > |
Minimization of DBW
Weak DBW
| > |
| > | nbw1:=randomNBW(6,[0,1],2):
nbw2:=randomNBW(6,[0,1],2): while isEmptyNBW(intersectNBW(nbw1,nbw2)) do nbw1:=randomNBW(6,[0,1],2); nbw2:=randomNBW(6,[0,1],2); od: reachableNBW(nbw1); reachableNBW(nbw2); |
   |
(18.1) |
   |
(18.1) |
| > |