Document Text Contents
Page 83
5
Büchi Automata for Shortest
Counterexamples
The present letter is a very long one, simply because I had no leisure to make it shorter.
Blaise Pascal, Provincial Letters: Letter XVI
In the automatonbased approach to model checking, a PLTLB property is verified by searching
for loops in the synchronous product of a Kripke structure M , representing the model, and a
Büchi automaton B, accepting counterexamples for the property. To obtain shortest counterex
amples, B must be able to accept these in a “short enough” way. In this chapter we formally de
fine, when a Büchi automaton accepts shortest counterexamples (termed tight), and we present
necessary and sufficient conditions for tightness (Sect. 5.1). Section 5.2 examines whether ex
isting approaches meet these conditions. It turns out that none of the constructions we looked
at fulfills the criteria for PLTLB. Therefore, in Sect. 5.3 we give a construction of a tight Büchi
automaton from a PLTLB formula. The construction is generalized to tighten arbitrary Büchi
automata in Sect. 5.4. Section 5.5 discusses related work and Sect. 5.6 gives a brief summary.
5.1 Tight Büchi Automata
Intuition If shortest counterexamples are desired in the automatonbased approach to model
checking, the product of the model M and the Büchi automaton B must have an initialized fair
path λ = 〈µ, ν〉 that can be represented as lasso of the same length as the shortest counterex
ample α = 〈β, γ〉 in M . From Lemma 1 it can be inferred that a path λ = 〈µ, ν〉 in M × B
of the same length as the counterexample α = 〈β, γ〉 in M implies that the corresponding
path ρ = στω in B can be represented as the same type as 〈β, γ〉. In other words, the Büchi
automaton should adapt as a chameleon to the counterexamples present in the model.
Example Consider the scenarios in Fig. 5.1. The Büchi automaton B in the left scenario has
a path στω of the same structure as the counterexample βγω in M , leading to an equally short
counterexample (β × σ)(γ × τ)ω in the product M × B. The path of the Büchi automaton in
the right scenario has an unnecessarily long stem and loop. Note, that the length of the stem in
M × B is the maximum of the lengths of the stems in M and B, and the length of the loop in
M × B is the least common multiple of the lengths of the loops in M and B.
67
Page 84
68 CHAPTER 5. BÜCHI AUTOMATA FOR SHORTEST COUNTEREXAMPLES
���� ������
��
�
� �� ��
���� �� ��
(β γ γ[0]) (σ)o xo (γ[1,2] γ γ γ γ[0]) (τ τ τ)o o o o x o o
�
��
�
�
��
�
�
��
�
�
�
!
!"
"
#
#$
$
%
%&
&
'
'(
(
)
)*
*
+
+,
,
�
�
.�.
.�. /
/
0
0
1
12
2
3
34
4
5
56
6
7
78
8
9
9:
:
;
;<
<
=
=>
>
?
[email protected]
@
A
AB
B
C
CD
D
E�E
E�E
F�F
F�F G
G
H
H
I
IJ
J
K
KL
L
M
MN
N
O
OP
P
Q
QR
R
S
ST
T
U
UV
V
W
WX
X
Y
YZ
Z
[
[\
\
]�]
]�]
^�^
^�^ _
_
`
` a
a
b
b c
c
d
d e�e
e�e
f�f
f�f g
g
h
h i
i
j
j k
k
l
l m
m
n
n o�o
o�o
p
p q
q
r
r s
s
t
t u
u
v
v w
w
x
x y
y
z
z {�{
{�{

 }
}
~
~ �
�
�
��
��
�
�
��
�
���
����
�
�
��
�
�
��
�
�
��
�
�
��
�
��������������������������������������������������������������������������������������������������
�
�
�
�
�
�
�
�
��������������������������������������������������������������������������������������������������
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
β γ γ γ
B
M
M x B
β γ γ γ γ γ
σ τ τ τ σ τ τ τ
β σ γ τ γ τ γ τxxxx
index 0 4 7 10 0 8 12 16
Figure 5.1: Scenarios with shortest and nonoptimal counterexample
Formal definition Kupferman and Vardi [KV01] call an automaton on finite words tight if
it accepts shortest prefixes for violations of safety formulae. We extend that notion to Büchi
automata on infinite words.
Definition 6 Let B = (S, T, I, L, F ) be a Büchi automaton. B is tight iff
∀α ∈ Lang(B) . ∀β, γ . (α = βγω ⇒
∃ρ ∈ ΠF (B) . (L(ρ) = α ∧ type(〈β, γ〉) ∈ type(ρ)))
Alternative criteria The left scenario in Fig. 5.1 suggests another, alternative formulation,
which may be more intuitive and is easier to prove for some automata: the subsequences
of α starting at indices 4, 7, 10, . . . are the same, as are those beginning at 5, 8, 11, . . ., and
6, 9, 12, . . .. On the other hand, the subsequences starting at the respective indices in a single
iteration (e.g., 4, 5, 6) are all different — otherwise a part of the loop could be cut out, contra
dicting minimality. Hence, if B is tight, there must be an initialized fair path ρ with L(ρ) = α
with the following property: for each pair of indices i, j, if the subsequences of α starting at
i and j have the same future (α[i,∞] = α[j,∞]), then ρ maps i and j to the same state in B
(ρ[i] = ρ[j]). Theorem 20 establishes the equivalence of the criteria.
Theorem 20 Let B = (S, T, I, L, F ) be a Büchi automaton. The following statements are
equivalent:
1. B is tight.
2. ∀α ∈ Lang(B) . ∀β, γ . (〈β, γ〉 is minimal for α⇒
∃ρ ∈ ΠF (B) . (L(ρ) = α ∧ type(〈β, γ〉) ∈ type(ρ)))
3. ∀α ∈ Lang(B) . ((∃β, γ . α = βγω) ⇒
(∃ρ ∈ ΠF (B) . (L(ρ) = α ∧ (∀i, j . α[i,∞] = α[j,∞] ⇒ ρ[i] = ρ[j]))))
4. ∀α ∈ Lang(B) . ∀β, γ . (〈β, γ〉 is minimal for α⇒
∃ρ ∈ ΠF (B) . ∃σ, τ . (L(ρ) = α ∧ ρ = στω ∧ 〈σ, τ〉 = 〈β, γ〉))
5. ∀α ∈ Lang(B) . ∀β, γ . (α = βγω ⇒
∃ρ ∈ ΠF (B) . ∃σ, τ . (L(ρ) = α ∧ ρ = στω ∧ 〈σ, τ〉 = 〈β, γ〉))
Proof: 5 ⇒ 4: Obvious, 〈β, γ〉 being minimal for α implies α = βγω.
Page 167
Curriculum Vitae
Viktor Schuppan
September 5, 1973 Born in München, Germany
1980 – 1984 Primary school, Putzbrunn
1984 – 1993 Gymnasium Neubiberg
1993 Abitur
1993 – 1999 Studies in Computer Science, TU München
1995 – 1996 Erasmus year at Queen’s University Belfast, UK
1996 Internship at Siemens, München
1997 Internship at HYPOBank, München
1999 Diploma in Computer Science, TU München
1999 – 2000 Alternative national service, Klinikum Großhadern
since 2001 Research and Teaching Assistant
Computer Systems Institute, ETH Zurich
151
5
Büchi Automata for Shortest
Counterexamples
The present letter is a very long one, simply because I had no leisure to make it shorter.
Blaise Pascal, Provincial Letters: Letter XVI
In the automatonbased approach to model checking, a PLTLB property is verified by searching
for loops in the synchronous product of a Kripke structure M , representing the model, and a
Büchi automaton B, accepting counterexamples for the property. To obtain shortest counterex
amples, B must be able to accept these in a “short enough” way. In this chapter we formally de
fine, when a Büchi automaton accepts shortest counterexamples (termed tight), and we present
necessary and sufficient conditions for tightness (Sect. 5.1). Section 5.2 examines whether ex
isting approaches meet these conditions. It turns out that none of the constructions we looked
at fulfills the criteria for PLTLB. Therefore, in Sect. 5.3 we give a construction of a tight Büchi
automaton from a PLTLB formula. The construction is generalized to tighten arbitrary Büchi
automata in Sect. 5.4. Section 5.5 discusses related work and Sect. 5.6 gives a brief summary.
5.1 Tight Büchi Automata
Intuition If shortest counterexamples are desired in the automatonbased approach to model
checking, the product of the model M and the Büchi automaton B must have an initialized fair
path λ = 〈µ, ν〉 that can be represented as lasso of the same length as the shortest counterex
ample α = 〈β, γ〉 in M . From Lemma 1 it can be inferred that a path λ = 〈µ, ν〉 in M × B
of the same length as the counterexample α = 〈β, γ〉 in M implies that the corresponding
path ρ = στω in B can be represented as the same type as 〈β, γ〉. In other words, the Büchi
automaton should adapt as a chameleon to the counterexamples present in the model.
Example Consider the scenarios in Fig. 5.1. The Büchi automaton B in the left scenario has
a path στω of the same structure as the counterexample βγω in M , leading to an equally short
counterexample (β × σ)(γ × τ)ω in the product M × B. The path of the Büchi automaton in
the right scenario has an unnecessarily long stem and loop. Note, that the length of the stem in
M × B is the maximum of the lengths of the stems in M and B, and the length of the loop in
M × B is the least common multiple of the lengths of the loops in M and B.
67
Page 84
68 CHAPTER 5. BÜCHI AUTOMATA FOR SHORTEST COUNTEREXAMPLES
���� ������
��
�
� �� ��
���� �� ��
(β γ γ[0]) (σ)o xo (γ[1,2] γ γ γ γ[0]) (τ τ τ)o o o o x o o
�
��
�
�
��
�
�
��
�
�
�
!
!"
"
#
#$
$
%
%&
&
'
'(
(
)
)*
*
+
+,
,
�
�
.�.
.�. /
/
0
0
1
12
2
3
34
4
5
56
6
7
78
8
9
9:
:
;
;<
<
=
=>
>
?
[email protected]
@
A
AB
B
C
CD
D
E�E
E�E
F�F
F�F G
G
H
H
I
IJ
J
K
KL
L
M
MN
N
O
OP
P
Q
QR
R
S
ST
T
U
UV
V
W
WX
X
Y
YZ
Z
[
[\
\
]�]
]�]
^�^
^�^ _
_
`
` a
a
b
b c
c
d
d e�e
e�e
f�f
f�f g
g
h
h i
i
j
j k
k
l
l m
m
n
n o�o
o�o
p
p q
q
r
r s
s
t
t u
u
v
v w
w
x
x y
y
z
z {�{
{�{

 }
}
~
~ �
�
�
��
��
�
�
��
�
���
����
�
�
��
�
�
��
�
�
��
�
�
��
�
��������������������������������������������������������������������������������������������������
�
�
�
�
�
�
�
�
��������������������������������������������������������������������������������������������������
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
�
β γ γ γ
B
M
M x B
β γ γ γ γ γ
σ τ τ τ σ τ τ τ
β σ γ τ γ τ γ τxxxx
index 0 4 7 10 0 8 12 16
Figure 5.1: Scenarios with shortest and nonoptimal counterexample
Formal definition Kupferman and Vardi [KV01] call an automaton on finite words tight if
it accepts shortest prefixes for violations of safety formulae. We extend that notion to Büchi
automata on infinite words.
Definition 6 Let B = (S, T, I, L, F ) be a Büchi automaton. B is tight iff
∀α ∈ Lang(B) . ∀β, γ . (α = βγω ⇒
∃ρ ∈ ΠF (B) . (L(ρ) = α ∧ type(〈β, γ〉) ∈ type(ρ)))
Alternative criteria The left scenario in Fig. 5.1 suggests another, alternative formulation,
which may be more intuitive and is easier to prove for some automata: the subsequences
of α starting at indices 4, 7, 10, . . . are the same, as are those beginning at 5, 8, 11, . . ., and
6, 9, 12, . . .. On the other hand, the subsequences starting at the respective indices in a single
iteration (e.g., 4, 5, 6) are all different — otherwise a part of the loop could be cut out, contra
dicting minimality. Hence, if B is tight, there must be an initialized fair path ρ with L(ρ) = α
with the following property: for each pair of indices i, j, if the subsequences of α starting at
i and j have the same future (α[i,∞] = α[j,∞]), then ρ maps i and j to the same state in B
(ρ[i] = ρ[j]). Theorem 20 establishes the equivalence of the criteria.
Theorem 20 Let B = (S, T, I, L, F ) be a Büchi automaton. The following statements are
equivalent:
1. B is tight.
2. ∀α ∈ Lang(B) . ∀β, γ . (〈β, γ〉 is minimal for α⇒
∃ρ ∈ ΠF (B) . (L(ρ) = α ∧ type(〈β, γ〉) ∈ type(ρ)))
3. ∀α ∈ Lang(B) . ((∃β, γ . α = βγω) ⇒
(∃ρ ∈ ΠF (B) . (L(ρ) = α ∧ (∀i, j . α[i,∞] = α[j,∞] ⇒ ρ[i] = ρ[j]))))
4. ∀α ∈ Lang(B) . ∀β, γ . (〈β, γ〉 is minimal for α⇒
∃ρ ∈ ΠF (B) . ∃σ, τ . (L(ρ) = α ∧ ρ = στω ∧ 〈σ, τ〉 = 〈β, γ〉))
5. ∀α ∈ Lang(B) . ∀β, γ . (α = βγω ⇒
∃ρ ∈ ΠF (B) . ∃σ, τ . (L(ρ) = α ∧ ρ = στω ∧ 〈σ, τ〉 = 〈β, γ〉))
Proof: 5 ⇒ 4: Obvious, 〈β, γ〉 being minimal for α implies α = βγω.
Page 167
Curriculum Vitae
Viktor Schuppan
September 5, 1973 Born in München, Germany
1980 – 1984 Primary school, Putzbrunn
1984 – 1993 Gymnasium Neubiberg
1993 Abitur
1993 – 1999 Studies in Computer Science, TU München
1995 – 1996 Erasmus year at Queen’s University Belfast, UK
1996 Internship at Siemens, München
1997 Internship at HYPOBank, München
1999 Diploma in Computer Science, TU München
1999 – 2000 Alternative national service, Klinikum Großhadern
since 2001 Research and Teaching Assistant
Computer Systems Institute, ETH Zurich
151