On a Decidable Formal Theory for Abstract Continuous-Time Dynamical Systems

Abstract

We propose a decidable formal theory which describes high-level properties of abstract continuous-time dynamical systems called Nondeterministic Complete Markovian Systems (NCMS). NCMS is a rather general class of systems which can represent discrete and/or continuous evolutions in continuous time and which is sufficient for modeling a wide range of real-time information processing and cyber-physical systems (CPS). We illustrate the obtained results with a proof of the mutual exclusion property of a CPS which implements Peterson’s algorithm.

This work was supported in part by the research project No. 11BF015-02 “Formal specifications and methods of development of reliable software systems”, Taras Shevchenko National University of Kyiv, Ukraine.

1 Introduction

A large amount of computing systems used today act as agents interacting with physical processes. They are now frequently called cyber-physical systems [1, 2]. Examples include autonomous automotive systems, robotics, process control, medical devices, energy conservation, etc. [3]. Let us give some quotes from the Cyber-Physical Systems (CPS) concept map [4] by S.S. Sunder of NIST (USA), E.A. Lee of UC Berkeley (USA) and others:

“CPS integrates the dynamics of the physical processes with those of the software and networking, providing abstractions and modeling, design, and analysis techniques for the integrated whole” [4].

“Classical models of computation in computer science, rooted in Turing-Church theories for non-concurrent systems, and in nondeterministic transition systems and process algebras for concurrent systems, do not handle temporal dynamics well” [4].

“A key CPS challenge is to conjoin the engineering abstractions for continuous dynamics (such as differential equations) with computer science abstractions (such as algorithms)” [4].

Besides, the following research needs in CPS are outlined in [1]: Abstraction and Architectures, Distributed Computations and Networked Control, and Verification and Validation. With regard to the first aspect (Abstraction and Architectures) it is stated that

“Innovative approaches to abstraction and architectures that enable seamless integration of control, communication, and computation must be developed for rapid design and deployment of CPS” [1].

The mentioned challenges imply the importance of development of adequate system models of various levels of abstraction and generality with emphasis on system’s temporal behavior which should not be restricted to a purely discrete or purely continuous evolution.

Although not aimed specifically at solving the mentioned challenges, many concrete models that combine a discrete and continuous behavior in some way were studied in control theory, theory of differential equations, and computer science, e.g. variable structure systems [5–7], impulsive differential equations [8, 9], differential equations with discontinuous right hand sides [10], switched systems [11], hybrid control systems [12–16], hybrid automata [17–19], phase transition systems [20], hybrid reactive modules [21], hybrid I/O automata [22]. The mentioned models may be useful for solving certain CPS-related problems, but they do not handle well such important aspects of CPS as levels of abstractions and distributed organization. As a result, high-level properties of CPS (e.g. mutual exclusion of access to a shared resource by different components within a CPS) are difficult to validate (and even formalize) in such models.

A possible solution to this problem is application of temporal [23–26] and dynamic logics [27–29] which allow reasoning about continuous-time systems (e.g. Temporal Logic of Reals [23], Duration Calculus [25], Monadic Second Order Logic over the structure of boolean finitely variable signals [24], continuous-time interpretation of Temporal Logic of Action [30], Real-time Temporal Logic [31], Differential Dynamic Logic [29], etc.). One can specify common high-level properties of interest of CPS rather straightforwardly in such logics and prove them. However, for expressive logics of this kind [24, 27–29] the validity problem is known to be undecidable (which is frequently related to the undecidability of the reachability problem for various classes of hybrid systems), so the search for decidable but useful fragments is still a relevant topic of research. It should be noted that most logics (fragments) that are known to be decidable are concerned with reasoning about systems which satisfy a kind of a finite variability assumption (non-Zenoness) [24, 32]: discrete-valued time-varying quantities of interest associated with the system can be modeled as piecewise constant functions (with finite sets of discontinuities over each bounded time segment). Although this assumption is reasonable in many practical cases, some real-world systems have adequate mathematical models which violate it (the simplest example is a hybrid automaton with Zeno executions which models of the dynamics of a bouncing ball [33]). This makes the problem of investigation of decidable formal theories which allow reasoning about more general classes of continuous-time dynamical systems important.

In this paper we will define and prove decidability of one such formal theory. For this purpose we need to select a sufficiently general class of dynamical systems. As we are interested in high-level properties, we will require such dynamical systems to be abstract models of CPS (which do not reflect excessive details about their structure and operation). We will also use the following informal assumption: each logically possible realization of the run-time behavior of a CPS can be modeled as an evolution of a (single) global state in the global continuous time (although the global state and time may be treated as purely mathematical objects with no physical manifestation). This suggests that the overall behavior of a CPS can be modeled as a set of functions (trajectories) from the global time domain to the set of global states which represent logically possible realizations of the system’s run-time behavior. On the other hand, well-known types of continuous-time dynamical systems have associated sets of trajectories as functions from a time domain to a state space. So in this paper we will consider a dynamical system to be a model of a CPS, if its associated set of trajectories represents the set of possible run-time behaviors of this CPS.

Classes of continuous-time dynamical systems of various levels of generality were considered in many works [5, 34–44]. Classical approaches to the definition of a dynamical system, such as those proposed by A.A. Markov, V.V. Nemytskii and V.V. Stepanov [35] and others (an overview can be found in [43]) can be considered as axiomatizations of properties of systems described by differential equations. As was noted in the work [38], the following properties of ordinary differential equations were of main concern in various axiomatizations: (1) local existence of solutions, (2) indefinite prolongability (global existence) of solutions, (3) unicity of solutions, (4) autonomness (the right-hand side of the equation does not depend explicitly on time). However, in a number of works [5, 37–40, 43, 45, 46], etc., there was a tendency to remove some of these properties from basic assumptions and consider increasingly general classes of dynamical systems (a comparison of many such approaches is given in [43]). In particular, in [38] it was proposed to eliminate the properties (1)–(4) mentioned above from the axiomatization to obtain a far-reaching generalization of dynamical systems. Variants of such a generalization include the notion of a process [38, 47] and the (process-independent) notion of a solution system [38] by O. Hájek. Similar ideas also appeared in some other works [40, 43, 44]. The general notion of a solution system by O. Hájek was used as basis of a more restricted notion of a Nondeterminisitc Complete Markovian System (NCMS) introduced in [48] for the purpose of studying the relation between the existence of global and local trajectories of dynamical systems. A NCMS is associated with a set of trajectories which are partial functions on the non-negative real time domain which satisfies certain assumption [48]. Although the class of NCMS is more restricted than the class of solution systems, it is sufficient for representing a very general class of causal (nonanticipative) systems which interact with the external environment using continuous-time input and output signals [49, 50], so we assume it to be sufficient for high-level modeling of real-time information processing systems and cyber-physical systems. For the reasons mentioned above, we will assume that the class of NCMS is sufficiently general, does not impose restrictions on the dynamics like the finite-variability assumption, and is suitable as a class of high-level models of CPS.

In this paper we will define a language for expressing various essential properties of NCMS, define a language interpretation, and show that the associated formal theory (the set of sentences which are valid in all interpretations) is decidable. To prove the decidability result we will use a reduction to the decidability of the monadic second-order theory of order of the real segment $[0,1]$ with quantification over $F_{\sigma }$-subsets (countable unions of closed sets) which was proved by M.O. Rabin [51] (as a consequence of the decidability of $S2S$, the monadic second-order theory of two successors). Then we will describe an example of an application of the obtained results for proving the mutual exclusion property of a CPS which implements Peterson’s algorithm. This example is an extension of the approach to proving properties of distributed algorithms which was proposed in [52].

2 Preliminaries

2.1 Notation

We use the following notation: $\mathbb {N}=\{1,2,3,...\}$, $\mathbb {N}_{0}=\mathbb {N} \cup \{0\}$, $\mathbb {R}$ is the set of real numbers, $\mathbb {R}_+$ is the set of nonnegative real numbers, $f : A \rightarrow B$ is a total function from $A$ to $B$, $f: A \tilde{\rightarrow }B$ is a partial function from $A$ to $B$, $2^A$ is the power set of a set $A$, $f|_X$ is the restriction of a function $f$ to a set $X$. If $A,B$ are sets, then $B^A$ denotes the set of all total functions from $A$ to $B$ and ${}^AB$ denotes the set of all partial function from $A$ to $B$. For a function $f:A \tilde{\rightarrow }B$ the symbol $f(x) \downarrow$ ($f(x) \uparrow$) means that $f(x)$ is defined (respectively undefined) on the argument $x$. We do not distinguish formally the notion of a function and a functional binary relation. When we write that a function $f:A \tilde{\rightarrow }B$ is total or surjective, we mean that $f$ is total on $A$ specifically (i.e. $f(x)\downarrow$ for all $x \in A$), or, respectively, is onto $B$ (i.e. for each $y \in B$ there exists $x \in A$ such that $y=f(x)$). The domain and range of a partial function $f: A \tilde{\rightarrow }B$ are $dom(f)=\{x\,|\,f(x)\downarrow \}$ and $range(f)=\{y~|~\exists x~f(x) \downarrow \wedge ~ y=f(x)\}$ respectively (note that in some areas of mathematics and computer science, including category theory, it is assumed that the domain and range of a partial function from $A$ to $B$ are $A$ and $B$ respectively, but we do not follow this convention in this paper and instead use the definitions given above). For partial functions $f$, $g$,$f(x)\cong g(x)$ denotes the strong equality (where $x$ is a fixed value): $f(x) \downarrow$ if and only if $g(x) \downarrow$, and $f(x)\downarrow$ implies $f(x)=g(x)$. By $f \circ g$ we denote the functional composition: $(f \circ g) (x) \cong f(g(x)).$

By $T$ we denote the non-negative real time scale $[0,+\infty )$, equipped with a topology induced by the standard topology on $\mathbb {R}$ and by $Bool=\{true,false\}$ we denote the set of boolean values equipped with the discrete topology.

The symbols $\lnot$, $\vee$, $\wedge$, $\Rightarrow$, and $\Leftrightarrow$ denote the logical operations of negation, disjunction, conjunction, implication, and equivalence respectively.

2.2 Nondeterministic Complete Markovian Systems (NCMS)

