Decidability of Modal Logics with Particular Emphasis on the Interval Temporal Logics [PhD Thesis]

I. Introduction 1
1. Modal logic 3
2. Halpern{Shoham logic 5
II. Elementary modal logics 7
3. Overview 9
4. Preliminaries 11
4.1. Domino systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
5. Undecidability 14
5.1. Key tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
5.2. First-order formulas with three variables . . . . . . . . . . . . . . . . 16
5.3. Undecidability for unimodal logic dened by Horn formulas with inequality
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
5.4. Undecidability for bimodal logic defined by Horn formulas . . . . . . 19
5.5. Local satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
6. Model properties 22
6.1. Minimal tree-based models . . . . . . . . . . . . . . . . . . . . . . . 22
6.2. Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
6.3. The closures of linear structures . . . . . . . . . . . . . . . . . . . . . 24
6.4. Forks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
6.5. Boundedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
6.6. Omitted proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
6.6.1. Proof of Lemma 6.2 . . . . . . . . . . . . . . . . . . . . . . . 26
6.6.2. Proof of Lemma 6.9 . . . . . . . . . . . . . . . . . . . . . . . 28
6.6.3. Proof of Lemma 6.10 . . . . . . . . . . . . . . . . . . . . . . . 32
6.6.4. Proof of Lemma 6.11 . . . . . . . . . . . . . . . . . . . . . . . 34
6.6.5. Proof of Lemma 6.12 . . . . . . . . . . . . . . . . . . . . . . . 35
7. The decidability 40
7.1. Tree-compatible case . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
7.1.1. Formulas that do not force long edges . . . . . . . . . . . . . 40
7.1.2. Formulas that force only long forward edges . . . . . . . . . . 41
7.1.3. Formulas that force long and backward edges . . . . . . . . . 42
7.2. The tree-incompatibility . . . . . . . . . . . . . . . . . . . . . . . . . 42
7.3. Sharpening the complexity . . . . . . . . . . . . . . . . . . . . . . . . 43
7.3.1. Formulas with TCMP . . . . . . . . . . . . . . . . . . . . . . 43
7.3.2. Formulas without TCMP that do not force long edges . . . . 45
7.3.3. Formulas without TCMP that force only long forward edges . 46
7.3.4. Formulas without TCMP that force long and backward edges 47
7.4. Horn formulas and equality . . . . . . . . . . . . . . . . . . . . . . . 48
8. Finite satisfiability 49
8.1. Formulas that do not force long edges . . . . . . . . . . . . . . . . . 49
8.1.1. Local satisfiability . . . . . . . . . . . . . . . . . . . . . . . . 49
8.1.2. Global satisfiability . . . . . . . . . . . . . . . . . . . . . . . . 50
8.2. Formulas that force long edges . . . . . . . . . . . . . . . . . . . . . 59
III. Halpern{Shoham logic 61
9. Overview 63
9.1. Main theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
9.2. Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
10.Proof of Theorem 9.1 66
10.1. The Regular Language LA . . . . . . . . . . . . . . . . . . . . . . . . 66
10.2. Orientation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
10.3. Encoding a Finite Automaton . . . . . . . . . . . . . . . . . . . . . . 71
10.4. A Cloud . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
10.5. Using a cloud. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
10.5.1. An example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
10.5.2. Encoding two-counter automaton . . . . . . . . . . . . . . . . 75
11.Proof of Theorem 9.2 76
11.1. Damage assessment . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
11.2. The parabola . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
12.More results 81
12.1. Superinterval relation . . . . . . . . . . . . . . . . . . . . . . . . . . 81
12.2. Global satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
12.3. Strict D . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
12.4. Arbitrary orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84