We have a Boolean state (or world), in which a number of atomic propositions (AP) are true or false

We’d like to reason about discrete linear time, which is an infinite sequence of states $A_0,A_1....$ with state $A_0$ at time 0 being the current state (thus any propositional formula over the AP talks about $A_0$)

We’d next line to add temporal modalities, such as:

always A - $\square A$

eventually A - $\diamond A$

next A - $\circ A$

etc

These let us express other natural temporal properties such as infinitely often a - $\square\diamond a$

We are given a finite set AP of atomic propositions (boolean variables), Boolean connectives plus two temporal modalities:

$\circ$ - next

$U$ - until

A formula in LTL is defined by the following grammar (in which brackets are omitted)

$$\varphi:=\text { true }|a| \varphi_{1} \wedge \varphi_{2}|\neg \varphi| \bigcirc \varphi | \varphi_{1} U \varphi_{2}$$

where $a\in AP$ and $\varphi_1,\varphi_2$ are LTL formulae

Other modalities can be expressed, e.g.

$$\diamond a \stackrel{\text { def }}{=} \text { trueUa }$$

$$\square a \stackrel{\text { def }}{=} \neg \diamond \neg a$$

A world is labelled by the AP that are true in it, so it is just a letter from the alphabet $2^{AP}$ (the set of all subsets of AP)

A word $\sigma$ is an infinite sequence of worlds, i.e. $\sigma \in (2^{AP})^\omega$

The satisfaction relation, $\sigma \models \varphi$ where $\sigma = A_0A_1...$ is a word and $\varphi$ is a formula, recursively defined by

$$\begin{array}{ll}
\sigma \models true & \\
\sigma \models a & \text{iff } a\in A_0\\
\sigma \models \varphi_1 \land \varphi_2 & \text{iff } \sigma \models \varphi_1 \text{ and } \sigma \models \varphi_2\\
\sigma\models\lnot\varphi & \text{iff } \sigma\not\models \varphi\\
\sigma\models\circ \varphi & \text{iff } A_1\ldots \models \varphi\\
\sigma\models\varphi_1 \cup \varphi_2 & \text{iff there is } i\leqslant s.t. A_i...\models \varphi_2 \text{ and } A_j...\models \varphi_2 \text{ for all } 0\leqslant j<i
\end{array}$$

Note here that the bottom line feels like it should be phi 1 and phi 2, but this was what Stefan said and I will follow him blindly into the darkness.

The set of all words that satisfy a formula $\varphi$ is called $Words(\varphi)$

A transition system TS has:

A finite set of states S

A transition relation $\rightarrow \subseteq S\times S$, which is left-total (for every $s_1\in S$, there is $s_2\in S$ such that $s_1\rightarrow s_2$)

A set of initial states $I\subseteq S$

A finite set of atomic propositions AP

A labelling function $L:S\rightarrow 2^{AP}$

The transitions may be labelled by a finite set of actions Act, in which case the transition relation becomes $\rightarrow \subseteq S\times Act \times S$

A run of TS is an infinite sequence of states

$$S_0\rightarrow s_1 \rightarrow ...$$

where $s_0\in I$, which produces an infinite trace $\sigma \in (2^{AP})^\omega$, $\sigma=L(s_0)L(s_2...)$

The set of all possible traces of the TS is called $Traces(TS)$

Finally, TS satisfies $\varphi$, $TS\models \varphi$, if $Traces(TS)\subseteq Words(\varphi)$ i.e. if each trace of the TS satisfies the formula $\varphi$

Thus is is possible that $TS\not\models \varphi$ and $TS \not\models \lnot \varphi$

We are given a Transition System $\tau$ and an LTL $\varphi$, both over the same set of atomic propositions AP. The task is to decide if $\tau\models\varphi$

That is, if all runs of $\tau$ satisfy $\varphi$, i.e. $Traces(\tau)\subseteq Words(\varphi)$.

Equivalently

$$Traces(\tau)\cap \big((2^{AP})^\omega \backslash Words(\varphi)\big)=\varnothing$$

This is the same as

$$Traces(\tau)\cap Words(\lnot \phi)=\varnothing$$

So if both the runs of $\tau$ and the models of $\varphi$ are represented by Buchi Automata, we can construct the intersection and check for emptiness. If it is empty, reply that $\tau\models\varphi$, otherwise return $a,b\in (2^{AP})^*$ such that $ab^\omega$ is a run of $\tau$ that falsifies $\varphi$

**Transforming a TS into a Buchi Automaton**- easy - move each label from the state onto all outgoing transitions and introduce a new start state (of the automaton) instead of multiple ones (of the TS)**Constructing the intersection of two BA**- easy - take the product of the two BA and making sure that we alternate infinitely often between accepting states from the two**Checking a BA for emptiness**- easy - check if there is a non-trivial strongly connected component that contains an accepting state and is reachable from the start state**Transforming an LTL formulae into an equivalent BA**- difficult - Translate it into a generalised BA that has multiple sets of accepting states and the acceptance condition is that a state form each set is visited infinitely often. A GBA is however easily transformed into an equivalent BA**Negating a BA**- Difficult

A state has two components

A subset of the AP (that are true; all the other are false) that records the current world, which is the last input seen

A subset of all subformulae of the $\varphi$ that should be true in the future, from this state onward

- A state must be propositionally consistent. This takes care of all boolean connectives

A transition from $s_1$ into $s_2$ labelled by $a\in 2^{AP}$ is added if

The label $a$ matches the first component of the state $s_2$

The state $s_1$ has the subformula $\circ\psi$ iff the state $s_2$ has the subformula (or AP) $\psi$ - this takes care of the Next operator

Whether the state $s_2$ has the subformula $\varphi_1\cup \varphi_2$

The state $s_1$ has $\varphi_2$, or

The state $s_1$ has $\varphi_1$ and the state $s_2$ has $\varphi_1\cup \varphi_2$

This partly takes care of the until operator as it can be expanded as follows

$$\varphi_{1} \cup \varphi_{2} \rightarrow \varphi_{2} \vee\left(\varphi_{1} \wedge \bigcirc\left(\varphi_{1} \cup \varphi_{2}\right)\right)$$

The expansion $\varphi_{1} \cup \varphi_{2} \rightarrow \varphi_{2} \vee\left(\varphi_{1} \wedge \bigcirc\left(\varphi_{1} \cup \varphi_{2}\right)\right)$ doesn’t guarantee that $\varphi_2$ eventually happens. Thus, any infinite run that always has $\varphi_{1}\cup\varphi_{2}$ but ever $\varphi_{2}$ is inconsistent. We can prevent it, though, by insisting that every run has states that have $\varphi_{2}$ or haven’t $\varphi_{1}\cup \varphi_{2}$ infinitely often.