Let $T = \mathbb {R}_+$ be the non-negative real time scale. Denote by $\mathfrak {T}$ the set of all intervals (connected subsets) in $T$ which have cardinality greater than one (i.e. which are non-empty and non-singleton sets).

Let $Q$ be a set (a state space) and $Tr$ be some set of functions of the form $s: A \rightarrow Q$, where $A \in \mathfrak {T}$. Let us call its elements trajectories.

Definition 1

[48, 49] A set of trajectories $Tr$ is closed under proper restrictions (CPR), if $s|_A \in Tr$ for each $s \in Tr$ and $A \in \mathfrak {T}$ such that $A \subseteq dom(s)$.

Definition 2

[48, 49]

• (1) A trajectory $s_1 \in Tr$ is a subtrajectory of $s_2 \in Tr$ (denoted as $s_1 \sqsubseteq s_2$), if $dom(s_1) \subseteq dom(s_2)$ and $s_1=s_2|_{dom(s_1)}$.

• (2) A trajectory $s_1 \in Tr$ is a proper subtrajectory of $s_2 \in Tr$ (denoted as $s_1 \sqsubset s_2$), if $s_1 \sqsubseteq s_2$ and $s_1 \ne s_2$.

The set $(Tr, \sqsubseteq )$ is a (possibly empty) partially ordered set (poset).

Definition 3

[48, 49] A CPR set of trajectories $Tr$ is

• (1) Markovian (Fig. 1), if for each $s_1, s_2 \in Tr$ and $t \in T$ such that

  $t=\sup dom(s_1)= \inf dom(s_2)$, $s_1(t)\downarrow$, $s_2(t)\downarrow$, and $s_1(t)=s_2(t)$,

  the following function $s$ belongs to $Tr$:

  $s(t) = s_1(t)$, if $t \in dom(s_1)$, and

  $s(t)=s_2(t)$, if $t \in dom(s_2)$.

• (2) complete, if each non-empty chain in $(Tr, \sqsubseteq )$ has a supremum.

Fig. 1.

Markovian property of NCMS. If one trajectory ends and another begins in a state $q$ at time $t$, then their concatenation is a trajectory.

Definition 4

[48] A nondeterministic complete Markovian system (NCMS) is a triple $(T, Q, Tr)$, where $Q$ is a set (state space) and $Tr$ (trajectories) is a set of functions $s: T \tilde{\rightarrow }Q$ such that $dom(s) \in \mathfrak {T}$, which is CPR, complete, and Markovian.

This is an intensional definition. An alternative extensional definition (or an overview of the class of all NCMS) can be given using the notion of an LR representation of NCMS which is described below.

Definition 5

Let $s_1, s_2 : T \tilde{\rightarrow }Q$. Then $s_1$ and $s_2$ coincide:

• (1) on $A \subseteq T$, if $s_1|_A=s_2|_A$ and $A \subseteq dom(s_1) \cap dom(s_2)$ (this is denoted as $s_1 \doteq _A s_2$);

• (2) in a left neighborhood of $t \in T$, if $t>0$ and there exists $t'\in [0,t)$ such that $s_1 \doteq _{(t',t]} s_2$ (this is denoted as $s_1 \doteq _{t-} s_2$);

• (3) in a right neighborhood of $t \in T$, if there exists $t'>t$, such that $s_1 \doteq _{[t,t')} s_2$ (this is denoted as $s_1 \doteq _{t+} s_2$).

Let $Q$ be a set. Denote by $ST(Q)$ the set of pairs $(s,t)$ where $s:A \rightarrow Q$ for some $A \in \mathfrak {T}$ and $t \in A$.

Definition 6

[48, 49] A predicate $p:ST(Q) \rightarrow Bool$ is called

• (1) left-local, if $p(s_1,t)\Leftrightarrow p(s_2,t)$ whenever $(s_1,t), (s_2,t) \in ST(Q)$ and $s_1 \doteq _{t-} s_2$, and, moreover, $p(s,t)$ whenever $t$ is the least element of $dom(s)$;

• (2) right-local, if $p(s_1,t)\Leftrightarrow p(s_2,t)$ whenever $(s_1,t), (s_2,t) \in ST(Q)$, $s_1 \doteq _{t+} s_2$, and, moreover, $p(s,t)$ whenever $t$ is the greatest element of $dom(s)$.

Denote by $LR(Q)$ the set of all pairs $(l,r)$, where $l:ST(Q) \rightarrow Bool$ is a left-local predicate and $r:ST(Q) \rightarrow Bool$ is a right-local predicate.

Definition 7

[49] A pair $(l,r) \in LR(Q)$ is called a LR representation of a NCMS $\varSigma =(T,Q,Tr)$, if $Tr=\{ s:A \rightarrow Q\,|\, A \in \mathfrak {T} \wedge (\forall t \in A~l(s,t) \wedge r(s,t)) \}.$

Theorem 1

[49, Theorem1]

• (1) Each pair $(l,r) \in LR(Q)$ is a LR representation of a NCMS with the set of states $Q$.

• (2) Each NCMS has a LR representation.

Although an LR representation of a given NCMS needs not be unique, there always exists a unique least LR representation.

Definition 8

The least LR representation $(l^*,r^*)$ of a NCMS $\varSigma =(T,Q,Tr)$ is a LR representation $(l,r)$ of $\varSigma$ such that $l^*(s,t) \Rightarrow l(s,t)$ and $r^*(s,t) \Rightarrow r(s,t)$ for all $(s,t) \in ST(Q)$.

Theorem 2

• (1) Each NCMS has a unique least LR representation $(l^*,r^*)$.

• (2) If $\varSigma =(T,Q,Tr)$ is a NCMS and $(l^*,r^*)$ is its least LR representation, then for all $(s,t) \in ST(Q)$,

  $$\begin{aligned}&l^*(s,t)\Leftrightarrow t=0 \vee (\exists t'\in (0,t)~s|_{(t',t]} \in Tr \cup \{s|_{\{t\}}\}); \\&\, r^*(s,t) \Leftrightarrow \exists t'\in (t,+\infty )~s|_{[t,t')} \in Tr \cup \{s|_{\{t\}}\}. \end{aligned}$$

Proof

(Sketch).

• (1) Let $\varSigma =(T,Q,Tr)$ be a NCMS. Let us define predicates $l^*:ST(Q) \rightarrow Bool$ and $r^*:ST(Q) \rightarrow Bool$ as follows: $l^*(s,t)$ if and only if $l(s,t)$ holds for each LR representation $(l,r)$ of $\varSigma$, and $r^*(s,t)$ if and only if $r(s,t)$ holds for each LR representation $(l,r)$ of $\varSigma$. It is easy to check that a pointwise conjunction of any non-empty set of left-local predicates on $ST(Q)$ is left-local and a pointwise conjunction of any non-empty set of right-local predicates on $ST(Q)$ is right-local. By Theorem 1, $\varSigma$ has a LR representation, so $l^*$ is left-local and $r^*$ is right-local, so $(l^*,r^*) \in LR(Q)$. Moreover, for any $A \in \mathfrak {T}$ and $s:A \rightarrow Q$, $l^*(s,t) \wedge r^*(s,t)$ holds for all $t \in A$ if and only if $l(s,t) \wedge r(s,t)$ holds for all $t \in A$ and all LR representations $(l,r)$ of $\varSigma$, i.e. if and only if $s \in Tr$. Thus $(l^*,r^*)$ is a LR representation of $\varSigma$ and is the least LR representation. Uniqueness of the least LR representation of a NCMS follows straightforwardly from its definition.

• (2) Let us introduce predicates $l_0,r_0:ST(Q) \rightarrow Bool$ such that for all $s,t$:

  $$\begin{aligned}&l_0(s,t) \Leftrightarrow t=0 \vee (\exists t'\in (0,t)~s|_{(t',t]} \in Tr \cup \{s|_{\{t\}}\}); \\&\, r_0(s,t) \Leftrightarrow \exists t'\in (t,+\infty )~s|_{[t,t')} \in Tr \cup \{s|_{\{t\}}\}. \end{aligned}$$

  Using the Markovian and CPR properties of $Tr$ is straightforward to show that $l_0$ is left-local, $r_0$ is right-local, and a function $s:T\tilde{\rightarrow }Q$ such that $dom(s) \in \mathfrak {T}$ belongs to $Tr$ if and only if $l_0(s,t) \wedge r_0(s,t)$ for all $t \in dom(s)$. Then $(l_0,r_0) \in LR(Q)$ and $(l_0,r_0)$ is a LR representation of $\varSigma$. Moreover, for any LR representation $(l,r)$ of $\varSigma$, it is easy to show that $l_0(s,t) \Rightarrow l(s,t)$ and $r_0(s,t) \Rightarrow r(s,t)$ for each $(s,t) \in ST(Q)$ by noting that $s \in Tr$ if and only if $l(s,t') \wedge r(s,t')$ for all $t' \in dom(s)$. Then $(l_0,r_0)$ is a least LR representation of $\varSigma$. From the item (1) of this theorem, a least LR representation of $\varSigma$ is unique, so $l_0 =l_*$ and $r_0=r_*$.

   $\square$

For each NCMS $\varSigma$ denote by $LR_{min}(\varSigma )$ the least LR representation of $\varSigma$. Let $LR^*(Q)$ be the set of all pairs $(l,r) \in LR(Q)$ such that for each $(s,t) \in ST(Q)$:

• (1) if $l(s,t)$ and $t$ is a non-minimal element of $dom(s)$, then there exists $t' \in (0,t)$ such that $l(s,t'') \wedge r(s,t'')$ for all $t'' \in (t',t)$;

• (2) if $r(s,t)$ and $t$ is a non-maximal element of $dom(s)$, then there exists $t'>t$ such that $l(s,t'')\wedge r(s,t'')$ for all $t'' \in (t,t')$.

Theorem 3

• (1) If $(l,r) \in LR^*(Q)$, then there exists a NCMS $\varSigma =(T,Q,Tr)$ such that $(l,r)=LR_{min}(\varSigma )$.

• (2) If $\varSigma =(T,Q,Tr)$ is a NCMS, then $LR_{min}(\varSigma ) \in LR^*(Q)$.

Proof

(Sketch).

• (1) Follows straightforwardly from Theorem 1(1) and Theorem 2.

