Linear Time (LT) Properties
- A linear-time property (LT property) over the set of atomic propositions $AP$ is a subset of $(2^{AP})^\omega$. Here, $(2^{AP})^{\omega}$ denotes the set of words that arise from the infinite concatenation of words in $2^{AP}$.
- An LT property is thus a language (set) of inifinite words over the alphabet $2^{AP}$.
- The closure of an LT property $P$ is the set of infinite traces whose finite prefiexs are also prefixes of $P$. The closure of LT property $P$ over $AP$ is defined by:
Invariants
- Invariants are LT properties that are given by a condition $\Phi$ for the states and require that $\Phi$ holds for all reachable states.
- An LT property $P_{inv}$ over $AP$ is an invariant if there is a propositional logic formula $\Phi$ over $AP$ such that:
$\Phi$ is called an invariant condition (or state condition) of $P_{inv}$.
- For Transition System (TS), $TS \models P_{inv}$:
- iff $trace(\pi) \in P_{inv}$ for all paths $\pi$ in $TS$
- iff $L(s) \models \Phi$ for all states $s$ that belong to a path of $TS$
- iff $L(s) \models \Phi$ for all states $s \in Reach(TS)$
Safety
- Safety property $P$ is defined as an LT property over $AP$ such that any infinite word $\sigma$ where $P$ does not hold contains a bad prefix. The latter means a finite prefix $\hat{\sigma}$ where the bad thing has happened, and thus no infinite word that starts with this prefix $\hat{\sigma}$ fulfills $P$.
- An LT property $P_{safe}$ over $AP$ is called a safety property if for all words $\sigma \in (2^{AP})^\omega \backslash P_{safe}$ there exists a finite prefix $\hat{\sigma}$ of $\sigma$ such that:
Any such finite word $\hat{\sigma}$ is called a bad prefix for $P_{safe}$. A minimal bad prefix for $P_{safe}$ denotes a bad prefix $\hat{\sigma}$ for $P_{safe}$ for which no proper prefix of $\hat{\sigma}$ is a bad prefix for $P_{safe}$
Liveness
- Do not constrain the finite behaviours, but require a certain condition on the infinte behaviours.
- An LT-property that does not rule out any prefix. Any finite prefix can be extended such that resulting infinte trace satisfies the liveness property under consideration.
- LT property $P_{live}$ over $AP$ is a liveness property whenever $pref(P_{live}) = (2^{AP})^*$.
Intersection of Safety and Liveness Properties
- The only LT property over $AP$ that is both a safety and a liveness property is $(2^{AP})^\omega$.
Fairness
- Fairness assumptions rule out infinite behaviours that considered unrealistic, and often necessary to establish liveness properties.
- Types of fairness contraints:
- Unconditional fairness: constrains the circumstances under which a process gets its turn infinitely often.
- Strong fairness: if an activity is infinitely often enabled, then it will be executed infinitely often.
- Weak fairness: if an activity is continously enabled, then it has to be executed infinitely often.
How to express fairness constrains?
Action-based
For state $s$, let $Act(s)$ denote the set of actions that are executable in state $s$, that is:
\[Act(s) = \{\alpha \in Act \mid \exists s' \in S. \ s -a\rightarrow s' \}.\]Then the unconditional, strong, and weak fairness can be difined as: For transition system $TS = (S, Act, \rightarrow. I, AP, L)$ withour terminal states, $A \in Act$, and infinite execution fragment $\rho = s_0 -\alpha_0 \rightarrow s_1 -\alpha_1 \rightarrow \dots$ of $TS$:
- $\rho$ is unconditionally $A$-fair whenever
- $\rho$ is strongly $A$-fair whenever
- $\rho$ is weakly $A$-fair whenever
Here, $\exists^{\infty} j$ stands for ‘‘there are infinitely many $j$’’ and $\forall^{\infty} j$ for ‘‘for nearly all $j$’’ in the sense of ‘‘for all, except for finitely many $j$’’.
- Strong (or unconditional) fairness assumptions are useful for solving contensions, and weak fairness is often sufficient for resolving the non-determinism that results from interleaving.
State-based (LTL) - atomic propositions
Let $\phi$ and $\psi$ be propositional logic formulae over $AP$.
- An unconditional LTL fairness constraint is an LTL formula of the form
- A strong LTL fairness condition is an LTL formula of the form
- A wak LTL fairness constraint is an LTL formula of the form
An LTL fairness assumption is a conjunction of LTL fairness constraints.
Satisfaction Relation for LTL with Fairness
Let $FairPaths(s)$ denote the set of all fair paths starting in $s$ abd $FairTraces(s)$ the set of all traces induced by fair paths starting in $s$. Formally, for fixed formula $fair$,
\[FairPaths(s) = \{ \pi \in Paths(s) \mid \pi \models fair\},\] \[FairTraces(s) = \{ trace(\pi) \mid \pi \in FairPaths(s) \}.\]These notions can be lifted to transition systems in the obvious way yielding $FairPaths(TS)$ and $FairTraces(TS)$. Hence, for state $s$ in transition system $TS$ (over $AP$) without terminal states, LTL formula $\varphi$, and LTL fairness assumption $fair$ let
\[s \models_{fair} \varphi \text{ iff } \forall \pi \in FairPaths(s). \ \pi \models \varphi\]and
\[TS \models_{fair} \varphi \text{ iff } \forall s_0 \in I. \ s_0 \models_{fair} \varphi.\]$TS$ satisfies $\varphi$ under the LTL fairness assumption $fair$ if $\varphi$ holds for all $fair$ paths that originate from some initial state.
Action-based vs. State-based
- The advantage of the action-based formulation of fairness assumptions is that many useful (and realizable) fairness assumptions can easily be expressed.
- Action-based fairness assumptions can always be ‘‘translated’’ into analogous LTL fairness assumptions, see P263 in Principle of Model checking.
- Hoever, a state-based LTL fairness assumption cannot always be represented as action-based fairness assumptions.
References
- Principle of Model Checking
- Lecture 5 Linear time properties: https://www.youtube.com/watch?v=RRdd-urEwDg
- https://www.youtube.com/watch?v=mlJcJrJVbKw
- https://www.youtube.com/watch?v=hH56r7tyCNg