LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems.pdf

发布时间：2022-06-13 发布人：admin 分类：说明书资料大小：2.17M 资料格式：pdf 举报版权申诉

4efafafa-babe-4a32-b6f8-72d30f23a308.pdf-第1页.png

第1页 / 共440页

4efafafa-babe-4a32-b6f8-72d30f23a308.pdf-第2页.png

第2页 / 共440页

4efafafa-babe-4a32-b6f8-72d30f23a308.pdf-第3页.png

第3页 / 共440页

4efafafa-babe-4a32-b6f8-72d30f23a308.pdf-第4页.png

第4页 / 共440页

4efafafa-babe-4a32-b6f8-72d30f23a308.pdf-第5页.png

第5页 / 共440页

4efafafa-babe-4a32-b6f8-72d30f23a308.pdf-第6页.png

第6页 / 共440页

4efafafa-babe-4a32-b6f8-72d30f23a308.pdf-第7页.png

第7页 / 共440页

4efafafa-babe-4a32-b6f8-72d30f23a308.pdf-第8页.png

第8页 / 共440页

Cover

Half-title

Title

Contents

Foreword to the first edition

Preface to the second edition

Our motivation for (re)writing this book

What’s new and what’s gone

The interdependence of chapters and prerequisites

Acknowledgements

Added for second edition

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 SAT solvers

1.6.1 A linear solver

1.6.2 A cubic solver

1.7 Exercises

1.8 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 Expressiveness of predicate logic

2.6.1 Existential second-order logic

2.6.2 Universal second-order logic

2.7 Micromodels of software

2.7.1 State machines

2.7.2 Alma – re-visited

2.7.3 A software micromodel

2.8 Exercises

2.9 Bibliographic notes

3 Verification by model checking

3.1 Motivation for verification

3.2 Linear-time temporal logic

3.2.1 Syntax of LTL

3.2.2 Semantics of LTL

3.2.3 Practical patterns of specifications

3.2.4 Important equivalences between LTL formulas

3.2.5 Adequate sets of connectives for LTL

3.3 Model checking: systems, tools, properties

3.3.1 Example: mutual exclusion

3.3.2 The NuSMV model checker

3.3.3 Running NuSMV

3.3.4 Mutual exclusion revisited

3.3.5 The ferryman

3.3.6 The alternating bit protocol

3.4 Branching-time logic

3.4.1 Syntax of CTL

3.4.2 Semantics of computation tree logic

3.4.3 Practical patterns of specifications

3.4.4 Important equivalences between CTL formulas

3.4.5 Adequate sets of CTL connectives

3.5 CTL and the expressive powers of LTL and CTL

3.5.1 Boolean combinations of temporal formulas in CTL

3.5.2 Past operators in LTL

3.6 Model-checking algorithms

3.6.1 The CTL model-checking algorithm

3.6.2 CTL model checking with fairness

3.6.3 The LTL model-checking algorithm

3.7 The fixed-point characterisation of CTL

3.7.1 Monotone functions

3.7.2 The correctness of SATEG

3.7.3 The correctness of SATEU

3.8 Exercises

3.9 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 Programming by contract

4.6 Exercises

4.7 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

Equivalences between modal formulas

Valid formulas

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.4 Natural deduction

5.5 Reasoning about knowledge in a multi-agent system

5.5.1 Some examples

5.5.2 The modal logic KT45n

5.5.3 Natural deduction for KT45n

5.5.4 Formalising the examples

5.6 Exercises

5.7 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…

6.3.4 Synthesising OBDDs

6.4 A relational mu-calculus

6.4.1 Syntax and semantics

6.5 Exercises

6.6 Bibliographic notes

Bibliography

Index

LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems MICHAEL HUTH Department of Computing Imperial College London, United Kingdom MARK RYAN School of Computer Science University of Birmingham, United Kingdom

CAMBRIDGE UNIVERSITY PRESS Cambridge, New York, Melbourne, Madrid, Cape Town, Singapore, São Paulo Cambridge University Press The Edinburgh Building, Cambridge CB2 8RU, UK Published in the United States of America by Cambridge University Press, New York www.cambridge.org Information on this title: www.cambridge.org/9780521543101 © Cambridge University Press 2004 This publication is in copyright. Subject to statutory exception and to the provision of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press. First published in print format 2004 ISBN-13 ISBN-10 ISBN-13 ISBN-10 978-0-511-26401-6 0-511-26401-1 eBook (EBL) eBook (EBL) 978-0-521-54310-1 0-521-54310-X paperback paperback Cambridge University Press has no responsibility for the persistence or accuracy of urls for external or third-party internet websites referred to in this publication, and does not guarantee that any content on such websites is, or will remain, accurate or appropriate.

