LEADER 04012nam 2200613Ia 450 001 9910809171103321 005 20170815161710.0 010 $a1-119-99146-3 010 $a1-283-40534-2 010 $a9786613405340 010 $a1-119-99148-X 010 $a1-119-99147-1 035 $a(CKB)3460000000003345 035 $a(EBL)698529 035 $a(SSID)ssj0000477008 035 $a(PQKBManifestationID)11332023 035 $a(PQKBTitleCode)TC0000477008 035 $a(PQKBWorkID)10501564 035 $a(PQKB)10931503 035 $a(MiAaPQ)EBC698529 035 $a(OCoLC)729726226 035 $a(CaSebORM)9780470027882 035 $a(EXLCZ)993460000000003345 100 $a20101207d2011 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 13$aAn introduction to practical formal methods using temporal logic$b[electronic resource] /$fMichael Fisher 205 $a1st edition 210 $aChichester, West Sussex, U.K. ;$aHoboken, N.J. $cWiley$dc2011 215 $a1 online resource (710 p.) 300 $aDescription based upon print version of record. 311 $a0-470-02788-6 320 $aIncludes bibliographical references and index. 327 $aCover; Title Page; Copyright; Preface; Chapter 1: Introduction; 1.1 Aims of the Book; 1.2 Why Temporal Logic?; 1.3 What is Temporal Logic?; 1.4 Structure of the Book; Chapter 2: Temporal Logic; 2.1 Intuition; 2.2 Syntactic Aspects; 2.3 Semantics; 2.4 Reactive System Properties; 2.5 What is Temporal Logic?; 2.6 Normal Form; 2.7 Bu?chi Automata and Temporal Logic; 2.8 Advanced Topics; 2.9 Final Exercises; Chapter 3: Specification; 3.1 Describing Simple Behaviours; 3.2 A Semantics of Imperative Programs; 3.3 Linking Specifications; 3.4 Advanced Topics; 3.5 Final Exercises; 3.6 Where to Next? 327 $aChapter 4: Deduction4.1 Temporal Proof; 4.2 Clausal Temporal Resolution; 4.3 The TSPASS System; 4.4 Advanced topics; 4.5 Final Exercises; Chapter 5: Model Checking; 5.1 Algorithmic Verification; 5.2 Automata-Theoretic Model Checking; 5.3 The Spin System; 5.4 Advanced Topics; 5.5 Final Exercises; Chapter 6: Execution; 6.1 From Specifications to Programs; 6.2 METATEM: Executing Temporal Formulae; 6.3 The Concurrent MetateM system; 6.4 Advanced Topics; Chapter 7: Selected Applications; 7.1 Model Checking Programs; 7.2 Security Protocol Analysis; 7.3 Recognizing Temporal Patterns 327 $a7.4 Parameterized Systems7.5 Reasoning with Intervals; 7.6 Planning; Chapter 8: Summary; Appendix A: Review of Classical Logic; A.1 Introduction; A.2 Propositional Logic; A.3 Normal Forms; A.4 Propositional Resolution; A.5 Horn Clauses; A.6 First-Order Logic; Appendix B: Solutions to Exercises; B.1 Solutions: Chapter 2; Solutions: Chapter 3; Solutions: Chapter 4; Solutions: Chapter 5; Solutions: Chapter 6; Solutions: Appendix A; References; Index 330 $aThe name ""temporal logic"" may sound complex and daunting; but while they describe potentially complex scenarios, temporal logics are often based on a few simple, and fundamental, concepts - highlighted in this book. An Introduction to Practical Formal Methods Using Temporal Logic provides an introduction to formal methods based on temporal logic, for developing and testing complex computational systems. These methods are supported by many well-developed tools, techniques and results that can be applied to a wide range of systems. Fisher begins with a full introduction to the subject 606 $aTemporal automata 606 $aLogic, Symbolic and mathematical 615 0$aTemporal automata. 615 0$aLogic, Symbolic and mathematical. 676 $a005.131 676 $a511.3 700 $aFisher$b Michael$f1962-$01654860 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910809171103321 996 $aAn introduction to practical formal methods using temporal logic$94006954 997 $aUNINA