Automata, Games, and Verification (Portal)

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, \Sigma, \delta, \lambda)$ with $\Sigma = \Sigma_{int} \cup \lbrace out_a , in_a \mid a \in \Sigma_{sync} \rbrace $, where

• $\Sigma_{int}$ is a set of internal actions,
• $\Sigma_{sync}$ a set of synchronizing actions,
• $out_a$ is an send action (or initiate action),
• $in_a$ is an receive action.

Composition by Synchronization

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

• $S = Q \times Q$

• $S_0 = Q_0 \times Q_0$

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

  Internal Transition:

  • For some $i \in\lbrace 1, … , n \rbrace$ , $(s, a, s’) \in S \times\Sigma_{int}\times S$ is an element such that:
    $(s(i), a, s’(i)) \in\delta$ , and $s(j) = s’(j)$ for $i \ne j \in\lbrace 1, …, n \rbrace$

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

  Synchronous Transition

  • For some $i \in \lbrace 1, … , n \rbrace$ and some $I \subseteq \lbrace 1, …, n \rbrace \setminus \lbrace i \rbrace$ with $|I| \in card$ ,
    $(s, a, s’) \in S \times \Sigma_{int} \times S$ is an element such that:

    • $s(i) \buildrel out_a \over\longrightarrow s’(i)$ is (a local transition) in $P$

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

    • for every $j \in I, s(j) \buildrel in_a \over\longrightarrow s’(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\lbrace 1, …, n \rbrace \setminus (I \cup\lbrace i \rbrace), s’(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’ \supset I$ with $|I’| \in card$ that for all $j \in I’$ ,
      there is a local transition from $s(j)$ that can take the receive action.

• $\Lambda(s) = \lbrace p_{i} \mid p \in \text{AP and p} \in\lambda(s(i)), i \in \lbrace 1, …, n\rbrace \rbrace$

In this course, send action = $out_a$ = $a!!$ ; receive action = $in_a$ = $a??$.

Example of Composition by Broadcast synchronization. $(card = \lbrace 1 \rbrace)$

Synchronization Primitives

In this course, there are 4 types of synchronization:
Pairwise Rendezvous, Broadcast, Asynchronous Rendezvous, and Lossy Broadcast.

Pairwise Rendezvous

Exactly ONE process take $out_a$ action, ONE process take $in_a$ action. $(card = \lbrace 1 \rbrace)$

Broadcast

ONE process take $out_a$ action, ALL process take $in_a$ action if they are able to $(card = \mathbb{N}_0)$.

Asynchronous Rendezvous

ONE process take $out_a$ action, ZERO / ONE process take $in_a$ action $(card = {0, 1})$.

Lossy Broadcast

ONE process take $out_a$ action, ONE process take $in_a$ action $(card = \mathbb{N}_0, I\text{ not necessarily maximal})$.

---

Next post:

Further Reading: Synchronization, Parameterized Verification by Javier Esparza.

---

Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com