Specification Language

Our specification language is linear temporal logic (LTL), with program point predicates $p$ as atomic propositions but omitting the type predicate $v : t$. The choice of linear temporal logic as the specification language, instead of for instance the modal $\mu$-calculus for which the model checking problem for our encoding into pushdown systems is also efficiently decidable, was solely motivated by the existence of the efficient model checker Moped [8] for LTL.

The operators of the logic are the standard ones. If $\phi$ and $\psi$ are formulas then so are $\neg \phi$, $\phi\wedge \psi$, $\phi\vee \psi$, ${\cal X} \> \phi$ and $\phi \>\; {\cal U} \>\; \psi$. The meaning of formulas is defined with respect to runs of infinite length $r \equiv c_0c_1c_2\ldots$. We let $r_i$ denote the suffix of $r$ starting in configuration $c_i$. Then satisfaction $r \mid\!= \phi$ of a formula $\phi$ by a run $r$ is defined as:

$r \mid\!= p$	iff	point $(c_0) : p$
$r \mid\!= \neg \phi$	iff	not $r \mid\!= \phi$
$r \mid\!= \phi\wedge \psi$	iff	$r \mid\!= \phi$ and $r \mid\!= \psi$
$r \mid\!= \phi\vee \psi$	iff	$r \mid\!= \phi$ or $r \mid\!= \psi$
$r \mid\!= {\cal X} \> \phi$	iff	$r_1 \mid\!= \phi$
$r \mid\!= \phi \>\; {\cal U} \>\; \psi$	iff	there is an $i\geq 0$ such that
		$r_i \mid\!= \psi$ and $r_j \mid\!= \phi$
		for all $0\leq j<i$

Henceforth let ${\sf false}$ abbreviate $p \wedge \neg p$ for some atomic predicate $p$, ${\sf true}$ abbreviate $\neg {\sf false}$, $\phi \Rightarrow \psi$ abbreviate $\neg \phi \vee \psi$, and $\mathsf{next}\;\phi$ abbreviate ${\cal X} \> \phi$ and $\phi\;\mathsf{until}\;\psi$ abbreviate $\phi \>\; {\cal U} \>\; \psi$. Further define $\mathsf{eventually}\;\phi \;\stackrel {\Delta}{=}\; {\sf true} \>\; {\cal U} \>\; \phi$ and $\mathsf{always}\;\phi \;\stackrel {\Delta}{=}\; \neg \left( \mathsf{eventually}\;\neg \phi \right)$. The weak until operator $\phi\;\mathsf{weakuntil}\;\psi$ abbreviates ${\phi}\;\mathsf{until}\;{\psi} \;\vee \; \mathsf{always}\;{\phi}$. Finally let $\mathsf{never}\;\phi \;\stackrel {\Delta}{=}\; \mathsf{always}\;\neg \phi$.

Given a PDS $\mathit{pds}$ let the notation $m \vdash \phi$ express the judgement that all runs starting in the entry program point of the method $m$ satisfy $\phi$. More formally:

Definition 4 (Model Checking a Method Call)   Given a PDS $\mathit{pds}$ with the single control location $p$ and a method $m$, the judgement $m \vdash \phi$ is valid iff for every run $r$ of the PDS $\mathit{pds'}$ from the initial configuration $\left< p, v\cdot \mathit{m\_\mbox{\texttt{loop}}} \right>$, $r \mid\!= \phi$ holds, where $v$ is the entry program point of method $m$ (i.e. $v :$   entry $m$), and $\mathit{pds'}$ is the PDS $\mathit{pds}$ extended with the fresh stack symbol $\mathit{m\_\mbox{\texttt{loop}}}$ and the single rewrite rule $\ensuremath{{\left< p, \mathit{m\_\texttt{loop}} \right>}\xrightarrow{{\scriptsize }}{\left< p, \mathit{m\_\texttt{loop}} \right>}}$ to achieve infinite runs.

The definition of a judgement $m \vdash \phi$ is motivated by the Moped tool which implements an algorithm for checking an initial configuration against an LTL formula.