Formal Methods Paparazzi: September 2014

Tuesday, September 30, 2014

Temporal Logic - LTL - 3

In this post we'll see the formal semantics of LTL (LTL - 1, LTL - 2, LTL - Literature):

The model is represented by

$\langle S, I, R, L\rangle$ where

$S$ is the set of states,

$I \subseteq S$ is the set of initial states,

$R:SxS$ is the relation transition definition and

$L: S \rightarrow 2^{AP}$ is the labeling definition where AP is the set of available atomic propositions.

In the example of the last post:

We have three states,

$S = \{s_0,s_1,s_2\}$ , with

$I = \{s_0\}$ ,

$R = \{(s_0,s_1), (s_1,s_2), (s_2, s_2)\}$ ,

$L = \{s_0\mapsto\{p\},s_1\mapsto\{q\},s_2\mapsto\{p,q,r\}\}$ .

A path is an infinite path

$\pi=\pi_0\pi_1\dots$ where

$\pi_0 \in I$ and for every

$i$ ,

$(\pi_i,\pi_{i+1})\in R$ . That is, the first state of the path is an initial state of the model, and for every two consecutive states of the path, there is a relation between them.

Now we define the semantics for the boolean operations and the temporal operators we have mentioned.

$\pi,i\vDash q$ with

$q \in AP$ if and only if

$q \in L(\pi_i)$ . That is, given a path

$\pi$ and index

$i$ of a state within the path an atomic proposition

$q$ is satisfied if and only if

$q$ belongs to the labels of that state.

$\pi,i\vDash \neg \varphi$ if and only if

$\pi,i\not\vDash \varphi$ . That is, not a formula is satisfied if the formula itself is not satisfied.

$\pi,i\vDash \varphi \land \theta$ if and only if

$\pi,i\vDash \varphi$ and

$\pi,i\vDash \theta$ . That is, the conjunction of two linear temporal logic formulas

$\varphi,\theta$ is satisfied if and only if both formulas are satisfied.

$\pi,i\vDash \varphi \lor \theta$ if and only if

$\pi,i\vDash \varphi$ or

$\pi,i\vDash \theta$ . That is, the disjunction of two linear temporal logic formulas

$\varphi,\theta$ is satisfied if and only at least one of the formulas is satisfied.

Now, we show the semantics of the temporal operators G, F, X, U.

$\pi,i\vDash \textbf{G}\varphi$ if and only if for every

$j\ge i$ ,

$\pi,j\vDash \varphi$ , that is, every path starting with every state after

$i$ satisfies

$\varphi$ .

$\pi,i\vDash \textbf{F}\varphi$ if and only if exists

$j\ge i$ ,

$\pi,j\vDash \varphi$ , that is, there is a state in the future such that the path starting with that state satisfies

$\varphi$ .

$\pi,i\vDash \textbf{X}\varphi$ if and only if

$\pi,i+1\vDash \varphi$ , that is, there is the next state satisfies

$\varphi$ .

$\pi,i\vDash \varphi\textbf{U}\theta$ if and only if exists

$j\ge i$ ,

$\pi,j\vDash \theta$ and for every

$i\le k < j$ ,

$\pi,k\vDash \varphi$ , that is, there is a state

$j$ in the future such that the

$\theta$ is satisfied, and every state till

$j$ (non-including) satisfies

$\varphi$ .

Or semantics:

Meeting of the Sussex Border Path with Hook Street at Monckton Hook (Andy Potter) / CC BY-SA 2.0

Thursday, September 25, 2014

Temporal Logic in Literature

In this post I want to put some phrases from Literature and show (possible) translation to temporal logic (LTL - 1, LTL - 2).

1)
"In such terms Mr Gradgrind always mentally introduced himself, whether to his private circle of acquaintance, or to the public in general." Charles Dickens, Hard Times, Chapter 2

Let's compare these two formulas:

$F (MrGradgrindMentallyIntroducesHimself)$

$G (MrGradgrindMentallyIntroducesHimself)$

The first one indicates that there is one state in the future in which Mr. Gradgrind mentally introduces himself. The second one indicates that this occurs at every state, matching the keyword always in the sentence.

2)
"There will be the noise of the blows of the whip, which they will give to the horses." Alexandre Dumas, The forty-Five Guardsmen, Chapter 1

Let's compare these two formulas:

$F\ noiseBlowsOfWhip \land F\ whipToHorses$

$F (noiseBlowsOfWhip \land whipToHorses)$

The first one indicates that there is a state in the future in which there is the noise of the blows of the whip, and there is state in the future in which they whip the horses, while the second one indicates a state in the future in which both things occur. Since we know that both things are related, the whip causes the noise, we know they must be at the same state, and the second formula is preciser.

3)
' This proposal met with general applause, until an old mouse got up and said: "That is all very well, but who is to bell the Cat?" ' Aesop, Aesop's fables, Belling the Cat

A first attempt could to be to write the following formula:

$Applause \land OldMouseQuestion$

However, this formula expresses that at the first instant of time both things occur, and the applause may happen later and even later the question. Thus, we may attempt to correct the formula as follows:

$Applause \land F\ OldMouseQuestion$

It is better in that it expresses that first the applause occurs and sometime in the future the question by the old mouse. However, the applause goes only to be interrupted by the old mouse (keyword: until). Then we correct it as follows:

$Applause\ U\ OldMouseQuestion$

Here represents that the applause goes on until the old mouse asks its question. The only ambiguous part that remains is whether the story starts with the applause or this happens at some moment in the future. Due to our additional knowledge that first there is a discussion, then the proposal to bell the cat and only then the applause, we know that this part does not occur at the first state:

$F\ Applause\ U\ OldMouseQuestion$