• (2) Let $\varSigma =(T,Q,Tr)$ be a NCMS and $(l^*,r^*)=LR_{min}(\varSigma )$. Then $(l^*,r^*) \in LR(Q)$, $(l^*,r^*)$ is a LR representation of $\varSigma$, and from Theorem 2(2) it follows immediately that $(l^*,r^*) \in LR^*(Q)$.

   $\square$

NCMS can be used as an abstraction of concrete mathematical models. Some examples are given below. More examples (including various discrete-continuous models) can be obtained using Theorem 1.

Example 1

Let $d \in \mathbb {N}$, $Q = \mathbb {R}^d$, and $f:\mathbb {R} \times \mathbb {R}^d \rightarrow \mathbb {R}^d$. Let $Tr$ be the set of all functions $s:A \rightarrow Q$, $A \in \mathfrak {T}$ such that $s$ is locally absolutely continuous on $A$ (i.e. is absolutely continuous on every segment $[a,b]\subseteq A$) and satisfies the differential equation $\frac{ds(t)}{dt}=f(t,s(t))$ almost everywhere on $A$ (in the sense of Lebesgue measure), i.e. $s$ is a Caratheodory solution.

Then $(T,Q,Tr)$ is a NCMS.

The proof of this follows from the definition of NCMS.

Example 2

Let $(Q,\rightarrow )$ be a state transition system, i.e. $Q$ is a set and $\rightarrow \subseteq Q \times Q$ is a binary relation. Assume that $Q$ is equipped with the discrete topology (i.e. all subsets are open). Let $Tr$ be the set of all piecewise-constant left-continuous functions $s:A \rightarrow Q$ which for all non-maximal $t \in A$ satisfy the condition $s(t+) \downarrow$ and

$$ {\left\{ \begin{array}{ll} s(t+)=s(t), &{} t \notin \mathbb {N}_0, \\ s(t)\rightarrow s(t+),&{} t \in \mathbb {N}_0, \\ \end{array}\right. } $$

where $s(t+)$ denotes the right limit at $t$ (see Fig. 2).

Then $(T,Q,Tr)$ is a NCMS.

The proof of this follows from the definition of NCMS.

Fig. 2.

A trajectory which models an execution of a (discrete-time) state transition system $(Q,\rightarrow )$. At the integer time moments the system changes its current state $q$ to a next state $q'$ such that $q \rightarrow q'$.

3 Main Result

We will define a formal language in which one can express relations between a finite set of arbitrary distinguished trajectories and a finite set of arbitrary NCMS. In particular, membership of a distinguished trajectory in the set of trajectories of a given NCMS and certain forms of partial coincidence of a distinguished trajectory with one of the trajectories of a given NCMS can be expressed in this language. The partial coincidence of trajectories can be considered as a “pattern matching”-like mechanism for specification of the behavior of dynamical systems and proving their properties.

Taking into account the properties of NCMS mentioned in Sect. 2.2, testing the existence of a trajectory of a NCMS which coincides with a given function on a given time interval or in a neighborhood of a given time moment can be done rather straightforwardly using the least LR representation. This suggests that a language should be able to express in some form the components of the least LR representations of a NCMS. We implement this approach as follows.

Let $\mathcal {T}=\{t_i~|~i \in \mathbb {N}\}$, $\mathcal {C}=\{C_i~|~i \in \mathbb {N}\}$, and $\mathcal {F}=\{F_i~|~i \in \mathbb {N}\}$ be countable pairwise-disjoint sets of variable names (it is assumed that the symbols within each set are identified by their indices).

Let $\mathcal {A}$ be the set of all atomic formulas of the forms $D_{i}(t_k)$, $E^-_{i,j}(t_k)$, $E^+_{i,j}(t_k)$, $L_{i,j}(t_k)$, $R_{i,j}(t_k)$, $t_i<t_j$, $t_i=t_j$, $t_i \in C_j$, $t_i \in F_j$ ($i,j,k \in \mathbb {N})$, where $D_i$ for all $i \in \mathbb {N}$ and $E^-_{i,j}$, $E^+_{i,j}$, $L_{i,j}$, $R_{i,j}$ for all $i,j \in \mathbb {N}$ are distinct unary predicate symbols (identified by their indices) and $<$, $=$, $\in$ are binary predicate symbols.

Let $\mathcal {L}$ be the set of all well-formed (second-order) formulas (a formal language) composed of atomic formulas from $\mathcal {A}$, symbols of logical connectives ($\lnot$, $\wedge$, $\vee$, $\rightarrow$, $\leftrightarrow$), and variable names from $\mathcal {T}$, $\mathcal {C}$, $\mathcal {F}$ bound by existential and universal quantifier symbols ($\exists t_i$, $\forall t_i$, $\exists C_i$, $\forall C_i$, $\exists F_i$, $\forall F_i$).

Let $\mathcal {L}^c$ be the set of all sentences (closed formulas) in $\mathcal {L}$.

To define an interpretation of formulas, let us introduce the following notions and notations.

• $Cl(X)$ and $F_{\sigma }(X)$, where $X \subseteq \mathbb {R}$ is a nonempty set, denote the sets of all closed subsets and $F_{\sigma }$-subsets of $X$ respectively (in the sense of the induced topology on $X$).

• $\mathcal {S}$ is the set of all algebraic structures of the form

  $$\begin{aligned} (T,<,(D_i)_{i \in \mathbb {N}},(E^-_{i,j})_{i,j \in \mathbb {N}},(E^+_{i,j})_{i,j \in \mathbb {N}},(L_{i,j})_{i,j \in \mathbb {N}}, (R_{i,j})_{i,j \in \mathbb {N}}), \end{aligned}$$

  where $T=\mathbb {R}_+$, $<$ is the standard strict order on $T$, and $D_i$, $E^-_{i,j}$, $E^+_{i,j}$ $L_{i,j}$, $R_{i,j}$ for all $i,j \in \mathbb {N}$ are unary predicates on $T$.

• $\models \subseteq \mathcal {S}\times \mathcal {L}$ is a logical validity relation defined as follows: for each $\varPhi \in \mathcal {L}$ and $S=(T,<,(D_i)_{i \in \mathbb {N}},(E^-_{i,j})_{i,j \in \mathbb {N}},(E^+_{i,j})_{i,j \in \mathbb {N}},(L_{i,j})_{i,j \in \mathbb {N}}, (R_{i,j})_{i,j \in \mathbb {N}}) \in \mathcal {S}$, $S \models \varPhi$ if and only if the universal closure of $\varPhi$ holds in the structure $S$ under the interpretation which assumes that the variables $t_1,t_2,...$ range over $T$, the variables $C_{1},C_2,...$ range over $Cl(T)$, the variables $F_1,F_2,...$ range over $F_\sigma (T)$, the symbol $<$ is interpreted as the relation $<$ on $T$, the symbol $=$ is interpreted as the equality on $T$, the symbol $\in$ is interpreted as set membership, the symbols $D_i$, $E^-_{i,j}$, $E^+_{i,j}$, $L_{i,j}$, $R_{i,j}$, for $i,j\in \mathbb {N}$ are interpreted as the predicates $D_i$, $E^-_{i,j}$, $E^+_{i,j}$, $L_{i,j}$, $R_{i,j}$ on $T$ respectively.

• $\mathcal {M}$ is the class of all tuples $((s_i)_{i \in \mathbb {N}},(\varSigma _{i})_{i \in \mathbb {N}})$ such that there exists a set $Q$ (states) such that:

  • (1) for each $i \in \mathbb {N}$ $s_i:T \tilde{\rightarrow }Q$ ($i$-th distinguished trajectory) is a function such that $dom(s_i) \in \mathfrak {T} \cup \{\emptyset \}$ (note that a nowhere defined function is not a trajectory of any NCMS, but we allow it here for convenience);

  • (2) each $\varSigma _i$, $i \in \mathbb {N}$ is a NCMS with the set of states $Q$ ($i$-th distinguished NCMS).

  We will call the elements of $\mathcal {M}$ models (of formulas).

• A structure associated with $M=((s_i)_{i \in \mathbb {N}},(\varSigma _{i})_{i \in \mathbb {N}}) \in \mathcal {M}$ is a unique tuple $(T,<,(D_i)_{i \in \mathbb {N}},(E^-_{i,j})_{i,j \in \mathbb {N}},(E^+_{i,j})_{i,j \in \mathbb {N}},(L_{i,j})_{i,j \in \mathbb {N}}, (R_{i,j})_{i,j \in \mathbb {N}}) \in \mathcal {S}$ such that:

  • (1) $D_i(t) \Leftrightarrow t \in dom(s_i)$ for all $i,j \in \mathbb {N}$ and $t \in T$;

  • (2) $E^-_{i,j}(t) \Leftrightarrow s_i \dot{=}_{t-} s_j$ for all $i,j \in \mathbb {N}$ and $t \in T$;

  • (3) $E^+_{i,j}(t) \Leftrightarrow s_i \dot{=}_{t+} s_j$ for all $i,j \in \mathbb {N}$ and $t \in T$;

  • (4) $L_{i,j}(t)\Leftrightarrow l^*_i(s_j,t)$ and $R_{i,j}(t) \Leftrightarrow r^*_i(s_j,t)$ for each $i,j \in \mathbb {N}$ and $t \in dom(s_j)$, where $(l_i^*,r_i^*)=LR_{min}(\varSigma _i)$;

  • (5) $\lnot L_{i,j}(t)$ and $\lnot R_{i,j}(t)$ for all $i,j \in \mathbb {N}$ and $t \in T$ such that $t \notin dom(s_j)$.

  This structure is denoted as $St(M)$.

• $\models ^{m} \subseteq \mathcal {M}\times \mathcal {L}$ is a logical validity relation defined as follows: for each $\varPhi \in \mathcal {L}$ and $M \in \mathcal {M}$, $M \models ^{m} \varPhi$ if and only if $St(M) \models \varPhi$. This is interpreted as follows: $\varPhi$ is assumed to be valid in a model $M$ ($M \models ^{m} \varPhi$), if $\varPhi$ is valid in the structure associated with $M$.

• $Th = \{\varPhi \in \mathcal {L}^c ~|~\forall M \in \mathcal {M}~ M \models ^{m} \varPhi \}$ is a formal theory which consists of all sentences valid in all models.

In short, $Th$ consists of the sentences $\varPhi$ valid in all models $M \in \mathcal {M}$ which consist of a sequence of distinguished trajectories $(s_i)_{i \in \mathbb {N}}$ and a sequence of distinguished NCMS $(\varSigma _i)_{i \in \mathbb {N}}$ under the assumption that in $\varPhi$ the variables $t_1,t_2,...$ range over $T$, $C_{1}, C_2,...$ range over $Cl(T)$, $F_1,F_2,...$ range over $F_\sigma (T)$, the symbols $<$ and $=$ mean the standard strict order and equality on $T$, $\in$ means set membership, the atomic formula $D_i(t_k)$ means $t_k \in dom(s_i)$, $E_{i,j}^-(t_k)$ means $s_i \dot{=}_{t_k-} s_j$, $E_{i,j}^+(t_k)$ means $s_i \dot{=}_{t_k+} s_j$, and $L_{i,j}(t_k)$, $R_{i,j}(t_k)$ mean that $s_j(t_k) \downarrow$ and $l_i^*(s_j,t_k)$ and $r_i^*(s_j,t_k)$ hold, where $(l_i^*,r_i^*)=LR_{min}(\varSigma _i)$.

Informally, the formulas in $Th$ express valid relations between trajectories and NCMS that hold for arbitrary distinguished trajectories and arbitrary NCMS.

Theorem 4

The formal theory $Th$ is decidable.

We will prove this theorem in the next section.

4 Proof of Decidability

In this section we give a proof of Theorem 4 using a series of lemmas.

Definition 9

A predicate $P: T \rightarrow Bool$ is called

• right-stable, if for each $t \in T$, $P(t)$ implies that there exists $t'>t$ such that $P(t'')$ holds for all $t'' \in [t,t')$;

