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

532 users

0 votes

Referring to Exam Paper : 2018.08.21 (Question 8c) and 2018.02.14 (Question 8c) respectively-

In the first question- Isn't it for S2, next state should be where 'a' must be true? So, the structure for S2 could be 'a with a loop'?

It would be helpful if you please explain both the questions.

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

1 Answer

0 votes
 
Best answer
A self-loop on a state labeled with a will neither satisfy S1 nor S2 in the first example.  The subformula !a& Xa holds on a path if in a state !a holds and on the successor state a holds. Hence, a must switch from false to true.

The formula a <-> X!a holds whenever there is a change on the truth value of a, i.e., if a switches from false to true as the above formula, but also if a switches from true to false. This is so, since a <-> X!a is equivalent to a&X!a | !a&Xa which contains the former formula. The past version of the X does not make a big difference here.

I guess the latter needs a bit more explanation: Looking at EXF((PWX!a)<->a), we can rewrite this to EFX((PWX!a)<->a) which is equivalent to  EF(!a<->X a)  and that is in turn equivalent to EF((!a&Xa | a&!Xa)), and also to EF(!a&Xa) | EF(a&!Xa) which makes S2 equivalent to S1 | EF(a&!Xa).

In the second case, we have EF((PWX!a)<->a) instead of EXF((PWX!a)<->a) and these two formulas are not equivalent as can be seen by the discussed structures. Note that PWX p holds initially for any p, and since a also holds on the single path in the second structure, (PWX!a)<->a holds initially on that single path, and thus also F((PWX!a)<->a) holds there. However, variable a never changes its value.
by (166k points)
edited by

Related questions

0 votes
1 answer
0 votes
1 answer
asked Jan 18, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
0 votes
1 answer
asked Jan 13, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
0 votes
2 answers
asked Jan 15, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
0 votes
1 answer
Imprint | Privacy Policy
...