Previous chapter: Model Checking

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Synthesis

In synthesis, we check automatically if there exists a program that satisfies a given specification.

If the answer is yes, we construct such a program.

We solve it by determine the winner of a two-player game between a system player and an environment player.

	Task	Goal
System player	choose the outputs of the system	meet the specification
Environment player	choose the inputs of the system	falsify the specification

Therefore, the specification is satisfied if the System player wins.
Such winning strategy can be translated into a program that is guaranteed to satisfy the specification.

Example: coffee machine

In this example, we assume there’s a machine that “outputs coffee” whenever users press a button.

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Model Checking

Given a system model, we try to check whether it meets its specification automatically and exhaustively.
To describe/represent the system and specification, we use Automata over infinite objects.

Verification Problem

The verification problem can be solved by:

Constructing the intersection of system, with an automaton for the negation of the specification,
then checking whether the language of the resulting automaton is empty.

$\textbf{Example 1.1. } \text{Consider the concurrent program }\small{\text{TURN}}:$
$$\text{local }t:\text{boolean where initially }t = false$$
$$P_0::\left[ \begin{array}{l}\text{loop forever do}\newline
\hspace{1cm}\left[ \begin{array}{l}
\ell_0: \text{await }\neg t; \newline
\ell_1: \text{critical;} \newline
\ell_2: t := true; \newline
\end{array} \right]\end{array} \right]
\mid\mid P_1::\left[ \begin{array}{l}
\text{loop forever do}\newline
\hspace{1cm}\left[ \begin{array}{l}
m_0: \text{await } t; \newline
m_1: \text{critical;} \newline
m_2: t := false; \newline
\end{array} \right]\end{array} \right]$$

The example above is a simple solution to the mutual exclusion problem:
it ensures that at any given point of time, at most one process is in the critical region.

From Program to automaton

To represent the above program using automaton, we need to define an alphabet $\Sigma$.

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)$

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