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