• left-stable, if for each $t \in T\backslash \{0\}$, $P(t)$ implies that there exists $t'< t$ such that $P(t'')$ holds for all $t'' \in (t',t]$.

Note that a truth set of a predicate is the set of arguments on which it holds.

Lemma 1

• (1) The truth set of a right-stable predicate is an $F_{\sigma }$-set.

• (2) The truth set of a left-stable predicate is an $F_{\sigma }$-set.

Proof

• (1) Let $P: T \rightarrow Bool$ be right-stable and $A = \{t~|~P(t)\}$ be the truth set of $P$. Then for each $t \in T$ there exists $b(t)>t$ such that $P(t)$ implies $P(t')$ for all $t' \in [t,b(t))$. Then $A = \bigcup _{t \in A} [t,b(t))$ is an open set in the sense of the Sorgenfrey (right half-open interval) topology on $\mathbb {R}$ [53]. The latter topology is hereditarily Lindelöf [53], which implies that every open cover of $A$ (as an open subspace of the Sorgenfrey line) has a countable sub-cover. The sets $\{[t,b(t))~|~t \in A\}$ form an open cover of A in this sense, so there is a countable subset $C \subseteq \{[t,b(t))~|~t \in A\}$ such that $A = \bigcup C$. All elements of $C$ are $F_{\sigma }$ sets in the sense of the topology on $T$, so $A$ is an $F_{\sigma }$-set in the same sense.

• (2) Analogous to the proof of the item (1).

   $\square$

One of the consequences of the theorem on the decidability of $S2S$ by M.O. Rabin is decidability of a second order theory of a real segment $[0,1]$ with quantification over closed subsets and over $F_{\sigma }$-subsets [51].

More specifically, let $\mathcal {A}^2_<$ be the set of atomic formulas of the forms $t_i<t_j$, $t_i=t_j$, $t_i \in C_j$, $t_i \in F_j$ ($i,j \in \mathbb {N}$), where $t_i \in \mathcal {T}, C_i \in \mathcal {C}, F_i \in \mathcal {F}$ and $<$, $=$, $\in$ are binary predicate symbols.

Let $\mathcal {L}^2_{<}$ be the set of all well-formed (second-order) formulas composed of atomic formulas from $\mathcal {A}^2_<$, symbols of logical connectives ($\lnot$, $\wedge$, $\vee$, $\rightarrow$, $\leftrightarrow$), and variable names from $\mathcal {T}$, $\mathcal {C}$, $\mathcal {F}$ bound by existential and universal quantifier symbols ($\exists t_i$, $\forall t_i$, $\exists C_i$, $\forall C_i$, $\exists F_i$, $\forall F_i$).

For each nonempty set $X \subseteq \mathbb {R}$ let $Th^2_<(X)$ be the set of all sentences (closed formulas) in $\mathcal {L}^2_{<}$ which are valid in the structure $(X, <_{X})$, where $<_{X}$ is the restriction of the standard order on reals to $X$, under the interpretation which assumes that $t_1, t_2$,... range over $X$, the variables $C_1, C_2$,... range over $Cl(X)$, $F_1, F_2$,... range over $F_{\sigma }(X)$, the symbol $<$ is interpreted as $<_X$, the symbol $=$ is interpreted as equality on $X$, and the symbol $\in$ is interpreted as set membership.

Lemma 2

The theory $Th^2_<(T)$ is decidable.

Proof

(Sketch). The theory $Th^2_<([0,1])$ is known to be decidable [51, Theorem 2.9]. Using this result it is straightforward to prove that $Th^2_<([0,1))$ is decidable, because in the language $\mathcal {L}^2_{<}$ one can express the following predicates $P_1$, $P_2$, the truth sets of the interpretations of which are $Cl([0,1))$ and $F_{\sigma }([0,1))$:

$$\begin{aligned} P_1(C_1) := \forall t_1 ~ (t_1 \in C_1 \rightarrow (\exists t_2 ~ t_1 < t_2)); \\ P_2(F_1) := \forall t_1 ~ (t_1 \in F_1 \rightarrow (\exists t_2 ~ t_1 < t_2)). \end{aligned}$$

Taking into account that any continuous increasing bijection $[0,+\infty ) \rightarrow [0,1)$ is a homeomorphism between $T$ and $[0,1)$ as topological spaces and is an order-isomorphism between $T$ and $[0,1)$ as ordered sets, it is straightforward to show that $Th^2_<([0,1)) = Th^2_<(T)$. Thus $Th^2_<(T)$ is decidable.    $\square$

Let us fix some injective computable functions $\mathbf {d}:\mathbb {N} \rightarrow \mathbb {N}$, $\mathbf {en}:\mathbb {N} \times \mathbb {N} \rightarrow \mathbb {N}$, $\mathbf {ep}:\mathbb {N} \times \mathbb {N} \rightarrow \mathbb {N}$, $\mathbf {l}:\mathbb {N} \times \mathbb {N} \rightarrow \mathbb {N}$, $\mathbf {r}:\mathbb {N} \times \mathbb {N} \rightarrow \mathbb {N}$, $\mathbf {e}:\mathbb {N} \times \mathbb {N} \rightarrow \mathbb {N}$, and $\mathbf {f}:\mathbb {N} \rightarrow \mathbb {N}$ with pairwise disjoint ranges. We will use them to map the predicate symbols $D_{i}$, $E^-_{i,j}$, $E^+_{i,j}$, $L_{i,j}$, $R_{i,j}$ of $\mathcal {L}$ to distinct $F_{\sigma }$-variable names $F_{\mathbf {d}(i,j)}$, $F_{\mathbf {en}(i,j)}$, $F_{\mathbf {ep}(i,j)}$, $F_{\mathbf {l}(i,j)}$, $F_{\mathbf {r}(i,j)}$ of $\mathcal {L}_{<}^2$, to have distinct intermediate $F_{\sigma }$-variable names $F_{\mathbf {e}(i,j)}$, $i,j \in \mathbb {N}$, and to map variable names $F_i$ of $\mathcal {L}$ to variable names $F_{\mathbf {f}(i)}$ of $\mathcal {L}^2_<$.

For each $i,j,k \in \mathbb {N}$ let us define the following $\mathcal {L}^2_{<}$-formulas:

$$\begin{aligned}&Dom_j(F_{\mathbf {d}(j)}):=\\&\quad ((\lnot \exists t_1~t_1 \in F_{\mathbf {d}(j)}) \vee (\exists t_1 \exists t_2 (t_1 \in F_{\mathbf {d}(j)} \wedge t_2 \in F_{\mathbf {d}(j)} \wedge t_1 < t_2))) \wedge \\&\quad \; \wedge \forall t_1 \forall t_2 \forall t_3 (t_1 \in F_{\mathbf {d}(j)} \wedge t_2 \in F_{\mathbf {d}(j)} \wedge t_1<t_3 \wedge t_3<t_2 \rightarrow t_3 \in F_{\mathbf {d}(j)}) \end{aligned}$$

$$\begin{aligned} Eq_{i,j,k}&(F_{\mathbf {d}(i)},F_{\mathbf {e}(i,i)},F_{\mathbf {e}(i,j)},F_{\mathbf {e}(j,i)},F_{\mathbf {e}(j,k)},F_{\mathbf {e}(i,k)},F_{\mathbf {d}(j)},F_{\mathbf {en}(i,j)},F_{\mathbf {ep}(i,j)}) :=\\ \forall t_1&\, (t_1 \in F_{\mathbf {d}(i)} \rightarrow t_1 \in F_{\mathbf {e}(i,i)}) \wedge \\ \wedge \forall t_1&\, (t_1 \in F_{\mathbf {e}(i,j)} \rightarrow t_1 \in F_{\mathbf {e}(j,i)}) \wedge \\ \wedge \forall t_1&\, ( t_1 \in F_{\mathbf {e}(i,j)} \wedge t_1 \in F_{\mathbf {e}(j,k)} \rightarrow t_1 \in F_{\mathbf {e}(i,k)})) \wedge \\ \wedge \forall t_1&\,(t_1 \in F_{\mathbf {e}(i,j)} \rightarrow t_1 \in F_{\mathbf {d}(i)}\wedge t_1 \in F_{\mathbf {d}(j)})\wedge \\ \wedge \forall t_1&\, (t_1 \in F_{\mathbf {en}(i,j)} \leftrightarrow \\ \leftrightarrow&\, \exists t_2 (t_2 <t_1 \wedge \forall t_3(t_2<t_3 \wedge (t_3 <t_1 \vee t_3=t_1) \rightarrow t_3 \in F_{\mathbf {e}(i,j)}))) \wedge \\ \wedge \forall t_1&\, (t_1 \in F_{\mathbf {ep}(i,j)} \leftrightarrow \\&\,\leftrightarrow \exists t_2 (t_1 <t_2 \wedge \forall t_3((t_1<t_3 \vee t_1=t_3) \wedge t_3 <t_2 \rightarrow t_3 \in F_{\mathbf {e}(i,j)}))) \end{aligned}$$

