Modal and Temporal Properties of Processes

In a clear and well-organized presentation, Modal and Temporal Properties of Processes introduces concurrent processes as terms of an algebraic language comprising a few basic operators, whose behaviours are described using transitions. The book describes how families of such transitions can be arranged as labeled graphs-themselves concrete summaries of the behaviour of processes-and how various combinations of processes and their resulting behaviour are determined by transition rules. An extensive use of games for both equivalence and model checking provides an approach that is more conceptually clear than generally employed alternatives.

Topics and features :

• Thorough treatment of process calculi for modeling concurrent systems
• Multiple verification techniques for showing temporal properties of systems
• Modal properties of systems and bisimulation equivalence presented in terms of games
• Introduction of modal mu-calculus as a general-purpose temporal logic
• Presentation of simple modal logics to aid in describing the capabilities of processes

Contents

• Processes
• Modalities and Capabilities
• Bisimulations
• Temporal Properties
• Modal Mu-Calculus
• Verifying Temporal Properties
• Exposing Structure
• References