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

868 questions

986 answers

1.4k comments

438 users

0 votes

Exam : 15.02.2017 : Q 8 d part 2 : 2017.02.15.vrs.solutions.pdf (uni-kl.de)

Problem : Translate below formula to LO2 :

I am first using boolean operations for disjunction of two automaton.

Then I am just translating it to LO2 presented in lecture (Module 8 - Slide 25)

Q. Could you please check if the steps I am following is correct ?

Q. Also could you please check if the solution is correct ?

Thanks in advance.

Update : 25.08.2022

Final resultant in LO2 of Product automaton

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

1 Answer

+1 vote
 
Best answer

Well, there are many ways how you can solve this. As I can see, you used the sum automaton to compute the disjunction of the two automata, and then you translated the result to LO2. That is fine. 

However, you do not need the sum automaton here. The disjunction of universal automata is dual to the conjunction of existential automata, and for the latter, the simple product automaton would  be sufficient. Hence, you don't need an additional state variable.

I would have solved it as follows without modifying the automata:

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

by (139k points)
selected by
Thanks for the clarification and the property.
I have applied the product automaton and the final result I have updated in the problem.
I understood your solution as well.
Could you please let me know if my updated solution in the problem is also correct or not ?
I think that your new solution is also correct. As said, there are many ways how to solve this, and the formula can be simplified further if wanted. But there is no need to do so.
Yes totally got your point.
Thanks for the clarification :)

Related questions

0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...