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

965 questions

1.1k answers


451 users

0 votes

In the exam solution:

problem 4a

But can I do this:

=E[a SU b]

=F[a SU b] ------(as EF=E or F)

=Fb ---------------(as F[a SU b]=Fb)

=AFb ------------(as AF=F)

= mu x. b V []x ---------------(As  AFa=mu x. a V []x)

then do local model checking? like this-

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

2 Answers

+1 vote
Fist of all, no E[a SU b] is not (E)F[a SU b]. You cannot just replace E by EF.

Second of all: No, the simplifications would for example also simplify the graph of the local model checking. Thus, we couldn't see whether you can handle the features we wanted to be there.
by (25.6k points)
+1 vote
In general, you can simplify formulas, of course. However, your above simplifications don't make sense to me. E[a SU b] is not the same as F[a SU b], and Fb is not the same as AFb.
by (147k points)
Imprint | Privacy Policy