Project-Team-Triskell:Mathematical foundations for distributed and reactive software

Project-Team : triskell

Section: Scientific Foundations

Keywords: Labeled transition systems, partial orders, event structures.

Mathematical foundations for distributed and reactive software

Transition systems

A labeled transition system (or LTS) is a directed graph which edges, called transitions, are labeled by letters from an alphabet of events. The vertices of this graph are called states. A LTS can be defines as a tuple $Im1 ${{M=(}Q^M,A,T^M\#8834 Q^M×A×Q^M,q_{init}^M{)}}$$ , in which Q^M is a set of states, q_init^M is an initial state, A is a set of events, T^M is a transition relation.

Note that from this definition, the set of states in a LTS s not necessarily finite. Usually, the term finite state automata is used to designate a LTS with a finite set of states and events. In fact, automatas are the simplest models than can be proposed. They are often used to model reactive (and usually distributed) systems. Within this framework, events represent the interactions (inputs and outputs) with the environment. The term input/output LTS (IO-LTS) is often used to designate this kind of automata.

Labeled transition systems are obtained from reactive systems specifications in high-level description languages such as uml. The construction of a LTS from a specification is done using an operational semantics for this language, which is usually formalized as a deduction rules system. For simple languages such as process algebras (like CCS ), operational semantics can be defined using less than axioms and inference rules, while for notations such as UML, semantics would be defined in more than 100 pages.

For performance reasons, these operational semantics rules are never used directly, and are subject to several transformations. For example, the way states are encoded is an efficiency factor for LTS generation.

Computation of transformations of LTS can be resumed to search and fix-point calculus on graphs. These calculi can be performed either explicitely or implicitly, without an exhaustive calculus or storage of a LTS.

Classical algorithms in language theory build explicitely finite state automatas, that are usually integrally stored in memory. However, for most of the problems we are interested in, exhaustive construction or storage of an LTS is not mandatory. Partial construction of an LTS is enough, and strategies similar to lazy evaluation in functional programs can be used: the only part of LTS computed is the part needed for the algorithm.

Similarly, one can forget a part of a LTS previously computed, and hence recycle and save memory space. The combination of these implicit calculus strategies allow the study of real size systems even on reasonably powerful machines.

Non interleaved models

One of the well known drawbacks of LTSs [45] is that concurrency is represented by means of behaviors interleaving. This is why LTS, automatas and so on are called ``interleaved models''. With interleaved models, a lot of memory is lost, and models represented can become very complex. Partial order models partially solve these problems.

A partial order is a tuple $Im2 ${(E,\#8804 ,\#928 ,\#981 ,\#931 ,I)}$$ in which:

E represents a set of atomic events, that can be observable or not. Each event is the occurrence of an action or operation. It is usually considered that an event is executed by an unique process in an system.
$\le$ is a partial order relation that describes a precedence relation between events. This order relation can be obtained using the hypotheses that:
1. processes are sequential : two events executed by the same process are causally ordered.
2. communications are asynchronous and point to point: the emission of a message precedes its reception.
$\sigma$ is an alphabet of actions.
I is a set of process names
$\Pi$ : $\Sigma$ $\rightarrow$ I is an action placement function.
$Im3 ${\#981 :E\#8594 \#931 }$$ is an event labeling function

A partial order can be used to represent a set of executions of a system in a more ``compact'' way than interleaved models. Another advantage of partial order models is to represent explicitely concurrency : two events that are not causally dependant can be executed concurrently. In a LTS, such a situation would have been represented by an interleaving.

A linearization of a partial order is a total order that respect the causal order. Any linearization of a partial order is a potential execution of the system represented. However, even if partial order can represent several executions, linearizations do not represent a real alternative. This problem is solved by a more complete partial order model called event structures.

A prime event structure [54] is a partial order equipped with an additional binary conflict relation. An event structure is usually defined by a tuple $Im4 ${(E,\#8804 ,\#9839 ,\#928 ,\#981 ,\#931 ,I)}$$ where:

$Im5 ${E,\#8804 ,\#928 ,\#981 ,\#931 ,I}$$ have the same signification as previously,
$Im6 ${\#9839 \#8838 E×E}$$ is a binary and symmetric relation that is inherited through causality ( $Im7 ${\#8704 e\#9839 e^\#8242 ,e\#8804 e^{\#8242 \#8242 }\#10233 e^{\#8242 \#8242 }\#9839 e^\#8242 }$$ ).

The conflict relation of an event structure defines pairs of events that can not appear in the same execution of the system represented, hence introducing alternative in partial orders. The potential executions of a system represented by an event structures are linearizations of conflict free orders contained in the structure. The main advantage of event structures is to represent at the same time concurrency and alternative in a partial order model. We think that these models are closer to human understanding of distributed systems executions than interleaved models.