IA159 Formal Verification Methods
LTLBA via Alternating 1-Weak BA
Jan Strejˇcek
Department of Computer Science
Faculty of Informatics
Masaryk University
Focus and sources
Focus
alternating 1-weak Büchi automata (A1W)
translation LTLA1W
translation A1WBA
Source
M. Y. Vardi: An Automata-Theoretic Approach to Linear
Temporal Logic, LNCS 1043, Springer, 1995.
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 2/30
LTLBA translations in general
applications in automata-based LTL model checking,
vacuity checking (checks trivial validity of a specification
formula), . . .
two LTLBA translations
LTL  generalized Büchi automata  BA
LTL  alternating 1-weak Büchi automata  BA
the latter translation is more popular
size-reducing optimizations of alternating 1-weak BA
produces smaller BA (in some cases)
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 3/30
LTLBA via alternating 1-weak BA
Alternating Büchi automata
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 4/30
Positive boolean formulae
Positive boolean formulae over set Q (B+(Q)) are defined as
 ::= |  | q | 1  2 | 1  2
where stands for true,  stands for false, and q ranges
over Q.
S  Q is a model of   the valuation assigning true just
to elements of S satisfies 
S is a minimal model of   S is a model of  and no proper
(written S |= ) subset of S is a model of 
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 5/30
Examples of positive boolean formulae
formulae of B+({p, q, r}) (minimal) models
 no model
, {p}, {q}, {r}, {p, q}, . . .
p  q {p, q}, {p, q, r}
p  (q  r) {p}, {p, q}, {p, r}, {q, r}, {p, q, r}
p  (q  r) {p, q}, {p, r}, {p, q, r}
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 6/30
Examples of positive boolean formulae
formulae of B+({p, q, r}) (minimal) models
 no model
, {p}, {q}, {r}, {p, q}, . . .
p  q {p, q}, {p, q, r}
p  (q  r) {p}, {p, q}, {p, r}, {q, r}, {p, q, r}
p  (q  r) {p, q}, {p, r}, {p, q, r}
minimal models = clauses in disjunctive normal form
 
S|=
(
pS
p)
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 7/30
Alternating Büchi automata
An alternating Büchi automaton is a tuple A = (, Q, , q0, F),
where
 is a finite alphabet,
Q is a finite set of states,
 : Q ×   B+(Q) is a transition function,
q0  Q is an initial state,
F  Q is a set of accepting states.
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 8/30
Trees
A tree is a set T  N
0 such that if xc  T, where x  N
0 and
c  N0, then also
x  T and
xc  T for all 0  c < c.

