- Full Description
The book presents an extensive introduction to LOTOS highlighting how the approach differs from competitor techniques such as CCS and CSP. The notation is illustrated by a number of running examples and by using the LOTOS process calculus a spectrum of semantic models for concurrent systems are reviewed. Specifically, linear-time semantics; based on traces; branching-time semantics; using both labelled transition systems and refusals, are used to highlight true concurrency semantics using event structures. In addition to this a simple timed extension to LOTOS is introduced using running examples, allowing consideration of how the untimed semantic models – traces, labelled transition systems, refusals and event structures – can be generalised to the timed setting. The authors also generalise the simple communicating automata notation to yield timed automata with multi-way synchronisation using model-checking verification methods and new techniques to prevent time-locks from arising.
- Table of Contents
Table of Contents
- Background on Concurrency Theory.
- Concurrency Theory, Untimed Models.
- Process Caculi: LOTOS.
- Basic Interleaved Semantic Models.
- True Concurrency Models: Event Structures.
- Testing Theory and the Linear Time, Branching Time Spectrum.
- Concurrency Theory – Further Untimed Notations.
- Beyond pbLOTOS.
- Comparison of LOTOS with CCS and CSP.
- Communicating Automata.
- Concurrency Theory – Timed Models.
- Timed Process Calculi, a LOTOS Perspective, Semantic Models for tLOTOS.
- Timed Communication Automata.
- Timelocks in Timed Automata.
- Discrete Timed Automata.
Please Login to submit errata.No errata are currently published