Atnaujinkite slapukų nuostatas

Logic in Computer Science: Modelling and Reasoning about Systems 2nd Revised edition [Minkštas viršelis]

3.96/5 (140 ratings by Goodreads)
(Imperial College of Science, Technology and Medicine, London), (University of Birmingham)
  • Formatas: Paperback / softback, 440 pages, aukštis x plotis x storis: 247x175x21 mm, weight: 750 g, Worked examples or Exercises; 10 Tables, unspecified
  • Išleidimo metai: 26-Aug-2004
  • Leidėjas: Cambridge University Press
  • ISBN-10: 052154310X
  • ISBN-13: 9780521543101
Kitos knygos pagal šią temą:
Logic in Computer Science: Modelling and Reasoning about Systems 2nd Revised editionDidesnis paveikslėlis
  • Formatas: Paperback / softback, 440 pages, aukštis x plotis x storis: 247x175x21 mm, weight: 750 g, Worked examples or Exercises; 10 Tables, unspecified
  • Išleidimo metai: 26-Aug-2004
  • Leidėjas: Cambridge University Press
  • ISBN-10: 052154310X
  • ISBN-13: 9780521543101
Kitos knygos pagal šią temą:
Pastovi nuoroda: https://www.kriso.lt/db/9780521543101.html
Raktažodžiai:
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.

Recenzijos

' an unusual, inspiring and remarkable book one can find in it all the material which is suitable for undergraduate and beginning graduate students in computer science and electrical engineering who will profit by using it in their professional activities in the near future.' Zentralblatt MATH 'The second edition of this successful textbook continues to provide a clear introduction to formal reasoning relevant to the needs of modern computer science and sufficiently exacting for practical applications.' Phinews 'This book provides an elegant introduction to formal reasoning that is relevant to computation science. This second edition improves the first one with extra and expanded sections on temporal logic model checking, SAT solvers, second-order logic, the Alloy specification language, and programming by contract. The material is up-to-date and practical ' Zentralblatt MATH

Daugiau informacijos

Provides a sound basis in logic, and introduces logical frameworks used in modelling, specifying and verifying computer systems.
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