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

1.6k comments

538 users

+1 vote

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

1 Answer

+1 vote

Note that the delimiters [] are part of the binary temporal operators, so that in the formula [a SU b & EGa], the SU operator has the two arguments "a" and "b & EGa". 

In general, we have the following equivalences (VRS, Chapter 7, page 45): 

    * [φ1 SU ψ1] ∧ [φ2 SU ψ2] ⇔ [(φ1∧φ2) SU (ψ1∧[φ2 SU ψ2] ∨ ψ2∧[φ1 SU ψ1])]

    * [φ1 SU ψ1] ∧ [φ2 WU ψ2] ⇔ [(φ1∧φ2) SU (ψ1∧[φ2 WU ψ2] ∨ ψ2∧[φ1 SU ψ1])]

    * [φ1 WU ψ1] ∧ [φ2 WU ψ2] ⇔ [(φ1∧φ2) WU (ψ1∧[φ2 WU ψ2] ∨ ψ2∧[φ1 WU ψ1])]

Thus, we have in particular

    [a WU false] ∧ [true SU b] 
        ⇔ [(a∧true) SU (false∧[true SU b] ∨ b∧[a WU false])]
        ⇔ [a SU (b∧[a WU false])]
        ⇔ [a SU (b∧Ga)]

Finally, E[a SU (b∧EGa)] is a CTL formula, since the path quantifiers and temporal operators occur in pairs, i.e., we have E[.SU.] and EG as the CTL operators.

by (166k points)

Related questions

0 votes
1 answer
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
asked Aug 23, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
0 votes
1 answer
Imprint | Privacy Policy
...