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.)