32^nd Spring School in Theoretical Computer Science

For the last 40 years, the theory of concurrency has been an active research area. Progressively, notions of time (or duration) have been added to models of concurrent systems. The definition by Alur and Dill of "timed automata" in the early nineties was a decisive step.
In this course we present several timed models used for modelling concurrent systems, focusing on problems with their parallel composition. We explain why timed automata have been a step forward in the modelling of reactive systems with timed constraints and we present their principal properties.

The notions of concurrency, causality and time have been a crucial aspect of reactive system design for years. Dealing with these three notions has become increasingly difficult as the complexity of the design grows. The synchronous programming model has had major successes for system level specification because it provides a simple way to access the power of concurrency in functional specification. Synchronous Languages like Esterel, Lustre, Signal, the Statecharts graphical notation, and design environments like Simulink/Stateflow all benefit from the simplicity of the synchronous assumption, i.e.: (1) the system evolves through an infinite sequence of successive atomic reactions indexed by a global logical clock, (2) during a reaction each component computes new events on output ports based on the presence/absence of events on input ports and, (3) communication of events among components occurs instantaneously.
However, if the synchronous assumption simplifies system specification, the problem of deriving a correct implementation from it does remain. In particular, difficulties arise when the target architecture has a distributed nature that does not match the synchronous assumption. This is the case for many important classes of applications in avionics, industrial plants, and the automotive industry. There, multiple processing elements operating at different paces are physically distributed and connected via asynchronous communication busses.
In this lecture, we present a simple and unified model of computation, based on heaps of pieces and related to Mazurkiewicz's trace theory. This model encompasses both synchronous and asynchronous models. Behaviour of synchronous systems is represented by heaps of rigid pieces, while asynchronous behaviour is represented by heaps of floppy pieces. Relations between these two models are investigated, with a particular focus on the composition of systems and properties such as confluence, equivalence or, preservation/reflection of concurrency.

The reachability problem asks whether we can reach a given state from some initial state. The decidability of this problem is a fundamental requirement, which we wish to be satisfied in any reasonable model used in the frame work of formal verification.
For Petri nets it was a long standing open problem until Mayr showed the reachability problem to be decidable in the beginning of 1980s. His proof turned out to be very complex, but nevertheless it is a mathematical nugget and its underlying techniques are widely applicable.
In my lecture I will present main steps in the proof. The presentation is based on the book of Reutenauer The mathematics of Petri Nets, Prentice Hall/Masson, 1990 (published first in French).

The automatic verification of finite state systems suffers from the explosion of states caused by the many possible permutations of concurrent events. Unfoldings are a verification technique that avoids this explosion by disregarding the order of concurrent events. It belongs to the group of so-called partial-order methods for model checking; it differs from other technqiues, like Valmari's stubborn sets or Peled's ample sets in the explicit use, also in the algorithms, of true concurrency structures.
Petri nets are a natural model for the unfolding approach, since they make concurrent events explicit, but the technique can be equally well applied to communicating automata. The behaviour of the Petri net is captured by unfolding of the net into an infinite acyclic occurrence net. The unfolding operation is similar to the unwinding of a finite automaton into an infinite acyclic automaton, but retains the concurrency aspects of the net.
The talk presents the basic theory of the unfolding technique, compares it with others, and comments on its application to different case studies.

In order to check whether a system meets its specifications, one needs first to describe formally the expected properties. When dealing with distributed, one usually consider the equivalent sequential system in order to use existing specification formalisms and tools. This sequentialisation suffers three main flaws: it involves a combinatorial blow-up, the very distributed nature of the system under consideration is lost, and some natural branching properties cannot be studied or even expressed. Therefore, distributed specification languages have been intensively studied in the recent past. We present first order and second order logics which serve as yardsticks for the expressivity of other formalisms. Then we introduce various temporal logics for partial orders and study their expressivity and complexity. Finally, we define simulation and bisimulation relations adapted to distributed systems.

The synchronous model is a very popular paradigm for real-time programming. This model was mainly studied in France, since almost 20 years, and several modeling and programming languages were based on this model. We will present two of these languages, Esterel and Lustre, which illustrate, respectively, the imperative and the data-flow programming styles. Specific problems concerning synchronous languages semantics and compilation will also be studied.

This talk introduces several classical models for concurrency such as Petri nets, asynchronous automata, Mazurkiewicz traces and event structures. Basic relationships between these models from algebraic, combinatorial, logical, and categorical points of view will be presented including Zielonka's theorem, Ochmanski's theorem, etc. Next, these basic models and classical results will related to other talks of this school. Occurrence nets, communicating automata, message sequence charts, and other extended formalisms will be discussed.

Message sequence charts (MSC) is a notation of the ITU (Z.120) that allows to describe telecommunication protocols in a concurrent manner. They visualize the interaction between processes or components of a system, that cooperate by means of asynchronous message exchange. MSCs are mostly used in early design stages, where they give an abstract view (scenarios) of the desired/undesired behavior of the system. This makes an early validation of properties crucial for the design process, since the verification tends to become more expensive on a detailed specification. Moreover, the abstract view of MSCs raises the problem of implementing the specification, e.g. on a network of communicating finite-state machines (CFM).
Contents :

• Expressivity of MSG and comparison with CFM.
• Model-checking and globally-cooperative MSG.
• Realizability of MSG by CFM, deadlocks, local choice.
• Related models: live sequence charts, netcharts, triggered MSC, template MSC.

A system consists of a process, of an environment and of possible ways of interactions between them. The synthesis problem is: given a specification, find a program for the process such that all behaviors of the system respect the given specification.
A distributed system has several processes; each of them interacts with the environment and with other processes. The distributed synthesis problem is now to find a program for each process such that the global behavior satisfies a given specification.
The lecture shall present several formalisms to describe synthesis problems. We will show a couple of decidability and undecidability results. The decidability results will be proved by reductions to game solvability problems. For distributed synthesis problems, we shall develop the model of distributed games.