Model checking

Model checking is a verification technique to determine if a system possesses a desired property. In our context a system is specified as a Petri net and a property is expressed as a temporal tree logic (CTL) or a linear temporal logic (LTL) formula. The model checking problem for a given PN and a formula f is to decide whether $ M_0 \models f$ or not.

Computational Tree Logic

CTL is a specification language for a propositional, branching-time temporal logic. The underlying set of atomic propositions consists of expressions considering markings, e.g. $ f = (M(p) > M(p\rq{}))$ is such an atomic proposition for $ p, p\rq{} \in P$ of PN. Every atomic proposition is a CTL formula; if $ f_1$ and $ f_2$ are CTL formulas, then so are
(a)
$ (f_1), \neg f_1, f_1 \wedge f_2, f_1 \vee f_2, f_1 \Rightarrow f_2, f_1 \Leftrightarrow f_2$ (with their usual meanings)
(b)
$ AF f_1, EF f_1, AG f_1, EG f_1, AX f_1, EX f_1, A[f_1 U f_2], E[f_1 U f_2]$
The temporal operators are nexttime (X), globally (G), sometime (or finally) (F) and until (U). A is the all path quantifier and E is the exists path quantifier.
$ AX f (EX f)$ intuitively means, that $ f$ holds in every (in some) direct successor $ y \in succ(x)$ of marking $ x$, resp. $ M_x$.
$ A[f_1 U f_2]$ intuitively means, that every path has an initial prefix $ \sigma$, such that $ f_1$ holds at all markings of $ \sigma$ apart from the last one and $ f_2$ holds for the last marking of $ \sigma$ ($ f_1$ holds, until $ f_2$ holds). $ E[f_1 U f_2]$ is analogously defined for some path.

Common abbreviations of CTL formulas, their definition and intuitive meanings are as follows:


$ AF f \equiv A[true U f]$ f is inevitable; finally f
$ EF f \equiv E[true U f]$ f potentially holds; f is possible
$ AG f \equiv \neg EF(\neg f)$ f is invariant; always f
$ EG f \equiv \neg AF(\neg f)$ f potentially holds always


Links

Model-Checking Kit of TU München

Lehrstuhl Informatik IV, Universität Dortmund
© 28.09.2001