Titlebook: Understanding Concurrent Systems; A.W. Roscoe Textbook 2010 Springer-Verlag London Limited 2010 Notation.Variable.communicating sequential

激怒

Further Operators .;. this happens when the first process terminates successfully via a special action ✓. In interrupt . this happens when the environment communicates an initial action of ., and in throw . any occurrence of an action in . within . counts as an exception which hands control to .. We study in particu

circumvent

Using FDRnd its functional sub-language which is roughly equivalent to Haskell. We see what FDR can and cannot do, and how to play to its strengths. For example we see—in an example based on finding a Hamiltonian path—how it is better to code complex systems as parallel compositions rather than as large sequ

Irrigate

边缘

Denotational Semantics and Behavioural Modelsequired of them. We see how CSP definitions of operators naturally lead to distributive operators, and discuss topics such as full abstraction and congruence with operational semantics. We look in detail at each of the traces, stable failures and failures divergences model, and understand their heal

N斯巴达人

Finite Observation Modelsinfinitely observable things to add to these. In this chapter we study what finite observation models exist. We examine the long-understood acceptances or ready-sets and refusal testing models. We discover two newer models: the acceptance-traces model of all finite linear observations, which is the

Eeg332

Infinite-Behaviour Modelsst of these, adding only divergence, can cope with finitely nondeterministic CSP with divergence strictness. The second, in which infinite traces and similar behaviours are added, can handle infinitely nondeterministic but divergence strict CSP. In the final class divergence strictness, or at least

obeisance

The Algebra of CSPrm, and therefore create an Algebraic Operational Semantics. Then we show how to reduce this to a normal form for the finest CSP model as developed in Chap. 12. We can then show how a small selection of optional laws such as . allow this normal form to be transformed into normal forms for any of the

发出眩目光芒

Timed Systems 1: ,-CSPls necessarily changes our understanding of the processes represented in this dialect. We develop a major new case study: the Bully algorithm for leadership election, and explain the use of the .-priority model that FDR uses to support timed analysis, implementing the principle of maximal progress.

粘

Timed Systems 2: Discrete Timed CSP the discrete variant of this, based on a semantic model involving . to record the passage of time, and show how it can be implemented in a variant of .-CSP. We use the alternating bit protocol as an example, and show how it relates to the more traditional continuous timed CSP through Ouaknine’s the

aviator

More About FDRd the other compression operators that FDR uses, the latter including types of bisimulation and the CSP-specific diamond operator. We then look at ideas for partial order reduction and “lazy compression” including the chase operator. We look at options for using parallel execution and improved memor