yyyyy
HHHHHH
SSSSSSSSSSSS
0
{{{{{ 1 2
xxxxx
FFFFF 3
00 01 20 21 22
210
T = { , 0, 1, 2, 3,
00, 01, 20,
21, 22, 210 }
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 9/30
Trees
A tree is a set T  N
0 such that if xc  T, where x  N
0 and
c  N0, then also
x  T and
xc  T for all 0  c < c.

yyyyy
HHHHHH
SSSSSSSSSSSS
0
{{{{{ 1 2
xxxxx
FFFFF 3
00 01 20 21 22
210
T = { , 0, 1, 2, 3,
00, 01, 20,
21, 22, 210 }
A Q-labeled tree is a pair (T, r) of a tree T and a labeling
function r : T  Q.
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 10/30
Alternating Büchi automata: a run
A run of an alternating BA A = (, Q, , q0, F) on word
w = w(0)w(1) . . .   is a Q-labeled tree (T, r) such that
r() = q0 and
for each x  T: {r(xc) | c  N0, xc  T} |= (r(x), w(|x|)).
A run (T, r) is accepting iff for each infinite path  in T it holds
that Inf()  F = , where Inf() is the set of all labels
(i.e. states) appearing on  infinitely often.
An automaton A accepts a word w iff there is an accepting run
of A on w. We set
L(A) = {w  
| A accepts w}.
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 11/30
Example of an alternating Büchi automaton
m
l
m
l
n
q3
q2
p
q1
n
n
l
m
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 12/30
Example of an alternating Büchi automaton
m
l
m
l
n
q3
q2
p
q1
n
n
l
m
Accepts the language lm(l + m + n)n.
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 13/30
Alternating 1-weak Büchi automata (A1W)
Let A = (, Q, , q0, F) be an alternating BA. For each p  Q
we define the set of all successors of p as
Succ(p) = {q | l  , S  Q : S  {q} |= (p, l)}.
Automaton A is 1-weak (or linear or very weak) if there exists
a partial order  on Q such that for all p, q  Q it holds:
q  Succ(p) = q  p
alternating 1-weak Büchi automaton = A1W automaton
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 14/30
Notes
standard Büchi automata are alternating Büchi automata
where each (p, l) is  or a disjunction of states
A1W automata have the same expressive power as LTL
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 15/30
LTLBA via alternating 1-weak BA
LTLA1W
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 16/30
LTLA1W
Input: an LTL formula  and an alphabet  = 2AP
for some finite AP  AP
Output: A1W automaton A = (, Q, , q, F) accepting L()
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 17/30
LTLA1W
Input: an LTL formula  and an alphabet  = 2AP
for some finite AP  AP
Output: A1W automaton A = (, Q, , q, F) accepting L()
Q = {q, q |  is a subformula of }
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 18/30
LTLA1W
Input: an LTL formula  and an alphabet  = 2AP
for some finite AP  AP
Output: A1W automaton A = (, Q, , q, F) accepting L()
Q = {q, q |  is a subformula of }
 is defined as follows (where   B+(Q) satisfies   )
(q , l) = = 
(qa, l) = if a  l,  otherwise  =
(q, l) = (q, l) q = q
(q, l) = (q, l)  (q, l) q = q
(qX, l) = q    =   
(qU, l) = (q, l)  ((q, l)  qU)    =   
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 19/30
LTLA1W
Input: an LTL formula  and an alphabet  = 2AP
for some finite AP  AP
Output: A1W automaton A = (, Q, , q, F) accepting L()
Q = {q, q |  is a subformula of }
 is defined as follows (where   B+(Q) satisfies   )
(q , l) = = 
(qa, l) = if a  l,  otherwise  =
(q, l) = (q, l) q = q
(q, l) = (q, l)  (q, l) q = q
(qX, l) = q    =   
(qU, l) = (q, l)  ((q, l)  qU)    =   
F = {q(U) |  U  is a subformula of }
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 20/30
LTLA1W
Theorem
Given an LTL formula  and an alphabet , one can construct
an A1W automaton A accepting L() and such that the
number of states of A is linear in the length of .
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 21/30
LTLBA via alternating 1-weak BA
A1WBA
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 22/30
A1WBA
Input: an alternating BA A = (, Q, , q0, F)
Output: a BA A = (, Q ,  , q0, F ) accepting L(A)
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 23/30
A1WBA
Input: an alternating BA A = (, Q, , q0, F)
Output: a BA A = (, Q ,  , q0, F ) accepting L(A)
Intuitively, A guesses labeling of each level of the computation
tree of A. Moreover, A has to divide the set of states into two
sets: states labeling paths with recent occurrence of an accepting
states and the other states.
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 24/30
A1WBA
Input: an alternating BA A = (, Q, , q0, F)
Output: a BA A = (, Q ,  , q0, F ) accepting L(A)
Q = 2Q × 2Q
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 25/30
A1WBA
Input: an alternating BA A = (, Q, , q0, F)
Output: a BA A = (, Q ,  , q0, F ) accepting L(A)
Q = 2Q × 2Q
q0 = ({q0}, )
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 26/30
A1WBA
Input: an alternating BA A = (, Q, , q0, F)
Output: a BA A = (, Q ,  , q0, F ) accepting L(A)
Q = 2Q × 2Q
q0 = ({q0}, )
 ((U, V), l) is defined as:
if U =  then
 ((U, V), l) = {(U , V ) | X, Y  Q such that
X |= qU (q, l) and
Y |= qV (q, l) and
U = X F and V = Y  (X  F)}
if U =  then
 ((, V), l) = {(U , V ) | Y  Q such that
Y |= qV (q, l) and
U = Y F and V = Y  F)}
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 27/30
A1WBA
Input: an alternating BA A = (, Q, , q0, F)
Output: a BA A = (, Q ,  , q0, F ) accepting L(A)
Q = 2Q × 2Q
q0 = ({q0}, )
 ((U, V), l) is defined as:
if U =  then
 ((U, V), l) = {(U , V ) | X, Y  Q such that
X |= qU (q, l) and
Y |= qV (q, l) and
U = X F and V = Y  (X  F)}
if U =  then
 ((, V), l) = {(U , V ) | Y  Q such that
Y |= qV (q, l) and
U = Y F and V = Y  F)}
F = {} × 2Q
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 28/30
LTLA1W
Theorem
Given an alternating BA A = (, Q, , q0, F), one can construct
a BA A accepting L(A) and such that the number of states of
A is 2O(|Q|).
Corollary
Given an LTL formula  and an alphabet , one can construct a
BA A accepting L() and such that the number of states of
A is 2O(||).
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 29/30
Coming next week
Partial order reduction
When can a state/transition be safely removed from a
Kripke structure?
What is a stuttering principle?
Can we effectively compute the reduction?
IA159 Formal Verification Methods: LTLBA via Alternating 1-Weak BA 30/30