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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes

Hi,

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 (170k 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
...