Model checking refers to the following problem: given a model of a system, test automatically whether this model meets a given specification.
0
votes
1answer
22 views
applying CTL/LTL model-checking on some system
I apologies if my title is vague, I'm trying to apply CTL/LTL model-checking on some system written in java, however, I still don't understand how to reach a result using either of the approaches ...
3
votes
0answers
46 views
Spot the formalism (some kind of process logic)
Consider the following specification technique.
A specification consists of a finite set of triples $\langle C, A, C' \rangle$,
where $A$ is the name of an action and $C, C'$ are conditions, that is,
...
3
votes
1answer
69 views
Looking for a book that derives and constructs a model checking application
I am teaching myself program verification and am currently learning proof assistants. I have the book Handbook of Practical Logic and Automated Reasoning which gives the proofs necessary for the ...
3
votes
1answer
103 views
Witness for the $EU(\phi_1,\phi_2)$ using BDDs
I wanted ask if you know an algorithm to find the witness for $EU(\phi_1,\phi_2)$ (CTL formula "Exist Until") using BDDs (Binary Decision Diagram). In pratice you should use the fixed point for ...
3
votes
1answer
65 views
Time to construct a GNBA for LTL formula
I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula:
Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ ...
6
votes
3answers
166 views
How can I decide manually whether two CTL formulae are equivalent?
Assume I have two formulae $\Phi$ and $\Psi$ (over the same set of atomic propositions $AP$) in CTL. We have that $\Phi \equiv \Psi$ iff $Sat_{TS}(\Phi) = Sat_{TS}(\Psi)$ for all transition systems ...
