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

928 questions

1k answers


441 users

0 votes

Exam : 14.02.2018 : Q 9 c part 2 : * (

Problem : Translate the following to LO2 :

I am trying to solve like this :

But I am little bit confused :

Q1. Can I apply distributive law to Universal quantifier like I did above ?

I came up with F[Xa SU Gb] but this is not right as per the solution and also I can see both a and b holds at the same time t2.

Also if I see interval part a is true in future and not at current time so I made it as Xa.

And the structure of Tp2Od looks like Gb.

Q2. Could you please let me know where am I wrong ?

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

1 Answer

0 votes

The universal quantifier distributes over conjunctions, that is fine. If I am reading the exam problem correctly, the signals are applied to t1 instead of t2 which is unusual. At first I thought that this is a typo, but then I saw the in the same exam there is another problem with the other points of time.

For this one, I suggest the following reasoning: 

    ∃t0. (0≤t0 ∧ ∃t1. (t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → a[t1]) ∧ (t1≤t2 → b[t1]) )))
  = ∃t0. (0≤t0 ∧ ∃t1. (t0≤t1 ∧ ∀t2.(t0≤t2 ∧ t2<t1 → a[t1]) ∧ ∀t2.(t1≤t2 → b[t1]) ))
  = ∃t0. (0≤t0 ∧ ∃t1. (t0≤t1 ∧ ((∃t2.t0≤t2 ∧ t2<t1) → a[t1]) ∧ ((∃t2.t1≤t2) → b[t1]) ))
  = ∃t0. (0≤t0 ∧ ∃t1. (t0≤t1 ∧ (t0<t1 → a[t1]) ∧ (true → b[t1]) ))
  = ∃t0. (0≤t0 ∧ ∃t1. (t0≤t1 ∧ (t0<t1 → a[t1]) ∧ b[t1] ))
  = ∃t0. (0≤t0 ∧ ∃t1. (t0=t1 ∧ (t0<t1 → a[t1]) ∧ b[t1] or t0<t1 ∧ (t0<t1 → a[t1]) ∧ b[t1]))
  = ∃t0. (0≤t0 ∧ ∃t1. (b[t0] or t0<t1 ∧ a[t1] ∧ b[t1]))
  = ∃t0. (0≤t0 ∧ b[t0] or ∃t1. (t0<t1 ∧ a[t1] ∧ b[t1]))

This suggests now F(b | XF(a&b))

by (143k points)
@KS, I saw the lecture but couldn't find any direct formulas for the conversion involving LO1 and LO2. Am I missing something?

It would be great if you could help me with this.
LO1 is a subset of LO2, hence, there is no need for a conversion, and LO2 is strictly more powerful than LO1, so that there is no conversion that way. The above reasoning I made, was manually, and not done by an algorithm.

Related questions

0 votes
1 answer
0 votes
1 answer
asked Aug 24, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy