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
Hello Professor, could you please clarify my understanding of the above formula:

I read the above as : On all paths , eventually there is 'a' and thereafter on all paths from 'a', the next state should also be 'a'. That is , in case there are multiple paths from the state that holds 'a', then all those paths should also have the next state as 'a'. If not the above statement is false.

Thanks a lot.
in * TF "Emb. Sys. and Rob." by (120 points)

1 Answer

0 votes

First of all, the portal should be a q2a system for everyone not just a professor is speaking to students, also students can communicate and discuss with other students. To that end, the users are anonymous as I am, too. wink

You explain the formula as it is, I can't do better. Maybe just note that "paths" means always "infinite paths" in temporal logics. Also have a look at slide 38 in the temporal logic chapter, where that formula is also discussed. 

by (139k points)
Thank you for the clarification. I was trying to understand the following but I am getting confused in this. How should I interpret this formula:
E((Fq) ∧ EG(p ∧ ¬q)) after looking at the answer in the following paper: https://es.cs.uni-kl.de/teaching/vrs/exams/2020.02.19.vrs/2020.02.19.vrs.solutions.pdf (page: 22)
Could you please help me with this?
Consider the inner formula EG(p∧¬q) first, and observe that it holds on s0,s1. Then label these states with a new variable x and consider E((Fq) ∧ x). It holds on state s0 that satisfies x and has a path where eventually q holds, namely the path from s0 to s2. Moreover, consider EF(q ∧ x) which holds in none of the states since q ∧ x holds in none of the states.

Related questions

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