0.5 Using temporal logic to specify properties  (Page 2/11)

Trace

Given a state space automaton, a trace $$ (sometimes called an $$ -trace ) is a (possibly infinite) sequence of states ${}_0$ , ${}_1$ , ${}_2$ ,which respects the automaton's transtion relation $T$ .

Thus a trace is a path through the state space (as we have already seen ). Now that we have logic propositions associated with each state,we can see that during a trace, those propositions will change their truth value over time.We'll illustrate this with diagrams like the following.

In this example, $p$ and $q$ are propositions from $\mathrm{Prop}$ . Since in the trace $$ , we have $p$ being true at (for example) index 2, we write ${}_{2}p$ . In this diagram, it is also the case that ${}_0(pq)$ .

Although a bit unintuitive at first, it will be convenient to convert all finite traces into infinite ones.To do the conversion, we simply envision that once the automaton reaches its ostensibly last ( $n$ th) state, it languishes furiously in that state over and over:

Stutter-Extend

The finite trace ${}_0\text{,}\text{,}{}_n$ can be stutter-extended to the infinite trace ${}_0\text{,}\text{,}{}_n\text{,}{}_n\text{,}{}_n\text{,}$ .

To ensure this still satisfies the definition of a trace (where successive states must obey the automaton's transition relation),it is often assumed that every state has a transition to itself. Note that this convention precludes assuming that somethingmust change between one state and the next, which is plausible since we are modeling asynchronous systems.This will be reflected in our formal logic below, which will have no built-in primitive for ``the-next-state''.

State formulas

Now that we have a formal model of what a trace is, we can start to make formal statements about what happens in a trace.The simplest statements are state formulas , i.e. , propositional formulas built out of $\mathrm{Prop}$ . For a given trace $$ and state formula $$ , we can immediately decide whethera particular state ${}_i$ satisifes $$ (notationally, `` ${}_i$ '').