Temporal specifications and ground induction problem

We assume that the language $\mathcal{T}\!\mathcal{L}$ of the first-order temporal logic is constructed in the standard way (see i.e. [HWZ00]) from a classical (non-temporal) first-order language $\mathcal{L}$ and a set of future-time temporal operators `$\lozenge$' (sometime), ` $\raisebox{-.2ex}{ \mbox{\unitlength=0.9ex \begin{picture}(2,2) \linethick... ...{2}} \put(0,0){\line(0,1){2}} \put(2,0){\line(0,1){2}} \end{picture}}}$' (always), and ` $\!\raisebox{-.2ex}{ \mbox{\unitlength=0.9ex \begin{picture}(2,2) \linethickness{0.06ex} \put(1,1){\circle{2}} % Draws circle with \par\end{picture}}}$' (in the next moment). Here, $\mathcal{L}$ does not contain equality or functional symbols. Formulae of $\mathcal{T}\!\mathcal{L}$ are interpreted in first-order temporal structures with constant domain. We assume the rigid semantics for the variables and constants. We assume also the standard notions of satisfiable and valid formulae (evaluated in initial worlds of temporal structures). A first-order temporal specification is a triple $<\mathcal{U},\mathcal{S},\mathcal{T}>$ where $\mathcal{U}$ and $\mathcal{S}$ are the universal part and the initial part, respectively, given by finite sets (conjunctions) of (nontemporal) first-order formulae, and $\mathcal{T}$ is the temporal part given by a finite set (conjunction) of temporal step formulae. A temporal step formula has the following form:

$$\forall \bar{x}\; (\varphi(\bar{x}) \rightarrow \!\raisebox{-... ...{2}} % Draws circle with \par\end{picture}}} \chi(\bar{x}))$$

where $\varphi$ and $\chi$ are first-order formulae with the (possibly empty) sequence of free variables $\bar{x}$. A temporal specification $<\mathcal{U},\mathcal{S},\mathcal{T}>$ is just a syntactical form of representation of the temporal formula $\raisebox{-.2ex}{ \mbox{\unitlength=0.9ex \begin{picture}(2,2) \linethick... ...(0,0){\line(0,1){2}} \put(2,0){\line(0,1){2}} \end{picture}}} \mathcal{T}$. If any temporal step formula of the specification $SP$ has one of the following forms: $\forall x \; (P(x) \Rightarrow \!\raisebox{-.2ex}{ \mbox{\unitlength=0.9ex \b... ....06ex} \put(1,1){\circle{2}} % Draws circle with \par\end{picture}}} R(x))$, or $p\Rightarrow \!\raisebox{-.2ex}{ \mbox{\unitlength=0.9ex \begin{picture}(2,2)... ...ss{0.06ex} \put(1,1){\circle{2}} % Draws circle with \par\end{picture}}} r$ , where $P$ and $p$ are unary (i.e. one-place) predicate symbol and propositional symbol, respectively, $R(x)$ and $r$ are boolean expressions composed from one-place predicates and propositional symbols, respectively, then the specification is called monodic [HWZ00,BDFL02]. Given a first-order temporal specification $SP$ and a ground first-order formula $\psi$, a ground induction problem is that where the validity of the formula $SP \rightarrow \raisebox{-.2ex}{ \mbox{\unitlength=0.9ex \begin{picture}(2,... ... \put(0,0){\line(0,1){2}} \put(2,0){\line(0,1){2}} \end{picture}}} \psi$ must be established