Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
An introduction to practical formal methods using temporal logic [[electronic resource] /] / Michael Fisher
| An introduction to practical formal methods using temporal logic [[electronic resource] /] / Michael Fisher |
| Autore | Fisher Michael <1962-> |
| Edizione | [1st edition] |
| Pubbl/distr/stampa | Chichester, West Sussex, U.K. ; ; Hoboken, N.J., : Wiley, c2011 |
| Descrizione fisica | 1 online resource (710 p.) |
| Disciplina |
005.131
511.3 |
| Soggetto topico |
Temporal automata
Logic, Symbolic and mathematical |
| ISBN |
1-119-99146-3
1-283-40534-2 9786613405340 1-119-99148-X 1-119-99147-1 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Cover; 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 Bü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?
Chapter 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 7.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 |
| Record Nr. | UNINA-9910130871603321 |
Fisher Michael <1962->
|
||
| Chichester, West Sussex, U.K. ; ; Hoboken, N.J., : Wiley, c2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
An introduction to practical formal methods using temporal logic / / Michael Fisher
| An introduction to practical formal methods using temporal logic / / Michael Fisher |
| Autore | Fisher Michael <1962-> |
| Edizione | [1st edition] |
| Pubbl/distr/stampa | Chichester, West Sussex, U.K. ; ; Hoboken, N.J., : Wiley, c2011 |
| Descrizione fisica | 1 online resource (710 p.) |
| Disciplina | 511.3 |
| Soggetto topico |
Temporal automata
Logic, Symbolic and mathematical |
| ISBN |
9786613405340
9781119991465 1119991463 9781283405348 1283405342 9781119991489 111999148X 9781119991472 1119991471 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Cover; 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 Bü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?
Chapter 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 7.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 |
| Altri titoli varianti | Practical formal methods using temporal logic |
| Record Nr. | UNINA-9910809171103321 |
|
Fisher Michael <1962->
|
||
| Chichester, West Sussex, U.K. ; ; Hoboken, N.J., : Wiley, c2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||