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

928 questions

1k answers

1.4k comments

441 users

0 votes

Hello!. I am trying to solve this logic translation to CTL, as given in the solutions of the paper, dated 2021.02.17. 

In the 2nd step, F[d U b] was converted to FGd | Fb. But in the next step, AGd is written with a note at the bottom. Could anyone please explain how the reduction took place from step 2 to 3.?.

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

1 Answer

0 votes
 
Best answer
The claim is that (Gd & (FGd | Fb)) is equivalent to Gd. To see this, note first that Gd implies FGd since Gd demands that always d holds, and hence, it then holds also after any other point of time forever. Now, abbreviate p:=Gd, q:=FGd and r:=Fb and note finally that the following propositional logic formula is valid:

(p->q) -> (p & (q | r) <-> p)
by (143k points)
selected by
Thank you for the explanation. I get the idea now.

Just to confirm my understanding, would it be true if there is a formula in the given format: Gd & (FGd | <any path formula or state formula>), for example:

Gd & (FGd | GFa) or Gd & (FGd | [d U b])

The rule of (p->q) -> (p & (q | r) <-> p) would still apply?
Yes, it does still apply. As you wrote above the second formula in the disjunction can be any formula.
Thanks for the clarification.

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
Imprint | Privacy Policy
...