Book:Michael R.A. Huth/Logic in Computer Science: Modelling and reasoning about systems

Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems

Published $\text {2000}$, Cambridge University Press

ISBN 0-521-65602-8

Subject Matter

• Symbolic Logic
• Mathematical Logic

Contents

Foreword (Edmund M. Clarke)

Preface

Acknowledgments

1 Propositional logic

1.1 Declarative sentences

1.2 Natural deduction

1.2.1 Rules for natural deduction

1.2.2 Derived rules

1.2.3 Natural deduction in summary

1.2.4 Provable equivalence

1.2.5 An aside: proof by contradiction

1.3 Propositional logic as a formal language

1.4 Semantics of propositional logic

1.4.1 The meaning of logical connectives

1.4.2 Mathematical induction

1.4.3 Soundness of propositional logic

1.4.4 Completeness of propositional logic

1.5 Normal forms

1.5.1 Semantic equivalence, satisfiability and validity

1.5.2 Conjunctive normal forms and validity

1.5.3 Horn clauses and satisfiability

1.6 Bibliographic notes

2 Predicate logic

2.1 The need for a richer language

2.2 Predicate logic as a formal language

2.2.1 Terms

2.2.2 Formulas

2.2.3 Free and bound variables

2.2.4 Substitution

2.3 Proof theory of predicate logic

2.3.1 Natural deduction rules

2.3.2 Quantifier equivalences

2.4 Semantics of predicate logic

2.4.1 Models

2.4.2 Semantic entailment

2.4.3 The semantics of equality

2.5 Undecidability of predicate logic

2.6 Bibliographic notes

3 Verification by model checking

3.1 Motivation for verification

3.2 The syntax of computation tree logic

3.3 Semantics of computation tree logic

3.3.1 Practical patterns of specifications

3.3.2 Important equivalences between CTL formulas

3.4 Example: mutual exclusion

3.4.1 The first modelling attempt

3.4.2 The second modelling attempt

3.5 A model-checking algorithm

3.5.1 The labelling algorithm

3.5.2 The pseudo-code of the model checking algorithm

3.5.3 The 'state explosion' problem

3.6 The SMV system

3.6.1 Modules in SMV

3.6.2 Synchronous and asynchronous composition

3.6.3 Mutual exclusion revisited

3.6.4 The alternating bit protocol

3.7 Model checking with fairness

3.8 Alternatives and extensions of CTL

3.8.1 Linear-time temporal logic

3.8.2 CTL^*

3.8.3 The expressive power of CTL

3.9 The fixed-point characterisation of CTL

3.9.1 Monotone functions

3.9.2 The correctness of SAT_EG

3.9.3 The correctness of SAT_EU

3.10 Bibliographic notes

4 Program verification

4.1 Why should we specify and verify code?

4.2 A framework for software verification

4.2.1 A core programming language

4.2.2 Hoare triples

4.2.3 Partial and total correctness

4.2.4 Program variables and logical variables

4.3 Proof calculus for partial correctness

4.3.1 Proof rules

4.3.2 Proof tableaux

4.3.3 A case study: minimal-sum section

4.4 Proof calculus for total correctness

4.5 Bibliographic notes

5 Modal logics and agents

5.1 Modes of truth

5.2 Basic modal logic

5.2.1 Syntax

5.2.2 Semantics

5.3 Logic engineering

5.3.1 The stock of valid formulas

5.3.2 Important properties of the accessibility relation

5.3.3 Correspondence theory

5.3.4 Some modal logics

5.3.5 Semantic entailment

5.4 Natural deduction

5.5 Reasoning about knowledge in a multi-agent system

5.5.1 Some examples

5.5.2 The modal logic $\text{KT45}^n$

5.5.3 Natural deduction for $\text{KT45}^n$

5.5.4 Formalising the examples

5.6 Bibliographic notes

6. Binary decision diagrams

6.1 Representing boolean functions

6.1.1 Propositional formulas and truth tables

6.1.2 Binary decision diagrams

6.1.3 Ordered BDDs

6.2 Algorithms for reduced OBDDS

6.2.1 The algorithm reduce

6.2.2 The algorithm apply

6.2.3 The algorithm restrict

6.2.4 The algorithm exists

6.2.5 Assessment of OBDDs

6.3 Symbolic model checking

6.3.1 Representing subsets of the set of states

6.3.2 Representing the transition relation

6.3.3 Implementing the functions $\text{pre}_\exists$ and $\text{pre}_\forall$

6.3.4 Synthesising OBDDs

6.4 A relational mu-calculus

6.4.1 Syntax and semantics

6.4.2 Coding CTL models and specifications

6.5 Bibliographic notes

Bibliography

Index

Next

Source work progress

• 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.4.2$: Mathematical induction

to be reviewed