Efnisyfirlit

• Half-title
• Title
• Copyright
• Contents
• Figures and tables
• Figures
• Tables
• Preface
• Part I A Classic Theory of Reactive Systems
• 1 Introduction
• Aims of this book
• 1.1 What are reactive systems?
• 1.2 Process algebras
• 2 The language CCS
• 2.1 Some CCS process constructions
• 2.1.1 The behaviour of processes
• 2.2 CCS, formally
• 2.2.1 The model of labelled transition systems
• 2.2.2 The formal syntax and semantics of CCS
• 2.2.3 Value-passing CCS
• 3 Behavioural equivalences
• 3.1 Criteria for good behavioural equivalence
• 3.2 Trace equivalence: a first attempt
• 3.3 Strong bisimilarity
• 3.4 Weak bisimilarity
• 3.5 Game characterization of bisimilarity
• 3.5.1 Weak bisimulation games
• 3.6 Further results on equivalence checking
• 4 Theory of fixed points and bisimulation equivalence
• 4.1 Posets and complete lattices
• 4.2 Tarski?s fixed point theorem
• 4.3 Bisimulation as a fixed point
• 5 Hennessy?Milner logic
• 5.1 Introduction to Hennessy?Milner logic
• 5.2 Hennessy?Milner theorem
• 6 Hennessy?Milner logic with recursive definitions
• Introduction
• 6.1 Examples of recursive properties
• 6.2 Syntax and semantics of HML with recursion
• 6.3 Largest fixed points and invariant properties
• 6.4 A game characterization for HML with recursion
• 6.4.1 Examples of use
• 6.5 Mutually recursive equational systems
• 6.6 Characteristic properties
• 6.7 Mixing largest and least fixed points
• 6.8 Further results on model checking
• 7 Modelling and analysis of mutual exclusion algorithms
• Introduction
• 7.1 Specifying mutual exclusion in HML
• 7.2 Specifying mutual exclusion using CCS itself
• 7.3 Testing mutual exclusion
• Part II A Theory of Real-time Systems
• 8 Introduction
• 8.1 Real-time reactive systems
• 9 CCS with time delays
• 9.1 Intuition
• 9.2 Timed labelled transition systems
• 9.3 Syntax and SOS rules of timed CCS
• 9.4 Parallel composition
• 9.5 Other timed process algebras and discussion
• 10 Timed automata
• 10.1 Motivation
• 10.2 Syntax of timed automata
• 10.3 Semantics of timed automata
• 10.4 Networks of timed automata
• 10.5 More on timed-automata formalisms
• 11 Timed behavioural equivalences
• 11.1 Timed and untimed trace equivalence
• 11.2 Timed and untimed bisimilarity
• 11.3 Weak timed bisimilarity
• 11.4 Region graphs
• 11.5 Zones and reachability graphs
• 11.6 Further results on timed equivalences
• 12 Hennessy?Milner logic with time
• Introduction
• 12.1 Basic logic
• 12.2 Hennessy?Milner logic with time and regions
• 12.3 Timed bisimilarity versus HML with time
• 12.4 Recursion in HML with time
• 12.4.1 Characteristic properties for timed bisimilarity
• 12.4.2 Examples of real-time temporal properties
• 12.5 More on timed logics
• 13 Modelling and analysis of Fischer?s algorithm
• Introduction
• 13.1 Mutual exclusion using timing
• 13.2 Modelling Fischer?s algorithm
• 13.2.1 Proving mutual exclusion using UPPAAL
• 13.2.2 An erroneous version of Fischer?s algorithm
• 13.3 Further exercises on timing-based mutual exclusion algorithms
• Appendix A Suggestions for student projects
• A.1 Alternating-bit protocol
• A.2 Gossiping girls
• A.3 Implementation of regions
• References
• Index