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:
Or semantics:
No comments:
Post a Comment