Download Liveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties PDF

TitleLiveness Checking as Safety Checking to Find Shortest Counterexamples to Linear Time Properties
Author
LanguageEnglish
File Size1.7 MB
Total Pages167
Table of Contents
                            Abstract
Zusammenfassung
Acknowledgments
Contents
1 Introduction
	1.1 Safety and Liveness
	1.2 Counterexamples in Verification
	1.3 Thesis Statement and Contributions
		1.3.1 Reduction
		1.3.2 Büchi Automata for Shortest Counterexamples
	1.4 Outline
	1.5 Previously Published Results
2 Common Concepts and Notation
	2.1 Background
		2.1.1 Temporal Logic
		2.1.2 Model Checking
	2.2 Preliminaries
	2.3 Kripke Structures as Models
	2.4 Linear Temporal Logic
	2.5 Büchi Automata
	2.6 Translating PLTLB Formulae into Büchi Automata
	2.7 Defining Safety and Liveness
	2.8 Model Checking Linear Time Properties
		2.8.1 Basics
		2.8.2 Lasso-shaped counterexamples
		2.8.3 Model checking using BDDs
		2.8.4 Bounded model checking using SAT solvers
		2.8.5 Abstraction
3 Symbolic Loop Detection for Finite State Systems
	3.1 Translating Simple Liveness into Safety
		3.1.1 Intuition
		3.1.2 Counter-Based Translation
		3.1.3 State-Recording Translation
		3.1.4 Comparison
	3.2 Translating Fair Repeated Reachability
		3.2.1 First Attempt
		3.2.2 Optimization
		3.2.3 Formalization and Correctness
		3.2.4 Extensions
	3.3 Complexity
		3.3.1 Explicit State Model Checking
		3.3.2 BDD-based Symbolic Model Checking
		3.3.3 Summary
	3.4 Shortest Counterexamples
	3.5 Related Work
		3.5.1 Reduction to and Power of Reachability Checking
		3.5.2 Shortest Counterexamples
	3.6 Summary
4 Extending to Infinite State Systems
	4.1 Regular Model Checking
		4.1.1 Preliminaries
		4.1.2 Reduction
		4.1.3 Example
		4.1.4 Discussion
	4.2 Pushdown Systems
		4.2.1 Preliminaries
		4.2.2 Reduction
		4.2.3 Complexity
		4.2.4 Shortest Lasso-Shaped Counterexamples
	4.3 Timed Automata
		4.3.1 Preliminaries
		4.3.2 Reduction
		4.3.3 Complexity
		4.3.4 Shortest Lasso-Shaped Counterexamples
	4.4 Related Work
	4.5 Summary
5 Büchi Automata for Shortest Counterexamples
	5.1 Tight Büchi Automata
	5.2 (Non-) Optimality of Specific Approaches
		5.2.1 Gerth et al. (GPVW)
		5.2.2 Kesten et al. (KPR)
	5.3 A Tight Look at LTL Model Checking
		5.3.1 Virtual Unrolling for Bounded Model Checking of PLTLB
		5.3.2 A Tight Büchi Automaton for PLTLB
		5.3.3 Partial Unrolling
	5.4 Generalization
	5.5 Related Work
		5.5.1 Virtual unrolling
		5.5.2 Tight automata
		5.5.3 Translating PLTLB into automata
	5.6 Summary
6 Variable Optimization
	6.1 The General Case
	6.2 Removing Constants
	6.3 Removing Input Variables
	6.4 Cone of Influence Reduction for Loop Detection
	6.5 Abstraction Refinement for Loop Detection
	6.6 Utility of ...
	6.7 Related Work
		6.7.1 Completeness in bounded model checking
		6.7.2 Identifying input variables and variable dependencies
		6.7.3 Abstraction and refinement
	6.8 Summary
7 Experiments
	7.1 A Forward Jumping Counter
	7.2 Real-World Examples
		7.2.1 State-Recording Translation versus Standard Approach
		7.2.2 BDD- versus SAT-based Model Checking of the Tight Encoding
		7.2.3 The Cost of Tightness
		7.2.4 Comparing Variants of Variable Optimization
		7.2.5 A Tight Büchi Automaton in the Standard Approach
	7.3 Summary
8 Conclusion
	8.1 Contributions
	8.2 Future Work
		8.2.1 State-Recording Translation
		8.2.2 Infinite State Systems
		8.2.3 Tight Büchi Automata
A Proofs and Auxiliary Lemmas
B Raw Data
List of Figures
List of Tables
Bibliography
                        
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 automaton-based 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 automaton-based 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 non-optimal 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 HYPO-Bank, 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

Similer Documents