Contents Foreword to the ﬁrst edition Preface to the second edition Acknowledgements 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, satisﬁability and validity 1.5.2 Conjunctive normal forms and validity 1.5.3 Horn clauses and satisﬁability 1.6 SAT solvers 1.6.1 A linear solver 1.6.2Acubicsolver 1.7 Exercises 1.8 Bibliographic notes 2 Predicate logic 2.1 The need for a richer language v page ix xi xiii 1 2 5 6 23 26 29 29 31 36 36 40 45 49 53 54 58 65 68 69 72 78 91 93 93

vi Contents 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 Quantiﬁer 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 Expressiveness of predicate logic 2.6.1 Existential second-order logic 2.6.2 Universal second-order logic 2.7 Micromodels of software 2.7.1 State machines 2.7.2 Alma – re-visited 2.7.3 A software micromodel 2.8 Exercises 2.9 Bibliographic notes 3 Veriﬁcation by model checking 3.1 Motivation for veriﬁcation 3.2 Linear-time temporal logic 3.2.1 Syntax of LTL 3.2.2 Semantics of LTL 3.2.3 Practical patterns of speciﬁcations 3.2.4 Important equivalences between LTL formulas 3.2.5 Adequate sets of connectives for LTL 3.3 Model checking: systems, tools, properties 3.3.1 Example: mutual exclusion 3.3.2TheNuSMVmodelchecker 3.3.3 Running NuSMV 3.3.4 Mutual exclusion revisited 3.3.5 The ferryman 3.3.6 The alternating bit protocol 3.4 Branching-time logic 3.4.1 Syntax of CTL 191 98 99 100 102 104 107 107 117 122 123 129 130 131 136 139 140 141 142 146 148 157 170 172 172 175 175 178 183 184 186 187 187 194 195 199 203 207 208

Contents 3.4.2 Semantics of CTL 3.4.3 Practical patterns of speciﬁcations 3.4.4 Important equivalences between CTL formulas 3.4.5 Adequate sets of CTL connectives 3.5 CTL* and the expressive powers of LTL and CTL 3.5.1 Boolean combinations of temporal formulas in CTL 3.5.2 Past operators in LTL 3.6 Model-checking algorithms 3.6.1 The CTL model-checking algorithm 3.6.2 CTL model checking with fairness 3.6.3 The LTL model-checking algorithm 3.7 The ﬁxed-point characterisation of CTL 3.7.1 Monotone functions 3.7.2 The correctness of SATEG 3.7.3 The correctness of SATEU 3.8 Exercises 3.9 Bibliographic notes 4 Program veriﬁcation 4.1 Why should we specify and verify code? 4.2 A framework for software veriﬁcation 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 Programming by contract 4.6 Exercises 4.7 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 vii 211 215 215 216 217 220 221 221 222 230 232 238 240 242 243 245 254 256 257 258 259 262 265 268 269 269 273 287 292 296 299 304 306 306 307 307 308 316 317

viii Contents 5.3.2 Important properties of the accessibility relation 5.3.3 Correspondence theory 5.3.4 Some modal logics 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 KT45n 5.5.3 Natural deduction for KT45n 5.5.4 Formalising the examples 5.6 Exercises 5.7 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 pre∃ and pre∀ 6.3.4 Synthesising OBDDs 6.4 A relational mu-calculus 6.4.1 Syntax and semantics 6.4.2 Coding CTL models and speciﬁcations 6.5 Exercises 6.6 Bibliographic notes Bibliography Index 320 322 326 328 331 332 335 339 342 350 356 358 358 359 361 366 372 372 373 377 377 380 382 383 385 387 387 390 390 393 398 413 414 418

Foreword to the first edition by Edmund M. Clarke FORE Systems Professor of Computer Science Carnegie Mellon University Pittsburgh, PA Formal methods have ﬁnally come of age! Speciﬁcation languages, theorem provers, and model checkers are beginning to be used routinely in industry. Mathematical logic is basic to all of these techniques. Until now textbooks on logic for computer scientists have not kept pace with the development of tools for hardware and software speciﬁcation and veriﬁcation. For exam- ple, in spite of the success of model checking in verifying sequential circuit designs and communication protocols, until now I did not know of a sin- gle text, suitable for undergraduate and beginning graduate students, that attempts to explain how this technique works. As a result, this material is rarely taught to computer scientists and electrical engineers who will need to use it as part of their jobs in the near future. Instead, engineers avoid using formal methods in situations where the methods would be of genuine beneﬁt or complain that the concepts and notation used by the tools are compli- cated and unnatural. This is unfortunate since the underlying mathematics is generally quite simple, certainly no more diﬃcult than the concepts from mathematical analysis that every calculus student is expected to learn. Logic in Computer Science by Huth and Ryan is an exceptional book. I was amazed when I looked through it for the ﬁrst time. In addition to propositional and predicate logic, it has a particularly thorough treatment of temporal logic and model checking. In fact, the book is quite remarkable in how much of this material it is able to cover: linear and branching time temporal logic, explicit state model checking, fairness, the basic ﬁxpoint ix

分享到：

赞收藏

资料库

LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems.pdf

相关推荐

课程资源

热门标签

最新资料