Branching-Time Temporal Logics. Theoretical Issues and a Computer Science Application [PhD Thesis]

Contents iii
Introduction vi
1 Preliminary notions 1
1.1 Set structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.1.1 Kripke structures . . . . . . . . . . . . . . . . . . . . . . 12
1.1.2 Computational graphs . . . . . . . . . . . . . . . . . . . 16
1.1.3 Computational trees . . . . . . . . . . . . . . . . . . . . 19
1.1.4 Unwinding by using forwarded-past . . . . . . . . . . . . 22
2 Branching-time temporal logics 27
2.1 Temporal logics, description logics, and propositional μ-calculus 28
2.1.1 The computational tree logic CTL? . . . . . . . . . . . . 28
2.1.2 Computational tree logics with past . . . . . . . . . . . . 31
2.1.3 The description logic ALCQ([,\) . . . . . . . . . . . . . 34
2.1.4 The propositional μ-calculus . . . . . . . . . . . . . . . 36
2.2 The branching-time temporal logics BTL? and BTL?bp . . . . . 40
2.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 42
2.2.3 Other operators . . . . . . . . . . . . . . . . . . . . . . . 48
2.2.4 The branching-time temporal logics BTL and BTLbp . . 50
2.3 The linear-past and non-past restrictions BTL?lp and BTL?np . . 52
2.3.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
2.3.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 53
2.4 The temporal constraint extension BTL?C . . . . . . . . . . . . 55
2.4.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
2.4.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 55
2.4.3 Other operators . . . . . . . . . . . . . . . . . . . . . . . 57
2.4.4 Related sub logic and new extensions . . . . . . . . . . . 58
2.5 Expressiveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
2.5.1 Unlimited branching-past versus limited branching-past . 63
2.5.2 Limited branching-past versus limited linear-past . . . . 65
2.5.3 Unlimited branching-past versus limited linear-past . . . 67
2.5.4 Graded logics versus ungraded logics . . . . . . . . . . . 67
3 Satisability and model checking 69
3.1 Logic transformations . . . . . . . . . . . . . . . . . . . . . . . . 70
3.1.1 Initial and nal worlds elimination . . . . . . . . . . . . 72
3.1.2 Path quantiers expansion . . . . . . . . . . . . . . . . . 75
3.1.3 Past time operators translation . . . . . . . . . . . . . . 81
3.1.4 Multi modal operators elimination . . . . . . . . . . . . 83
3.2 Logic to alternating tree automaton translations . . . . . . . . . 85
3.2.1 BTL and BTLnp translation . . . . . . . . . . . . . . . 85
3.2.2 BTL and BTLnp model checking . . . . . . . . . . . . . 88
4 An undecidable extension 96
4.1 Substructure quantiers . . . . . . . . . . . . . . . . . . . . . . 97
4.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
4.1.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 98
4.2 Undecidability result . . . . . . . . . . . . . . . . . . . . . . . . 99
4.2.1 Pre-grid building and global accessibility . . . . . . . . . 100
4.2.2 Commutative futures and grid characterization . . . . . . 103
4.2.3 Locally compatible tiling . . . . . . . . . . . . . . . . . . 108
4.2.4 Reducibility and undecidability . . . . . . . . . . . . . . 109
5 Engineering usefulness 111
5.1 The cache coherence problem in shared-bus systems . . . . . . . 112
5.2 Formal specication of a two-phases cache coherence protocol . 115
5.3 Project of a new two-phases cache coherence protocol . . . . . . 122
5.4 Formal verication of the protocol . . . . . . . . . . . . . . . . . 130
Conclusions and further developments 135
Bibliography 137
List of Figures 143
List of Tables 145