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


538 users

0 votes


Translate E([a U b] ^ ¬ [c U d]) to CTL [2022.09.06 VRS].

Solution is given as


My approach is little bit different and I want to check the correct of this solution, 

E([a SU b] & ¬ [c SU d]) = 

                                 = EF([a SU b] & ¬ [c SU d]) used E = EF

                                 = EF(AG[a SU b] & AG[!c WB d]) used ![c SU d] = [!c WB d] and AG ->                                                                                                                                   vanishes, 

                                 = EF(AGA[a SU b] & AGA[!c WB d]) used AG = AGA 

Can we use Vanishes gives AG , since AG can be entirely removed? Does that make valid CTL?   EF(AGA[a SU b] & AGA[!c WB d]) is a valid CTL as per my understanding. 

in # Study-Organisation (Master) by (2.7k points)

1 Answer

0 votes
No, that is not correct. E is not equivalent to EF, so the first step is already incorrect. Also in the particular formula, the two formulas E([a SU b] & ¬[c SU d]) and EF([a SU b] & ¬ [c SU d]) are not equivalent.

Second, where do the AG operators in the second step come from?
by (166k points)
There is a formula in the cheat sheet, AG can be vanishes.  I thought, I can add AG to anywhere if Nothing is there.
AG -> Vanishes,
Vanishes->AG will it work in the reverse direction?
Which cheat sheet do you mean? AG cannot be simply added or removed. AG phi means that phi holds on all states reachable from a state s while phi just means that it holds on the current state s. That is a different formula!

Related questions

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