Logic in Computer Science: Modelling and

Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. The second edition of this successful textbook addresses both those requirements, by continuing to provide a clear introduction to formal reasoning which is both relevant to the needs of modern computer science and rigorous enough for practical application. Improvements to the first edition have been made throughout, with extra and expanded sections on SAT solvers, existential/universal second-order logic, micro-models, programming by contract and total correctness. The coverage of model-checking has been substantially updated. Further exercises have been added. Internet support for the book includes worked solutions for all exercises for teachers, and model solutions to some exercises for students.

Foreword to the first edition

ix

Preface to the second edition

xi

Acknowledgements

xiii

1 Propositional logic

1

(92)

1.1 Declarative sentences

2

(3)

1.2 Natural deduction

5

(26)

1.2.1 Rules for natural deduction

6

(17)

1.2.2 Derived rules

23

(3)

1.2.3 Natural deduction in summary

26

(3)

1.2.4 Provable equivalence

29

(1)

1.2.5 An aside: proof by contradiction

29

(2)

1.3 Propositional logic as a formal language

31

(5)

1.4 Semantics of propositional logic

36

(17)

1.4.1 The meaning of logical connectives

36

(4)

1.4.2 Mathematical induction

40

(5)

1.4.3 Soundness of propositional logic

45

(4)

1.4.4 Completeness of propositional logic

49

(4)

1.5 Normal forms

53

(15)

1.5.1 Semantic equivalence, satisfiability and validity

54

(4)

1.5.2 Conjunctive normal forms and validity

58

(7)

1.5.3 Horn clauses and satisfiability

65

(3)

1.6 SAT solvers

68

(10)

1.6.1 A linear solver

69

(3)

1.6.2 A cubic solver

72

(6)

1.7 Exercises

78

(13)

1.8 Bibliographic notes

91

(2)

2 Predicate logic

93

(79)

2.1 The need for a richer language

93

(5)

2.2 Predicate logic as a formal language

98

(9)

2.2.1 Terms

99

(1)

2.2.2 Formulas

100

(2)

2.2.3 Free and bound variables

102

(2)

2.2.4 Substitution

104

(3)

2.3 Proof theory of predicate logic

107

(15)

2.3.1 Natural deduction rules

107

(10)

2.3.2 Quantifier equivalences

117

(5)

2.4 Semantics of predicate logic

122

(9)

2.4.1 Models

123

(6)

2.4.2 Semantic entailment

129

(1)

2.4.3 The semantics of equality

130

(1)

2.5 Undecidability of predicate logic

131

(5)

2.6 Expressiveness of predicate logic

136

(5)

2.6.1 Existential second-order logic

139

(1)

2.6.2 Universal second-order logic

140

(1)

2.7 Microinodels of software

141

(16)

2.7.1 State machines

142

(4)

2.7.2 Alma - re-visited

146

(2)

2.7.3 A software micromodel

148

(9)

2.8 Exercises

157

(13)

2.9 Bibliographic notes

170

(2)

3 Verification by model checking

172

(84)

3.1 Motivation for verification

172

(3)

3.2 Linear-time temporal logic

175

(12)

3.2.1 Syntax of LTL

175

(3)

3.2.2 Semantics of LTL

178

(5)

3.2.3 Practical patterns of specifications

183

(1)

3.2.4 Important equivalences between LTL formulas

184

(2)

3.2.5 Adequate sets of connectives for LTL

186

(1)

3.3 Model checking: systems, tools, properties

187

(20)

3.3.1 Example: mutual exclusion

187

(4)

3.3.2 The NuSMV model checker

191

(3)

3.3.3 Running NuSMV

194

(1)

3.3.4 Mutual exclusion revisited

195

(4)

3.3.5 The ferryman

199

(4)

3.3.6 The alternating bit protocol

203

(4)

3.4 Branching-time logic

207

(10)

3.4.1 Syntax of CTL

208

(3)

3.4.2 Semantics of CTL

211

(4)

3.4.3 Practical patterns of specifications

215

(1)

3.4.4 Important equivalences between CTL formulas

215

(1)

3.4.5 Adequate sets of CTL connectives

216

(1)

