This is a learning note of a course in CISPA, UdS. Taught by Swen Jacobs

Last post: Labeled Transition Systems

Processes

A Process is an LTS $P=(Q,Q_0,\mathrm{\Sigma },\delta ,\lambda )$ with $\mathrm{\Sigma }={\mathrm{\Sigma }}_{int}\cup \{ou{t}_a,i{n}_a\mid a\in {\mathrm{\Sigma }}_{sync}\}$, where

• ${\mathrm{\Sigma }}_{int}$ is a set of internal actions,
• ${\mathrm{\Sigma }}_{sync}$ a set of synchronizing actions,
• $ou{t}_a$ is an send action (or initiate action),
• $i{n}_a$ is an receive action.

Composition by Synchronization

The composition $P^n$ of $n$ (uniform) processes wrt. $card$ is the LTS $(S,S_0,{\mathrm{\Sigma }}_{int}\cup {\mathrm{\Sigma }}_{sync},\mathrm{\Delta },\mathrm{\Lambda })$ with:

• $S=Q\times Q$

• $S_0=Q_0\times Q_0$

• $\mathrm{\Delta }\subseteq S\times ({\mathrm{\Delta }}_{int}\cup {\mathrm{\Delta }}_{sync}\times S)$ is the set of all transitions that satisfy one of the following:

  Internal Transition:

  • For some $i\in \{1,\dots ,n\}$ , $(s,a,s^{\prime })\in S\times {\mathrm{\Sigma }}_{int}\times S$ is an element such that:
    $(s(i),a,s^{\prime }(i))\in \delta$ , and $s(j)=s^{\prime }(j)$ for $i\ne j\in \{1,\dots ,n\}$

  Process $s(i)$ take the action, other processes $s(j)$ remain their current states.

  Synchronous Transition

  • For some $i\in \{1,\dots ,n\}$ and some $I\subseteq \{1,\dots ,n\}\setminus \{i\}$ with $|I|\in card$ ,
    $(s,a,s^{\prime })\in S\times {\mathrm{\Sigma }}_{int}\times S$ is an element such that:

    • $s(i)\stackrel{ou{t}_a}{⟶}{s}^{\prime }(i)$ is (a local transition) in $P$

      One process $s(i)$ take the send action.

    • for every $j\in I,s(j)\stackrel{i{n}_a}{⟶}{s}^{\prime }(j)$ is (a local transition) in $P$

      $I$ is the set of processes that can take the receive action. (size of $I$ must not be larger then $card$)

    • for every $j\in \{1,\dots ,n\}\setminus (I\cup \{i\}),s^{\prime }(j)=s(j)$

      Other processes $s(j)$ that cannot take receive actions remain their current states.

    • $I$ is maximal.

      There does not exist a larger set $I^{\prime }\supset I$ with $|I^{\prime }|\in card$ that for all $j\in I^{\prime }$ ,
      there is a local transition from $s(j)$ that can take the receive action.

• $\mathrm{\Lambda }(s)=\{p_i\mid p\in \text{AP and p}\in \lambda (s(i)),i\in \{1,\dots ,n\}\}$

In this course, send action = $ou{t}_a$ = $a!!$ ; receive action = $i{n}_a$ = $a??$.

Example of Composition by Broadcast synchronization. $(card=\{1\})$

This is a learning note of a course in CISPA, UdS. Taught by Swen Jacobs

Labeled Transition Systems (LTS)

LTS is a concept in theoretical computer science used in the study of computation. It is used to describe the potential behavior of discrete systems, e.g. Model Checking.

It consists of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition. Mathematically, it can be described as directed graph.

Labels

Labels can be used to describe the behaviour or distinguish between states.
If the set of label is a singleton (only contains one label), then it can be omitted in the system.

LTS v.s. Finite-state Automata

In Transition systems:

• The set of states is not necessarily finite, or even countable.
• The set of transitions is not necessarily finite, or even countable.
• No “start” state or “final” states are given.

Formal definition