$$\begin{aligned}&Lloc_{i,j,k}(F_{\mathbf {d}(i)}, F_{\mathbf {en}(i,j)}, F_{\mathbf {l}(k,i)},F_{\mathbf {l}(k,j)}):=\\&\quad \forall t_1\, ( t_1\in F_{\mathbf {en}(i,j)} \rightarrow (t_1 \in F_{\mathbf {l}(k,i)} \leftrightarrow t_1 \in F_{\mathbf {l}(k,j)}))\wedge \\&\, \wedge \forall t_1\, (t_1 \in F_{\mathbf {d}(i)} \wedge (\lnot \exists t_2\, (t_2<t_1 \wedge t_2 \in F_{\mathbf {d}(i)})) \rightarrow t_1 \in F_{\mathbf {l}(k,i)} ) \wedge \\&\, \wedge \forall t_1\, (\lnot t_1 \in F_{\mathbf {d}(i)} \rightarrow \lnot t_1 \in F_{\mathbf {l}(k,i)}) \end{aligned}$$

$$\begin{aligned}&Rloc_{i,j,k}(F_{\mathbf {d}(i)}, F_{\mathbf {ep}(i,j)}, F_{\mathbf {r}(k,i)},F_{\mathbf {r}(k,j)}):=\\&\quad \forall t_1\, ( t_1\in F_{\mathbf {ep}(i,j)} \rightarrow (t_1 \in F_{\mathbf {r}(k,i)} \leftrightarrow t_1 \in F_{\mathbf {r}(k,j)}))\wedge \\&\, \wedge \forall t_1\, (t_1 \in F_{\mathbf {d}(i)} \wedge (\lnot \exists t_2\, (t_1<t_2 \wedge t_2 \in F_{\mathbf {d}(i)})) \rightarrow t_1 \in F_{\mathbf {r}(k,i)} ) \wedge \\&\, \wedge \forall t_1\, (\lnot t_1 \in F_{\mathbf {d}(i)} \rightarrow \lnot t_1 \in F_{\mathbf {r}(k,i)}) \end{aligned}$$

$$\begin{aligned}&Min_{i,j}(F_{\mathbf {d}(j)},F_{\mathbf {l}(i,j)},F_{\mathbf {r}(i,j)}) := \\&\quad \forall t_1~( t_1 \in F_{\mathbf {l}(i,j)} \wedge t_1 \in F_{\mathbf {d}(j)} \wedge \exists t_2 (t_2<t_1 \wedge t_2 \in F_{\mathbf {d}(j)}) \rightarrow \\&\quad \, \rightarrow \exists t_3 (t_3<t_1 \wedge \forall t_4 (t_3<t_4 \wedge t_4<t_1 \rightarrow t_4 \in F_{\mathbf {l}(i,j)} \wedge t_4 \in F_{\mathbf {r}(i,j)}))) \wedge \\&\wedge \forall t_1~( t_1 \in F_{\mathbf {r}(i,j)} \wedge t_1 \in F_{\mathbf {d}(j)} \wedge \exists t_2 (t_1<t_2 \wedge t_2 \in F_{\mathbf {d}(j)})) \rightarrow \\&\qquad \rightarrow \exists t_3 (t_1<t_3 \wedge \forall t_4 (t_1<t_4 \wedge t_4<t_3 \rightarrow t_4 \in F_{\mathbf {l}(i,j)} \wedge t_4 \in F_{\mathbf {r}(i,j)})) \end{aligned}$$

Informally, $Dom_j$ expresses that $F_{\mathbf {d}(j)}$ is the domain of a distinguished trajectory $j$ (the empty set or a non-degenerate interval), $Eq_{i,j,k}$ is intended to express the properties of the relations of left and right coincidence of trajectories, $Lloc_{i,j,k}$ and $Rloc_{i,j,k}$ are intended to express left-locality and right-locality of predicates, and $Min_{i,j}$ is intended to express the properties of the members of $LR^*(Q)$ for arbitrary $Q$ (least LR representations of NCMS).

For each $\varPhi \in \mathcal {L}$ denote by $\mathfrak {m}(\varPhi )$ the maximal value of among all indices $i,j$ of the predicate symbols of the forms $D_i$, $E^-_{i,j}$, $E^+_{i,j}$, $L_{i,j}$, $R_{i,j}$ which appear in $\varPhi$, or $1$, if no such symbols appears in $\varPhi$.

For each $\varPhi \in \mathcal {L}^c$ let us define an associated formula $Trans(\varPhi )$ as follows. Let $\varPhi \in \mathcal {L}^c$ and $u_1, u_2,..., u_m$ be an increasing sequence of all elements of the set

$$\begin{aligned} \{\mathbf {d}(j),\mathbf {l}(i,j),\mathbf {r}(i,j),\mathbf {ep}(i,j),\mathbf {en}(i,j),\mathbf {e}(i,j)\}\, | \, i,j \in \{1,2,...,\mathfrak {m}(\varPhi )\}\}, \end{aligned}$$

and $\varPhi '$ be the formula obtained from $\varPhi$ by renaming all variable names of the form $F_i$ to $F_{\mathbf {f}(i)}$ and subsequent replacement of all atomic sub-formulas of $\varPhi$ of the forms $D_{i}(t_k)$, $E^-_{i,j}(t_k)$, $E^+_{i,j}(t_k)$, $L_{i,j}(t_k)$, $R_{i,j}(t_k)$ ($i,j,k \in \mathbb {N}$) with $t_k \in F_{\mathbf {d}(i,j)}$, $t_k \in F_{\mathbf {en}(i,j)}$, $t_k \in F_{\mathbf {ep}(i,j)}$, $t_k \in F_{\mathbf {l}(i,j)}$, $t_k \in F_{\mathbf {r}(i,j)}$ respectively.

Then $Trans(\varPhi )$ denotes the following formula:

$$\begin{aligned}&\forall F_{u_1} \forall F_{u_2} ... \forall F_{u_m} \bigwedge _{j=1}^{\mathfrak {m}(\varPhi )} Dom_j (F_{\mathbf {d}(j)}) \wedge \bigwedge _{i=1}^{\mathfrak {m}(\varPhi )} \bigwedge _{j=1}^{\mathfrak {m}(\varPhi )} \bigwedge _{k=1}^{\mathfrak {m}(\varPhi )} ( \\&\quad Eq_{i,j,k}(F_{\mathbf {d}(i)},F_{\mathbf {e}(i,i)},F_{\mathbf {e}(i,j)},F_{\mathbf {e}(j,i)}, F_{\mathbf {e}(j,k)},F_{\mathbf {e}(i,k)},F_{\mathbf {d}(j)},F_{\mathbf {en}(i,j)},F_{\mathbf {ep}(i,j)}) \wedge \\&\wedge \, Lloc_{i,j,k}(F_{\mathbf {d}(i)}, F_{\mathbf {en}(i,j)}, F_{\mathbf {l}(k,i)},F_{\mathbf {l}(k,j)}) \wedge \\&\wedge \, Rloc_{i,j,k}(F_{\mathbf {d}(i)}, F_{\mathbf {ep}(i,j)}, F_{\mathbf {r}(k,i)},F_{\mathbf {r}(k,j)})) \wedge \\ \wedge&\bigwedge _{i=1}^{\mathfrak {m}(\varPhi )} \bigwedge _{j=1}^{\mathfrak {m}(\varPhi )} Min_{i,j} (F_{\mathbf {d}(j)},F_{\mathbf {l}(i,j)},F_{\mathbf {r}(i,j)}) \rightarrow \varPhi ' \end{aligned}$$

Obviously, $Trans(\varPhi )$ is a closed formula in $\mathcal {L}^2_<$.

Informally, $Trans$ translates $\mathcal {L}$-sentences into $\mathcal {L}^2_<$-sentences for the purpose of reduction of testing membership in $Th$ to testing membership in $Th^2_<(T)$.

Denote $I_0 = \mathbb {N}$ and $I_n = \{1,2,...,n\}$ for each $n \in \mathbb {N}$.

For each $n \in \mathbb {N} \cup \{0\}$ let $\mathcal {S}_n$ be the set of all structures

$$(T,<,(D_i)_{i \in \mathbb {N}},(E^-_{i,j})_{i,j \in \mathbb {N}},(E^+_{i,j})_{i,j \in \mathbb {N}},(L_{i,j})_{i,j \in \mathbb {N}}, (R_{i,j})_{i,j \in \mathbb {N}}) \in \mathcal {S}$$

such that there exists an indexed family $(E_{i,j})_{i,j \in I_n}$ of predicates on $T$ which satisfy the following conditions:

• (1) for each $i,j \in I_n$ the truth sets of $D_i$, $E_{i,j}^-$, $E_{i,j}^+$, $L_{i,j}$, $R_{i,j}$, $E_{i,j}$ are in $F_{\sigma }(T)$;

• (2) for each $i \in I_n$ the truth set of $D_i$ belongs to $\mathfrak {T} \cup \{\emptyset \}$;

• (3) for each $i,j,k \in I_n$ and $t \in T$ the following properties of $E_{i,j}$ hold:

  • $D_{i}(t) \Rightarrow E_{i,i}(t)$;

  • $E_{i,j}(t) \Rightarrow E_{j,i}(t)$;

  • $E_{i,j}(t) \wedge E_{j,k}(t) \Rightarrow E_{i,k}(t)$;

  • $E_{i,j}(t) \Rightarrow D_i(t) \wedge D_j(t)$;

  • $E_{i,j}^-(t) \Leftrightarrow \exists t' \in [0,t)~\forall t'' \in (t',t]~ E_{i,j}(t'')$;

  • $E_{i,j}^+(t) \Leftrightarrow \exists t'>t~\forall t'' \in [t,t')~ E_{i,j}(t'')$;