3.5 CTL* and the expressive powers of LTL and CTL

217

(4)

3.5.1 Boolean combinations of temporal formulas in CTL

220

(1)

3.5.2 Past operators in LTL

221

(1)

3.6 Model-checking algorithms

221

(17)

3.6.1 The CTL model-checking algorithm

222

(8)

3.6.2 CTL model checking with fairness

230

(2)

3.6.3 The LTL model-checking algorithm

232

(6)

3.7 The fixed-point characterisation of CTL

238

(7)

3.7.1 Monotone functions

240

(2)

3.7.2 The correctness of SATEEG

242

(1)

3.7.3 The correctness of SATEEU

243

(2)

3.8 Exercises

245

(9)

3.9 Bibliographic notes

254

(2)

4 Program verification

256

(50)

4.1 Why should we specify and verify code?

257

(1)

4.2 A framework for software verification

258

(11)

4.2.1 A core programming language

259

(3)

4.2.2 Hoare triples

262

(3)

4.2.3 Partial and total correctness

265

(3)

4.2.4 Program variables and logical variables

268

(1)

4.3 Proof calculus for partial correctness

269

(23)

4.3.1 Proof rules

269

(4)

4.3.2 Proof tableaux

273

(14)

4.3.3 A case study: minimal-sum section

287

(5)

4.4 Proof calculus for total correctness

292

(4)

4.5 Programming by contract

296

(3)

4.6 Exercises

299

(5)

4.7 Bibliographic notes

304

(2)

5 Modal logics and agents

306

(52)

5.1 Modes of truth

306

(1)

5.2 Basic modal logic

307

(9)

5.2.1 Syntax

307

(1)

5.2.2 Semantics

308

(8)

5.3 Logic engineering

316

(12)

5.3.1 The stock of valid formulas

317

(3)

5.3.2 Important properties of he accessibility relation

320

(2)

5.3.3 Correspondence theory

322

(4)

5.3.4 Some modal logics

326

(2)

5.4 Natural deduction

328

(3)

5.5 Reasoning about knowledge in a multi-agent system

331

(19)

5.5.1 Some examples

332

(3)

5.5.2 The modal logic KT45n

335

(4)

5.5.3 Natural deduction for KT45n

339

5.5.4 Formalising the examples

312

(38)

5.6 Exercises

350

(6)

5.7 Bibliographic notes

356

(2)

6 Binary decision diagrams

358

(56)

6.1 Representing boolean functions

358

(14)

6.1.1 Propositional formulas and truth tables

359

(2)

6.1.2 Binary decision diagrams

361

(5)

6.1.3 Ordered BDDs

366

(6)

6.2 Algorithms for reduced OBDDs

372

(10)

6.2.1 The algorithm reduce

372

(1)

6.2.2 The algorithm apply

373

(4)

6.2.3 The algorithm restrict

377

(1)

6.2.4 The algorithm exists

377

(3)

6.2.5 Assessment of OBDDs

380

(2)

6.3 Symbolic model checking

382

(8)

6.3.1 Representing subsets of the set of states

383

(2)

6.3.2 Representing the transition relation

385

(2)

6.3.3 Implementing the functions preE and preA

387

(1)

6.3.4 Synthesising OBDDs

387

(3)

6.4 A relational mu-calculus

390

(8)

6.4.1 Syntax and semantics

390

(3)

6.4.2 Coding CTL models and specifications

393

(5)

6.5 Exercises

398

(15)

6.6 Bibliographic notes

413

(1)

Bibliography

414

(4)

Index

418

What is included with this book?

The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.

The Used, Rental and eBook copies of this book are not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.

FREE SHIPPING

Rent More, Save More! Use code: BBRENTAL

5% off 1 book, 7% off 2 books, 10% off 3+ books

Logic in Computer Science: Modelling and Reasoning about Systems

Summary

Table of Contents

Supplemental Materials

FREE SHIPPING

Rent More, Save More! Use code: BBRENTAL

5% off 1 book, 7% off 2 books, 10% off 3+ books

Logic in Computer Science: Modelling and Reasoning about Systems

Summary

Table of Contents

Supplemental Materials

Digital License