0
$\begingroup$

A question gives me a set of atomic propositions AP = {a, b, c}and asks me to give a linear temporal property that represents all executions over AP such that:

(1) a and b never happen at the same time

OR

(2) a is preceded by c

Can anyone give me some pointers on how to answer this question (possibly with a model solution)? So far all I have done is split the property into two parts such that the property $P$ is the union of $P_1$ and $P_2$ but I don't know how to formulate my answer.

(This question is from a past exam paper).

Any help is highly appreciated.

$\endgroup$
  • 1
    $\begingroup$ Splitting the property is a good idea, since you have the $\vee$ operator to join them. Try to use LTL operators such as "Always" ($G$) and "until" $U$. The first one is pretty easy, the second requires some thought. What you tried so far? $\endgroup$ – Shaull Apr 17 '15 at 14:47
  • $\begingroup$ One issue with such natural language requirements is that they can be ambiguous - in particular, what exactly did the person setting this exam mean by "a is preceded by c"? Must c have held at some earlier state, or the immediately preceding one? If the latter, is that for all occurrences of a or just the first one? $\endgroup$ – Klaus Draeger Apr 17 '15 at 16:48
1
$\begingroup$

Since you are asked to formulate these properties in LTL, you might want to think of them as properties given with predicates over infinite sequences of states (or events where each event changes the state); in your case, you know that at each state some of the three propositions, {a, b, c} might be true.

When we talk about LTL, it's good to summarize what does the formalism support to figure out whether the given property can be formulated in it. Note that previously mentioned propositions are often formulated as state formulas, which might hold in a particular state. So, LTL supports: state formulas (propositions that might hold in particular state), (standard) Boolean operators (like logical or ||), and path quantifiers (like globally G and next X, which produce other state formulas), which effectively allow state formulas to describe sequences of states.

I will describe one potential solution in the "extended" LTL, which includes additional operators besides the fundamental ones. (These are easily expressible using only the basic operators, next and until; more details can be found in a more thorough treatment of LTL).

So far all I have done is split the property into two parts such that the property P is the union of P1 and P2 but I don't know how to formulate my answer.

Indeed, at the top level, as you recognized, you should have union, which effectively translates to || of P1 and P2:

P1 || P2

Going back to P1 ((1) a and b never happen at the same time), which states that something should never happen, it's good to think whether such temporal quantification can be translated to some of the offered quantifiers in LTL. This is indeed possible, and "never some property P" can be expressed in terms of combining a Boolean operator and a quantifier, in the following way:

G( not P ) (always, P is not true)

thus, P1 can be expressed by using given propositions as:

G( not (a && b) ) (always, it is not true that both a and b hold)

On the other hand, as Shaull pointed out, the second property is a bit trickier. Although, such a requirement might have been written more precisely (to avoid ambiguity), we can interpret it to mean that a and c should happen, at some point, such that c happened earlier than a.

Now, when we identified earlier, we might think of another LTL quantifier that semantically matches the notion of ordering states (or events). That quantifier is:

X (quantifier for next, i.e. formula that will hold in the next state)

Thus (under the interpretation that both propositions must be true at some point), we want to say that eventually, c happens, while at a point after that, eventually a happens as well:

F( c && X(F a))

arriving at the final solution:

P1 || P2 = (G( not (a && b) )) || F( c && X(F a))

which checks that either of the given properties are satisfied in the execution, as you originally suggested.

After you have an idea of how the formula should look like to makes sense (semantically, with respect to the property you want to model), you always want to check whether the formula is well formed, i.e. whether the formula is syntactically correct. (More details can be found in one of the more thorough treatments of LTL.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.