• (4) for each $i,j,k \in I_n$ and $t \in T$ the following properties of $L_{k,i}$ hold:

  • $E^-_{i,j}(t) \Rightarrow (L_{k,i}(t) \Leftrightarrow L_{k,j}(t))$;

  • if $t$ is a minimal element of $\{t'~|~D_i(t')\}$, then $L_{k,i}(t)$;

  • $\lnot D_i(t)\Rightarrow \lnot L_{k,i}(t)$;

• (5) for each $i,j,k \in I_n$ and $t \in T$ the following properties of $R_{k,i}$ hold:

  • $E^+_{i,j}(t) \Rightarrow (R_{k,i}(t) \Leftrightarrow R_{k,j}(t))$;

  • if $t$ is a maximal element of $\{t'~|~D_i(t')\}$, then $R_{k,i}(t)$;

  • $\lnot D_i(t)\Rightarrow \lnot R_{k,i}(t)$;

• (6) for each $i,j \in I_n$ and $t \in T$ the following holds:

  • if $L_{i,j}(t)$ and $t$ is a non-minimal element of $\{t'~|~D_j(t')\}$, then there exists $t' \in [0,t)$ such that $L_{i,j}(t'') \wedge R_{i,j}(t'')$ for all $t'' \in (t',t)$;

  • if $R_{i,j}(t)$ and $t$ is a non-maximal element of $\{t'~|~D_j(t')\}$, then there exists $t'>t$ such that $L_{i,j}(t'') \wedge R_{i,j}(t'')$ for all $t'' \in (t,t')$.

Lemma 3

Let $\varPhi \in \mathcal {L}^c$. Then $Trans(\varPhi ) \in Th^2_<(T)$ if and only if $S \models \varPhi$ for all $S \in \mathcal {S}_{\mathfrak {m}(\varPhi )}$.

Proof

(Sketch). Follows straightforwardly from the definition of $Trans$, $\mathcal {S}_{\mathfrak {m}(\varPhi )}$, and the interpretation of $\mathcal {L}^2_<$ formulas.    $\square$

Lemma 4

Let $\varPhi \in \mathcal {L}$, $n \in \mathbb {N}$, $n \ge \mathfrak {m}(\varPhi )$. Then $S \models \varPhi$ for all $S \in \mathcal {S}_n$ if and only if $S \models \varPhi$ for all $S \in \mathcal {S}_0$.

Proof

(Sketch).

• “If”: Assume that $S \models \varPhi$ for all $S \in \mathcal {S}_n$. Using the definition of $\mathcal {S}_0$, it is easy to check that $\mathcal {S}_0 \subseteq \mathcal {S}_n$. Then $S \models \varPhi$ for all $S \in \mathcal {S}_0$.

