Scribd
Upload
4 views1 page

Model Checking Exercise and Kripke Models

The document describes an exercise on model checking a Kripke model M with 4 states and 6 transitions between states. Each state is labeled with a proposition. Students are asked to determine if 10 formula are true or false in the given Kripke model by checking if various states satisfy the formula. They are also asked to construct a Kripke model for the specification AG (requested → AF acknowledged).

Uploaded by

theresa.painter
Copyright
© Attribution Non-Commercial (BY-NC)
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
4 views1 page

Model Checking Exercise and Kripke Models

The document describes an exercise on model checking a Kripke model M with 4 states and 6 transitions between states. Each state is labeled with a proposition. Students are asked to determine if 10 formula are true or false in the given Kripke model by checking if various states satisfy the formula. They are also asked to construct a Kripke model for the specification AG (requested → AF acknowledged).

Uploaded by

theresa.painter
Copyright
© Attribution Non-Commercial (BY-NC)
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd

Exercise on Model Checking

1) Given the Kripke model M = ({t0, t1, t2, t3}, {(t0, t2), (t0, t1), (t1, t2), (t1, t3), (t2, t3), (t3, t3) }, L) where L(t0) = {p}, L(t1) = {q}, L(t2) = {r}, L(t3) = {q}.

Determine whether the following formulae are true or false. (10 %)

a) t0 |= Ep b) t0 |= A(q r) c) t0 |= EXAG(q) d) t1 |= EXAG(q) e) t0 |= EF(p U q) f) t0 |= EF((p r) U q) g) t0 |= AF(q) h) t2 |= EF(r) i) t1 |= E(q U r) j) t1 |= AX(q)

2) Construct the Kripke models for the following specifications AG ( requested AF acknowledged )

You might also like