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


543 users

0 votes

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



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 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 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 (166k 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
Imprint | Privacy Policy