0 votes

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?

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

1 Answer

0 votes
 
Best answer

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.

by (93k points)
selected by

Related questions

0 votes
1 answer
asked Jan 26, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
0 votes
1 answer
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
...