• “Only if”: Assume that $S \models \varPhi$ for all $S \in \mathcal {S}_0$. Let

  $$\begin{aligned} S'=(T,<,(D_i)_{i \in \mathbb {N}},(E^-_{i,j})_{i,j \in \mathbb {N}},(E^+_{i,j})_{i,j \in \mathbb {N}},(L_{i,j})_{i,j \in \mathbb {N}}, (R_{i,j})_{i,j \in \mathbb {N}}) \in \mathcal {S}_n \end{aligned}$$

  be an arbitrary element. Then there exists a family $(E_{i,j})_{i,j \in I_n}$ of predicates on $T$ such that the properties (1)–(6) of $\mathcal {S}_n$ hold for $S'$ and $(E_{i,j})_{i,j \in I_n}$.

  Let us prove that $S' \models \varPhi$.

  For each $i,j \in I_n$ let $D_i'=D_i$, $E'^-_{i,j}=E^-_{i,j}$, $E'^+_{i,j}=E^+_{i,j}$. For each $i,j \in \mathbb {N}$ such that $(i,j) \notin I_n \times I_n$ let us define unary predicates $D_i'$, $E'^-_{i,j}$, $E'^+_{i,j}$ on $T$ such that $\lnot D_i'(t)$, $\lnot E'^-_{i,j}(t)$, $\lnot E'^+_{i,j}(t)$ for all $t \in T$.

  For each $i,j \in \mathbb {N}$ let us define unary predicates $L'_{i,j}$, $R'_{i,j}$ on $T$ such that

  • if $(i,j) \in I_n \times I_n$, then $L'_{i,j}=L_{i,j}$, otherwise for all $t \in T$, $L'_{i,j}(t)$ if and only if $t$ is a minimal element of the truth set of $D_j'$;

  • if $(i,j) \in I_n \times I_n$, then $R'_{i,j} = R_{i,j}$, otherwise for all $t \in T$, $R'_{i,j}(t)$ if and only if $t$ is a maximal element of the truth set of $D_j'$.

  Let

  $$\begin{aligned} S''=(T,<,(D'_i)_{i \in \mathbb {N}},(E'^-_{i,j})_{i,j \in \mathbb {N}},(E'^+_{i,j})_{i,j \in \mathbb {N}},(L'_{i,j})_{i,j \in \mathbb {N}}, (R'_{i,j})_{i,j \in \mathbb {N}}). \end{aligned}$$

  Obviously, $S'' \in \mathcal {S}$. The structures $S'$ and $S''$ have the same carrier set. Also, because $n \ge \mathfrak {m}(\varPhi )$, the symbols of all predicates which appear in $\varPhi$ have the same interpretations in $S'$ and $S''$, so $S'' \models \varPhi$ if and only if $S' \models \varPhi$.

  Let us show that $S'' \in \mathcal {S}_0$. Let $(E'_{i,j})_{i,j \in I_0}$ be an indexed family of predicates such that for each $i,j \in \mathbb {N}$, if $(i,j) \in I_0 \times I_0$, then $E'_{i,j}=E_{i,j}$, and if $(i,j) \notin I_0 \times I_0$, then $\lnot E'_{i,j}(t)$ for all $t \in T$.

  It is easy to check that the properties (1)–(3) and (6) of $\mathcal {S}_0$ hold for $S''$ and $(E'_{i,j})_{i,j \in I_0}$. Let us prove the property (4) of $\mathcal {S}_0$ for $S''$ and $(E'_{i,j})_{i,j \in I_0}$.

  Let $i,j,k \in I_0$ and $t \in T$.

  • Let us show that $E'^-_{i,j}(t) \Rightarrow (L'_{k,i}(t) \Leftrightarrow L'_{k,j}(t))$. Assume that $E'^-_{i,j}(t)$. Then $i,j \in I_n$, so $E^-_{i,j}(t)$. If $k \in I_n$, then $L_{k,i}(t) \Leftrightarrow L_{k,j}(t)$, because the property (4) of $\mathcal {S}_n$ holds for $S'$ and $(E_{i,j})_{i,j \in I_n}$, so $L'_{k,i}(t) \Leftrightarrow L'_{k,j}(t)$. Otherwise, $k \notin I_n$ and from the property (3) of $\mathcal {S}_n$ for $S'$ and $(E_{i,j})_{i,j \in I_n}$ it follows that $t$ is not a minimal element of the truth set of $E^-_{i,j}$ and is not a minimal element of the truth sets of $D_i=D'_i$ and $D_j=D'_j$. Then $\lnot L'_{k,i}(t)$ and $\lnot L'_{k,j}(t)$, whence $L'_{k,i}(t) \Leftrightarrow L'_{k,j}(t)$. We conclude that $E'^-_{i,j}(t) \Rightarrow (L'_{k,i}(t) \Leftrightarrow L'_{k,j}(t))$.

  • Let us show that if $t$ is a minimal element of $\{t'~|~D'_i(t')\}$, then $L'_{k,i}(t)$. Let $t$ be a minimal element of $\{t'~|~D'_i(t')\}$. Then $D'_i(t)$, so $i \in I_n$ and $t$ is a minimal element of $\{t'~|~D_i(t')\}$. If $k \in I_n$, then $L_{k,i}(t)$ by the property (4) of $\mathcal {S}_n$ for $S'$ and $(E_{i,j})_{i,j \in I_n}$, so $L'_{k,i}(t)$. Otherwise, $k \notin I_n$ and $t$ is a minimal element of $\{t'~|~D'_i(t')\}$, so $L'_{k,i}(t)$. In both cases, $L'_{k,i}(t)$.

  • Let us show that $\lnot D'_i(t) \Rightarrow \lnot L'_{k,i}(t)$. Assume that $\lnot D'_i(t)$. If $i \in I_n$ and $k \in I_n$, then $\lnot D_i(t) \Rightarrow \lnot L_{k,i}(t)$, $D_i = D'_i$, and $L_{k,i}=L'_{k,i}$, so $\lnot L'_{k,i}(t)$. Otherwise, $i \notin I_n$ or $k \notin I_n$, whence $\lnot L'_{k,i}(t)$, because $t$ is not an element of the truth set of $D'_i$. In both cases, $\lnot L'_{k,i}(t)$.

  Thus the property (4) of $\mathcal {S}_0$ holds for $S''$ and $(E'_{i,j})_{i,j \in I_0}$. The property (5) of $\mathcal {S}_0$ can be proven for $S''$ and $(E'_{i,j})_{i,j \in I_0}$ analogously.

  We conclude that $S'' \in \mathcal {S}_0$. Then $S'' \models \varPhi$ by assumption. Thus $S' \models \varPhi$. Because $S'$ is arbitrary, we have $S' \models \varPhi$ for all $S' \in \mathcal {S}_n$.   $\square$

Lemma 5

$St(M) \in \mathcal {S}_0$ for each $M \in \mathcal {M}$.

Proof

Let $M=((s_i)_{i \in \mathbb {N}},(\varSigma _{i})_{i \in \mathbb {N}}) \in \mathcal {M}$ and $Q$ be the (common) set of states of all $\varSigma _i$, $i \in \mathbb {N}$. Let

$$\begin{aligned} S=St(M)=(T,<,(D_i)_{i \in \mathbb {N}},(E^-_{i,j})_{i,j \in \mathbb {N}},(E^+_{i,j})_{i,j \in \mathbb {N}},(L_{i,j})_{i,j \in \mathbb {N}}, (R_{i,j})_{i,j \in \mathbb {N}}). \end{aligned}$$

Then $S \in \mathcal {S}$. Let us show that $S \in \mathcal {S}_0$. For each $i \in \mathbb {N}$ let $(l_i^*,r_i^*)=LR_{min}(\varSigma _i)$. By Theorem 3(2), $(l^*_i,r^*_i) \in LR^*(Q)$. By the definition of $St(M)$, for all $i,j \in \mathbb {N}$ and $t \in T$, $D_i(t) \Leftrightarrow t \in dom(s_i)$, $E^-_{i,j}(t) \Leftrightarrow s_i \dot{=}_{t-} s_j$, and $E^+_{i,j}(t) \Leftrightarrow s_i \dot{=}_{t+} s_j$. Moreover, if $s_j(t) \downarrow$, then $L_{i,j}(t)\Leftrightarrow l^*_i(s_j,t)$ and $R_{i,j}(t) \Leftrightarrow r^*_i(s_j,t)$, and if $s_j(t) \uparrow$, then $\lnot L_{i,j}(t)$ and $\lnot R_{i,j}(t)$.

For each $t \in T$ let $V(t)= \{(i,j) \in \mathbb {N} \times \mathbb {N}~|~E^-_{i,j}(t) \vee E^+_{i,j}(t)\}$ and $V^T(t)$ is a transitive closure of $V(t)$. Let $(E_{i,j})_{i,j \in \mathbb {N}}$ be an indexed family of predicates on $T$ such that $E_{i,j}(t) \Leftrightarrow (i,j) \in V^T(t)$ for all $i,j \in \mathbb {N}$ and $t \in T$.

Note that for each $t \in T$, $V(t)$ is a symmetric binary relation, so $V^T(t)$ is also a symmetric binary relation.

It is easy to check that the properties (2) and (3) of $\mathcal {S}_0$ hold for $S$ and $(E_{i,j})_{i,j \in \mathbb {N}}$. Taking into account that for each $i \in \mathbb {N}$, $l^*_i$ is left-local and $r^*_i$ is right-local, the properties (4) and (5) of $\mathcal {S}_0$ also hold for $S$ and $(E_{i,j})_{i,j \in \mathbb {N}}$. The property (6) of $\mathcal {S}_0$ can be easily checked for $S$ and $(E_{i,j})_{i,j \in \mathbb {N}}$ by taking into account that $(l^*_i,r^*_i) \in LR^*(Q)$ for all $i \in \mathbb {N}$.

Let us prove the remaining property (1) of $\mathcal {S}_0$ for $S$ and $(E_{i,j})_{i,j \in \mathbb {N}}$, i.e. that the truth sets of $D_i$, $E^-_{i,j}$, $E^+_{i,j}$, $L_{i,j}$, $R_{i,j}$, $E_{i,j}$ belong to $F_{\sigma }(T)$ for all $i,j \in \mathbb {N}$.

Let us fix $i,j \in \mathbb {N}$. We have $\{t~|~D_i(t)\} = dom(s_i) \in \mathfrak {T} \cup \{\emptyset \} \subset F_{\sigma }(T)$.

It is easy to see that $E^-_{i,j}$ is a left-stable predicate and $E^+_{i,j}$ is a right-stable predicate. Then by Lemma 1, the truth sets of $E^-_{i,j}$ and $E^+_{i,j}$ belong to $F_{\sigma }(T)$.

Let $P_j$ be a predicate on $T$ such that $P_j(t)$ if and only if $t$ is a non-minimal element of $dom(s_j)$. Let $A$, $B$ be predicates on $T$ such that $A(t) \Leftrightarrow L_{i,j}(t) \wedge P_j(t)$, $B(t) \Leftrightarrow L_{i,j}(t) \wedge \lnot P_j(t)$ for all $t \in T$. Because $(l^*_i,r^*_i) \in LR^*(Q)$, $A$ is a left-stable predicate, so by Lemma 1 the truth set of $A$ belongs to $F_{\sigma }(T)$. Moreover, because $\lnot L_{i,j}(t)$ for all $t \in T\backslash dom(s_j)$, $B(t)$ implies that $t$ is a minimal element of $dom(s_j)$, so the truth set of $B$ is either empty or a singleton set, so it is in $F_{\sigma }(T)$. Then $\{t~|~L_{i,j}(t)\}=\{t~|~A(t)\} \cup \{t~|~B(t)\} \in F_{\sigma }(T)$.

By analogy it is easy to prove that $\{t~|~R_{i,j}(t)\} \in F_{\sigma }(T)$.

Let us show that $\{t~|~E_{i,j}(t)\} \in F_{\sigma }(T)$. Let

$$\begin{aligned} W=\{ \{t'~|~E^-_{i,j}(t')\} ~|~i,j \in \mathbb {N} \} \cup \{ \{t'~|~E^+_{i,j}(t')\} ~|~i,j \in \mathbb {N} \}. \end{aligned}$$

From the arguments mentioned it follows that $W \subseteq F_{\sigma }(T)$. Using the definition of $E_{i,j}$ it is easy to check that $\{t~|~E_{i,j}(t)\}$ can be represented as a countable union of finite intersections of elements of $W$. As finite intersections of $F_{\sigma }$-sets are $F_{\sigma }$-sets, it follows that $\{t~|~E_{i,j}(t)\} \in F_{\sigma }(T)$.

We conclude that the truth sets of $D_i$, $E^-_{i,j}$, $E^+_{i,j}$, $L_{i,j}$, $R_{i,j}$, $E_{i,j}$ are in $F_{\sigma }(T)$. The properties (1)-(6) of $\mathcal {S}_0$ hold for $S$ and $(E_{i,j})_{i,j \in \mathbb {N}}$, so $S = St(M) \in \mathcal {S}_0$.    $\square$

Lemma 6

For each $S \in \mathcal {S}_0$ there exists $M \in \mathcal {M}$ such that $S=St(M)$.

Proof

(Sketch). Let

$$\begin{aligned} S=(T,<,(D_i)_{i \in \mathbb {N}},(E^-_{i,j})_{i,j \in \mathbb {N}},(E^+_{i,j})_{i,j \in \mathbb {N}},(L_{i,j})_{i,j \in \mathbb {N}}, (R_{i,j})_{i,j \in \mathbb {N}}) \in \mathcal {S}_0. \end{aligned}$$

Then $S \in \mathcal {S}$ and there exists an indexed family $(E_{i,j})_{i,j \in \mathbb {N}}$ of predicates on $T$ such that the properties (1)–(6) of $\mathcal {S}_0$ hold for $S$ and $(E_{i,j})_{i,j \in \mathbb {N}}$.

Let $Q=2^{\mathbb {N}}$ and for each $i \in \mathbb {N}$, $s_i:T \tilde{\rightarrow }Q$ be a function such that $s_i(t)\downarrow =\{j \in \mathbb {N}~|~E_{i,j}(t)\}$ for each $t \in T$ such that $D_i(t)$ and $s_i(t) \uparrow$ for each $t \in T$ such that $\lnot D_i(t)$. For each $k \in \mathbb {N}$ let $l_k:ST(Q) \rightarrow Bool$ and $r_k:ST(Q) \rightarrow Bool$ be predicates such that for each $(s,t) \in ST(Q)$:

• $l_k(s,t)$ if and only if either $t$ is a minimal element of $dom(s)$, or there exists $i \in \mathbb {N}$ such that $s \doteq _{t-}s_i$ and $L_{k,i}(t)$.

• $r_k(s,t)$ if and only if either $t$ is a maximal element of $dom(s)$, or there exists $i \in \mathbb {N}$ such that $s \doteq _{t+}s_i$ and $R_{k,i}(t)$.

It follows immediately that $l_k$ is left-local and $r_k$ is right-local. Then $(l_k,r_k) \in LR(Q)$. For each $k \in \mathbb {N}$ let $Tr_k=\{ s:A \rightarrow Q\,|\, A \in \mathfrak {T} \wedge (\forall t \in A~l_k(s,t) \wedge r_k(s,t)) \}$ and $\varSigma _k = (T,Q,Tr_k)$. Let $M=((s_i)_{i \in \mathbb {N}},(\varSigma _k)_{k \in \mathbb {N}})$. The property (2) of $\mathcal {S}_0$ for $S$ and $(E_{i,j})_{i,j \in \mathbb {N}}$ implies that $dom(s_i) \in \mathfrak {T} \cup \{\emptyset \}$ for all $i \in \mathbb {N}$ and Theorem 1(1) implies that $\varSigma _k$ is a NCMS with the set of states $Q$ for all $k \in \mathbb {N}$. Thus $M \in \mathcal {M}$.

For each $k \in \mathbb {N}$ let $(l^*_k,r_k^*) = LR_{min}(\varSigma _k)$.

Using the properties of $\mathcal {S}_0$ it is not difficult to check that for each $i,j \in \mathbb {N}$ and $t \in T$, $D_i(t) \Leftrightarrow t \in dom(s_i)$, $E^-_{i,j}(t) \Leftrightarrow s_i \dot{=}_{t-} s_j$, $E^+_{i,j}(t) \Leftrightarrow s_i \dot{=}_{t+}s_j$, and also if $s_j(t)\downarrow$, then $L_{i,j}(t) \Leftrightarrow l^*_i(s_j,t)$ and $R_{i,j}(t)\Leftrightarrow r_i^*(s_j,t)$ and if $s_j(t) \uparrow$, then $\lnot L_{i,j}(t)$ and $\lnot R_{i,j}(t)$. Then $S=St(M)$.    $\square$

Lemma 7

Let $\varPhi \in \mathcal {L}^c$. Then $Trans(\varPhi ) \in Th^2_<(T)$ if and only if $\varPhi \in Th$.

Proof

By Lemma 3, $Trans(\varPhi ) \in Th^2_<(T)$ if and only if $S \models \varPhi$ for all $S \in \mathcal {S}_{\mathfrak {m}(\varPhi )}$. By Lemma 4, $S \models \varPhi$ for all $S \in \mathcal {S}_{\mathfrak {m}(\varPhi )}$ if and only if $S \models \varPhi$ for all $S \in \mathcal {S}_0$. Lemmas 5, 6 imply that $S \models \varPhi$ for all $S \in \mathcal {S}_0$ if and only if $St(M) \models \varPhi$ (i.e. $M \models ^m \varPhi$) for all $M \in \mathcal {M}$. Thus $Trans(\varPhi ) \in Th^2_<(T)$ if and only if $\varPhi \in Th$.    $\square$

Now we can prove Theorem 4.

Proof of Theorem 4 (Sketch). Lemma 7 implies that $Th = \{\varPhi \in \mathcal {L}^c~|~Trans(\varPhi ) \in Th^2_<(T)\}$. Then because $Th^2_<(T)$ is decidable by Lemma 2, it is straightforward to show that $Th$ is decidable.    $\square$

5 Example of Application

Let us consider an example of application of the obtained results. Distributed CPS often contain several components (e.g. information processing units) which need an exclusive access to a single shared resource (e.g. an actuator) [2].

Consider a CPS which consists of three components (or processes), two of which (component 1 and component 2) share a certain resource. The resource may be accessed sequentially, but simultaneous access by two components is prohibited. To guarantee absence of simultaneous access to the resource, the components 1 and 2 communicate using shared memory and implement a variant of Peterson’s mutual exclusion algorithm. The components 1 and 2 can read shared memory and the current state of another component at any time (possibly simultaneously), but cannot write directly into the shared memory. Instead, the component 3 has exclusive write access to the shared memory and acts as an arbiter which receives write requests from the components 1 and 2. If the component 3 receives one request at a given time moment, it satisfies it immediately. If it receives two requests simultaneously, it chooses one of them (arbitrarily), satisfies it, and declines another one.

Let us model the behavior of the described CPS as a set of trajectories from the time domain $T$ to a set (global) states $Q$ of the form $A_1 \times A_2 \times A_3 \times M \times R$, where $A_i$, $i=1,2,3$ is the set of (individual) states of the component $i$, $M$ is the set of states of the shared memory, and $R$ is the set of states of the shared resource. For each $q \in Q$ we denote by $a_i(q)$ the projections of $q$ on the coordinate $i$, $i=1,2,3$, and by $m(q)$ denote the projection of $q$ on the 4-th coordinate.

Let us assume that $A_1=Bool$, $A_2=Bool$, $A_3=Bool \times Bool \times Bool \times Bool$, and $M=Bool$. The elements of $A_i$, $i=1,2$ indicate whether the component $i$ is interested in obtaining the access the shared resource. The elements of $M$ indicate which of the two components have the priority over another one. The elements of $A_3$ have the form $(w_1,v_1,w_2,v_2)$, where for $i=1,2$, $w_i=true$ means that the component $i$ is asking the component 3 to write the value $v_i$ into the shared memory, and $w_i=false$ means that the component $i$ is not asking the component 3 to change the shared memory. For each $q \in A_3$ we will denote by $w_1(q)$, $v_1(q)$, $w_2(q)$, $v_2(q)$ the projections of $a_3(q)$ on the 1, 2, 3, 4-th coordinate.

For each predicate $P:Q \rightarrow Bool$ let us denote

$$ Tr^P=\{s:A \rightarrow Q ~|~A \in \mathfrak {T}\wedge \forall t\in A~P(s(t))\} $$

and $\varSigma ^P=(T,Q,\varSigma ^P)$. Obviously, $Tr^P$ is CPR, complete, and Markovian set of trajectories, so $\varSigma ^P$ is a NCMS.

For each predicate $P:Q \rightarrow Bool$ denote by $\bar{P}$ the predicate on $Q$ such that $\bar{P}(q)\Leftrightarrow \lnot P(q)$ for all $q \in Q$.

We will specify the behavior and the mutual exclusion property of the described CPS in terms of the properties of the following tuple of NCMS:

$$\begin{aligned}&(\varSigma _i)_{i=1,2,...,14}= \\&\quad =(\varSigma ^{a_1},\varSigma ^{\bar{a}_1}, \varSigma ^{a_2},\varSigma ^{\bar{a}_2}, \varSigma ^{m}, \varSigma ^{\bar{m}}, \varSigma ^{w_1}, \varSigma ^{\bar{w}_1}, \varSigma ^{w_2}, \varSigma ^{\bar{w}_2}, \varSigma ^{v_1}, \varSigma ^{\bar{v}_1}, \varSigma ^{v_2}, \varSigma ^{\bar{v}_2}). \end{aligned}$$

Let us introduce the following names for the indices of the components of the tuple: $\mathbf {a}_1=1$, $\mathbf {\bar{a}}_1=2, \mathbf {a}_2=3, \mathbf {\bar{a}}_2=4, \mathbf {m}=5, \mathbf {\bar{m}}=6, \mathbf {w}_1=7, \mathbf {\bar{w}}_1 = 8, \mathbf {w}_2=9, \mathbf {\bar{w}}_2=10, \mathbf {v}_1=11, \mathbf {\bar{v}}_1=12, \mathbf {v}_2=13, \mathbf {\bar{v}}_2=14$.

Let $\varPsi$, $\varPhi _1$, $\varPhi _2$, $\varPhi _3$ be the following formulas in the language $\mathcal {L}$:

$$\begin{aligned} \varPsi :=\forall t_1~\bigwedge _{k=1}^{7}\lnot (L_{2k-1,1}(t_1) \wedge L_{2k,1}(t_1)) \wedge \lnot (R_{2k-1,1}(t_1),R_{2k,1}(t_1)) \end{aligned}$$

$$\begin{aligned}&\;\;\;\, \varPhi _1(t_1):=(\exists t_2 \exists t_3 \exists t_4~t_2<t_3 \wedge t_3<t_4\wedge t_4<t_1 \wedge \\&\qquad \qquad \qquad \;\; (\forall t_5(t_2<t_5\wedge (t_5< t_1 \vee t_5=t_1)\rightarrow L_{i_1,1}(t_5)))\wedge \\&\qquad \qquad \qquad \qquad \quad \;\;\wedge \; L_{{w}_1,1}(t_3) \wedge L_{v_1,1}(t_3) \wedge R_{v_1,1}(t_3) \wedge \\&(\forall t_5((t_3<t_5\vee t_3=t_5)\wedge (t_5< t_1 \vee t_5=t_1)\rightarrow R_{\bar{w}_1,1}(t_5))) \wedge (R_{\bar{i}_2,1}(t_4)\vee R_{m,1}(t_4))~) \end{aligned}$$

$$\begin{aligned}&\,\,\varPhi _2(t_1):=(\exists t_2 \exists t_3 \exists t_4~t_2<t_3 \wedge t_3<t_4\wedge t_4<t_1 \wedge \\&\qquad \qquad \qquad (\forall t_5(t_2<t_5\wedge (t_5< t_1 \vee t_5=t_1)\rightarrow L_{i_2,1}(t_5)))\wedge \\&\qquad \qquad \qquad \qquad \quad \wedge \; L_{w_2,1}(t_3) \wedge L_{\bar{v}_2,1}(t_3) \wedge R_{\bar{v}_2,1}(t_3) \wedge \\&(\forall t_5((t_3<t_5\vee t_3=t_5)\wedge (t_5< t_1 \vee t_5=t_1)\rightarrow R_{\bar{w}_2,1}(t_5))) \wedge (R_{\bar{i}_1,1}(t_4)\vee R_{\bar{m},1}(t_4))~) \end{aligned}$$

$$\begin{aligned}&\varPhi _3:=\forall t_1 ((R_{\bar{w}_1,1}(t_1)\wedge R_{\bar{w}_2,1}(t_1) \rightarrow (R_{m,1}(t_1)\vee R_{\bar{m},1}(t_1)) \wedge \\&\qquad \qquad \;\; \wedge (R_{ w_1,1}(t_1)\wedge R_{\bar{w}_2,1}(t_1) \wedge R_{v_1,1}(t_1) \rightarrow R_{m,1}(t_1))\wedge \\&\qquad \qquad \;\; \wedge (R_{w_1,1}(t_1)\wedge R_{\bar{w}_2,1}(t_1) \wedge R_{\bar{v}_1,1}(t_1) \rightarrow R_{\bar{m},1}(t_1))\wedge \\&\qquad \qquad \;\; \wedge (R_{\bar{w}_1,1}(t_1)\wedge R_{w_2,1}(t_1) \wedge R_{v_2,1}(t_1) \rightarrow R_{m,1}(t_1))\wedge \\&\qquad \qquad \;\; \wedge (R_{\bar{w}_1,1}(t_1)\wedge R_{w_2,1}(t_1) \wedge R_{\bar{v}_2,1}(t_1) \rightarrow R_{\bar{m},1}(t_1))) \end{aligned}$$

$$ \varPhi := \lnot \exists t_1(\varPsi \wedge \varPhi _1(t_1) \wedge \varPhi _2(t_1) \wedge \varPhi _3) $$

Informally, we can interpret $\varPhi (t_i)$, $i=1,2$ as a statement that the component $i$ of the CPS described above can access the shared resource at time $t_1$, and this happens only if there exist three preceding time moments ($t_2<t_3<t_4<t_1$) such that the component $i$ sets its individual state to $True$ at time $t_2$ (i.e. indicates that it is interested in accessing the shared resource) and sends a request to write the value $true$, if $i=1$ or $false$, if $i=2$ to the shared memory to the component 3 at time $t_3$, and at time $t_4$, either the component $3-i$ is not interested in accessing the shared resource, or the value of the shared memory indicates the priority of the component $i$ over the component $3-i$. This statement can be considered as a high-level expression of the Peterson’s algorithm. Also, informally, $\varPhi _3$ expresses the algorithm of the component 3 and $\varPsi$ is a consistency condition like “a predicate and its negation cannot hold simultaneously”.

Then $\varPhi$ can be interpreted as the statement that there is no time moment $t_1$ at which the components 1 and 2 of the CPS described above can simultaneously access the shared resource.

One can prove that $\varPhi \in Th$ directly using definitions. However, this can also be checked by a decision procedure for $Th$ described in the proof of Theorem 4, which gives a mechanized proof of the mutual exclusion property of an abstract version of Peterson’s algorithm in the case of CPS.

6 Conclusions and Future Work

We have proposed a decidable formal theory for describing high-level properties of NCMS. The class of NCMS contains abstract dynamical systems which can represent discrete and continuous evolutions in continuous time and are sufficient for modeling a wide range of real-time information processing and cyber-physical systems. In the future works we plan to extend the introduced theory and apply it to verification of practical cyber-physical systems.