Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


529 users

0 votes


I have some trouble interpreting the solution given to the problems in the exams. For example in the solution given below, I don't understand why did we add F!(a & b) as the formula itself looks like its equivalent to [!a SU (a & b)]. Generally, how should I start reading these formulas? also what does (to <= t2 < t1) & (!a t2) means? does it means that at time step t2  (!a) must hold whereas timestep t2<t1 which in turn can be interpreted as G(!a) ? 

in * TF "Emb. Sys. and Rob." by (1.4k points)

1 Answer

+1 vote
Best answer

I admit that this is not straightforward and requires a little trick. The solution given is correct which you can see as follows. 

At first we consider subformulas and try to match them with given "LTL templates". That does not work well here, but a formula which is close to the inner part would be

    ∃t1. t0≤t1 ∧ (a[t1] ∧ b[t1]) ∧ (∀t2. (t0≤t2 ∧ t2<t1 → ¬a[t2]))

which is the LO1 semantics of the LTL formula [¬a SU a ∧ b]. To simplify matters, let us now introduce the following abbreviations:

  •     alpha(t1)   := a[t1] ∧ b[t1]
  •     beta(t0,t1) := (∀t2. (t0≤t2 ∧ t2<t1 → ¬a[t2]))

so that the above formula becomes

    ∃t1. t0≤t1 ∧ alpha(t1) ∧ beta(t0,t1)

As already written above, that is close to what we actually need, i.e.,:

    ∃t1. t0≤t1 ∧ (alpha(t1) -> beta(t0,t1))

It is however possible to rewrite the above formula into the equivalent following form:

    ∃t1. t0≤t1 ∧ (alpha(t1) -> beta(t0,t1))
    = ∃t1. t0≤t1 ∧ (¬alpha(t1) ∨ beta(t0,t1))
    = ∃t1. t0≤t1 ∧ (¬alpha(t1) ∨ alpha(t1) ∧ beta(t0,t1))
    = ∃t1. t0≤t1 ∧ ¬alpha(t1) ∨ t0≤t1 ∧ alpha(t1) ∧ beta(t0,t1))
    = (∃t1. t0≤t1 ∧ ¬alpha(t1)) ∨ (∃t1. t0≤t1 ∧ alpha(t1) ∧ beta(t0,t1))

You can now clearly see that the second disjunct is the formula that we mentioned above, i.e., [¬a SU a ∧ b] and that the former disjunct is clearly F¬alpha, i.e., F¬(a ∧ b) (all evaluated at time t0). 

Having seen this, we now have

    ∀t0. 0≤t0 -> [F¬(a ∧ b) ∨ [¬a SU a ∧ b]](t0)

and that is clearly

   G(F¬(a ∧ b) ∨ [¬a SU a ∧ b])


by (166k points)
selected by

Related questions

0 votes
1 answer
asked Jun 17, 2020 in * TF "Emb. Sys. and Rob." by elly.yanakieva (150 points)
0 votes
1 answer
asked Feb 5, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
asked Jan 27, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
2 answers
0 votes
1 answer
Imprint | Privacy Policy