Exam Paper : 2020.02.19 : Question 7a

Question

For the below questions, what will be the Kripke Structures?

1. 

2. 

Another question is - How to cross-check our solution in these type of questions?  Can we do it using online tool, somehow?

Answer 1

For the first pair of formulas, see https://q2a.cs.uni-kl.de/1991/exam-2020-02-19-problem-7. The same counterexample is found in the solutions of the mentioned exam. It just given in text form since it is a single path instead of the graphical form that you can find under the above link.

For the second example, a Kripke structure would be the following one:

The above Kripke structure has been computed with the LTL tool https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html where the following formula was given

(b & X(!b & G F a)) -> (b & X(!b & G a))

Since this is not true, the tool comes up with a counterexample which will satisfy the negation of the above formula, i.e., 

(b & X(!b & G F a)) & !(b & X(!b & G a))

Hence, the above structure satisfies S1 and falsifies S2.