11institutetext:  University College London, London, UK, 11email:
<EMAIL_ADDRESS>22institutetext: Department of Mathematics University of
Rijeka, Rijeka, Croatia, 22email<EMAIL_ADDRESS>33institutetext: Federal
University of Paraíba, João Pessoa, Brazil, 33email<EMAIL_ADDRESS>44institutetext: Munich Research Center, Huawei, Munich, Germany
55institutetext: University of Pennsylvania, Philadelphia, USA, 55email:
<EMAIL_ADDRESS>66institutetext: HSE University, Computer Science
Dept., Moscow, Russia 77institutetext: SRI International, Menlo Park, USA,
77email<EMAIL_ADDRESS>
# On the Complexity of Verification of Time-Sensitive Distributed Systems:
Technical Report

Max Kanovich Tajana Ban Kirigin Vivek Nigam Andre Scedrov and Carolyn Talcott
11662233445577

###### Abstract

This paper develops a Multiset Rewriting language with explicit time for the
specification and analysis of Time-Sensitive Distributed Systems (TSDS). Goals
are often specified using explicit time constraints. A good trace is an
infinite trace in which the goals are satisfied perpetually despite possible
interference from the environment. In our previous work [16], we discussed two
desirable properties of TSDSes, _realizability_ (there exists a good trace)
and _survivability_ (where, in addition, all admissible traces are good). Here
we consider two additional properties, _recoverability_ (all compliant traces
do not reach points-of-no-return) and _reliability_ (the system can always
continue functioning using a good trace). Following [16], we focus on a class
of systems called _Progressing Timed Systems_ (PTS), where intuitively only a
finite number of actions can be carried out in a bounded time period. We prove
that for this class of systems the properties of recoverability and
reliability coincide and are PSPACE-complete. Moreover, if we impose a bound
on time (as in bounded model-checking), we show that for PTS the reliability
property is in the $\Pi_{2}^{p}$ class of the polynomial hierarchy, a subclass
of PSPACE. We also show that the bounded survivability is both NP-hard and
coNP-hard.

##  1 Introduction

In our previous work [16], we considered the verification of Time-Sensitive
Distributed Systems (TSDS) motivated by applications with autonomous drones
performing surveillance of an area. The drones must always collectively have
recent pictures, i.e., at most M time units old, of certain strategic
locations. In attempting to achieve this goal, the drones consume energy and
must return to the base station to recharge their batteries. In addition, the
environment may interfere as there may be winds that move the drone in a
certain direction, or other flying objects may block a drone’s path.

In [16] we considered two verification properties, realizability and
survivability. Here we introduce two more properties, reliability and
recoverability. Let us explain all four properties in a little more detail.
The _realizability_ problem consists of checking, whether under the given time
constraints, the specified system can achieve the assigned goal, e.g., always
collect recent pictures of the sensitive locations. In many settings, the
drones themselves or the environment may behave non-deterministically. For
example, if a drone wants to reach a point in the northeast, it may initially
move either north or east, both being equally likely. Similarly, there could
be wind at a particular location, causing any drone under the influence of the
wind to move in the direction of the wind. A stronger property,
_survivability_ , accounts for such nondeterminism and tests whether the
specified system can achieve the assigned goal for all possible outcomes (of
drone actions and environmental influences). The properties of realizability
and survivability represent the two extremes w.r.t. requirements placed on a
system. A system that is realizable can achieve the designed goal in some way.
A system that satisfies survivability will always achieve the goal, under all
circumstances. In some cases, realizability may not be satisfactory, while in
others, survivability may be too costly or unattainable. For such systems,
intermediate solutions are of interest.

To model such intermediate requirements in system design, in this paper we
introduce additional properties, namely _reliability_ and _recoverability_. In
order to ensure system goals, drones should always be able to function. In
particular, drones should always be able to come back to recharge, both in
terms of distance and energy. In other words, drones should never go too far
and reach so-called _points-of-no-return_ where it may no longer be possible
to safely return to home base. Engineers should strive to program drones to
avoid reaching points-of-no-return. This property is referred to as
_recoverability_.

A system satisfies _reliability_ if the system is always able to successfully
continue its expected performance, i.e., the system never gets stuck. For
example, drones should always be able to ensure the system goals, regardless
of the disturbances they have experienced in the environment. At any point in
time, after the drones have successfully monitored sensitive locations for a
certain period of time, they should be able to find a way to continue with
their good performance. For example, considering possible technical failures
and maintenance of the drones, it may be necessary for engineers to call in
additional drones to collectively provide up-to-date images of the entire area
of interest.

Following [16], we focus on a class of systems called _Progressing Timed
Systems_ (PTS), which are specified as timed multiset rewriting theories. In a
PTS, only a finite number of actions can be carried out in a bounded time
interval. In addition to formalizing the properties, we show that the
following relations hold for PTS:

$S_{urvivability}\ \implies\ R_{eliability}\ \Longleftrightarrow\
R_{ecoverability}\ \implies\ R_{ealizability}\ .$

In their spirit, these properties seem similar to safety and liveness
properties [1] or a combination of these properties. However, it is not
straightforward to classify them in these terms. The properties we consider,
defined in Section 4.3, contain an alternation of quantifiers, which makes it
more challenging to formally represent them as a combination of safety and
liveness properties [1].

In our previous work [20, 19, 15, 18], we proposed a timed Multiset Rewriting
(MSR) framework for specifying compliance properties similar to quantitative
safety properties [1, 6] and investigated the complexity of a number of
decision problems. These properties were defined over sets of finite traces,
i.e., executions of a finite number of actions. The above properties, on the
other hand, are defined over _infinite traces_.

The transition to properties over infinite traces leads to many challenges, as
one can easily fall into undecidable fragments of verification problems. The
main challenge is to identify the syntactic conditions on specifications so
that the verification problems fall into a decidable fragment and, at the same
time, that interesting examples can be specified.

The remainder of the paper is organized as follows:

  * •

Following [16], in Section 2 we discuss _Progressing Timed Systems_ (PTS). In
Section 3 we illustrate its expressiveness by encoding a simplified drone
example as a PTS.

  * •

In Section 4 we define a language for specifying the relevant quantitative
temporal properties of timed systems used to define the properties of
_realizability_ , _reliability, recoverability_ and _survivability_.

  * •

In Section 5 we then formally compare the expressiveness of these properties.

  * •

Section 6 investigates the complexity of verification problems that involve
the above properties. While these problems are undecidable in general [20], we
show that they are PSPACE-complete for PTSes. We also show that, when we bound
time (as in bounded-model checking), realizability of PTSes is NP-complete,
survivability is in the $\Delta_{2}^{p}$ class of the polynomial hierarchy and
the reliability is in the $\Pi_{2}^{p}$ class of the polynomial hierarchy
[28]. The upper bound results regarding realizability and survivability were
obtained in [16], while here we obtain new complexity results for the lower
bound complexity results for the $n$-time bounded survivability and the
complexity results relating to reliability from Section 6.

  * •

We also provide a discussion on related and future work, Section 7.

##### Relation to our previous work

This technical report considerably extends the conference paper [16]. It also
updates and subsumes the technical report [17]. For ease of reference, we
include some of the material from [16, 17]. All the material involving
properties of reliability and recoverability is new, including the
investigation of the relations among all four properties from Section 5, the
complexity results relating to reliability from Section 6, and the lower bound
complexity results for $n$-time bounded survivability are new.

##  2 Multiset Rewriting Systems

Assume a finite first-order typed alphabet, $\Sigma$, with variables,
constants, function and predicate symbols. Terms and formulas are constructed
as usual (see [10]) by applying symbols of correct type (or sort).

######  Definition 1 (Fact)

If $P$ is a predicate of type
$\tau_{1}\times\tau_{2}\times\cdots\times\tau_{n}\rightarrow o$, where $o$ is
the type for propositions, and $u_{1},\ldots,u_{n}$ are terms of types
$\tau_{1},\ldots,\tau_{n}$, respectively, then $P(u_{1},\ldots,u_{n})$ is a
_fact_. A fact is _ground_ if it contains no variables.

We assume that the alphabet contains the constant $z:Nat$ denoting zero and
the function $s:Nat\to Nat$ denoting the successor function. Whenever it is
clear from the context, we write $n$ for $s^{n}(z)$ and $(n+m)$ for
$s^{n}(s^{m}(z))$.

In addition, we allow an unbounded number of fresh values [5, 9] to be
involved.

In order to specify timed systems, we attach a timestamp to each fact.

######  Definition 2 (Timestamped Fact)

_Timestamped facts_ are of the form $F@t$, where $F$ is a fact and
$t\in\mathbb{N}$ is a natural number called timestamp.

Note that timestamps are _not_ constructed by using the successor function. To
obtain the complexity results, we use a symbolic representation of the
problems and abstractions that can handle unbounded time values. For more
insight see discussion after Definition 7.

There is a special predicate symbol $Time$ with arity zero that is used to
represent global time.

For simplicity, we often just say facts instead of timestamped facts. Also,
when we want to emphasize the difference between a fact $F$ and a timestamped
fact $F@t$, we say that $F$ is an _untimed fact_.

######  Definition 3 (Configuration)

A configuration is a finite multiset of ground timestamped facts,
$\mathcal{S}=\\{~{}Time@t,~{}F_{1}@t_{1},\ldots,~{}F_{n}@t_{n}~{}\\}$ with a
single occurrence of a $Time$ fact.
Given a configuration $\mathcal{S}$ containing $Time@t$, we say that a fact
$F@t_{F}$ in $\mathcal{S}$ is a _future fact_ if its timestamp is greater than
the global time $t$, i.e., if $t_{F}>t$. Similarly, a fact $F@t_{F}$ in
$\mathcal{S}$ is a _past fact_ if $t_{F}<t$, and a fact $F@t_{F}$ in
$\mathcal{S}$ is a _present fact_ if $t_{F}=t$.

Configurations are to be interpreted as states of the system. Consider the
following configuration where the global time is 4:

$\small\mathcal{S}_{1}=\left\\{\begin{array}[]{l}Time@4,\,Dr(d1,1,2,10)@4,\,Dr(d2,5,5,8)@4,\,P(p1,1,1)@3,\,P(p2,5,6)@0\end{array}\right\\}$

Fact $Dr(d_{Id},x,y,e)@t$ denotes that drone $d_{Id}$ is at position $(x,y)$
at time $t$ with $e$ energy units left in its battery; fact $P(p_{ID},x,y)@t$
denotes that a point to be monitored is at position $(x,y)$ and that the last
picture of it was taken at time $t$. Thus, the above configuration denotes a
scenario with two drones located at positions $(1,2)$ and $(5,5)$ and with 10
and 8 energy units, and with two points to be monitored at positions $(1,1)$
and $(5,6)$, where the former was last photographed at time $3$ and the latter
at time 0.

Using variables, including time variables, we are able to represent (sets of)
configurations of particular form. For example,

$~{}Time@(T+D),\,Dr(X,5,6,Y)@(T+D),\,P(p2,5,6)@T$

specifies that some drone $X$ with $Y$ energy units is currently at the
position $(5,6)$ and that the point of interest at position $(4,6)$ was last
photographed $D$ time units ago. This holds for any configuration containing
the above facts for some instantiation of the variables $T,D,X$ and $Y$.

Configurations are modified by multiset rewrite rules which can be interpreted
as actions of the system. There is only one rule, $Tick$, which represents how
global time advances

$Time@T\longrightarrow Time@(T+1)$ (1)

where $T$ is a time variable denoting the global time. With an application of
a $Tick$ rule, a configuration
$\\{~{}Time@t,\,F_{1}@t_{1},\ldots,\,F_{n}@t_{n}~{}\\}$ representing the state
of a system at time $t$, is replaced with the configuration
$\\{~{}Time@(t+1),\,F_{1}@t_{1},\ldots,\,F_{n}@t_{n}~{}\\}$ representing the
system at time $t+1$.

The remaining rules are _instantaneous_ , since they do not modify global
time, but may modify the remaining facts of configurations (those different
from $Time$). Instantaneous rules have the form:

$\begin{array}[]{l}Time@T,\,\,W_{1}@T_{1},\ldots,\,W_{p}@T_{p},{\color[rgb]{0.65,0,0}\,F_{1}@T_{1}^{\prime}},\ldots,{\color[rgb]{0.65,0,0}\,F_{n}@T_{n}^{\prime}}\
\mid\ \,\mathcal{C}\ \longrightarrow\\\ \ \exists\vec{X}.\,[\
Time@T,\,W_{1}@T_{1},\ldots,\,W_{p}@T_{p},\,{\color[rgb]{0,0.44,0.57}Q_{1}@(T+d_{1})},\ldots,\,{\color[rgb]{0,0.44,0.57}Q_{m}@(T+d_{m})}\,]\end{array}$
(2)

where $d_{1},\ldots,d_{m}$ are natural numbers,
$W_{1}@T_{1},\ldots,\,W_{p}@T_{p},\,F_{1}@T_{1}^{\prime},\ldots,{\,F_{n}@T_{n}^{\prime}}$
are timestamped facts, possibly containing variables, and $\mathcal{C}$ is the
guard of the rule which is a set of constraints involving the time variables
that appear as timestamps of facts in the pre-condition of the rule, i.e., the
variables $T,T_{1},\ldots,T_{p},T_{1}^{\prime},\ldots,T_{n}^{\prime}$. The
facts $W_{i},F_{j}$ and $Q_{k}$ are all different from the fact $Time$ and
$\vec{X}$ are variables that do not appear in
$W_{1},\ldots,\,W_{p},\,F_{1},\ldots,{\,F_{n}}$.

Constraints may be of the form:

$T>T^{\prime}\pm d\quad\textrm{ or }\quad T=T^{\prime}\pm d$ (3)

where $T$ and $T^{\prime}$ are time variables, and $d\in\mathbb{N}$ is a
natural number.

Here and throughout the rest of the paper, the symbol $\pm$ stands for either
$+$ or $-$, i.e., constraints may involve addition or subtraction.

We use $T^{\prime}\geq T^{\prime}\pm d$ to denote the disjunction of
$T>T^{\prime}\pm d$ and $T=T^{\prime}\pm d$. All variables in the guard of a
rule are assumed to appear in the rule’s pre-condition.

Finally, the variables $\vec{X}$ that are existentially quantified in a rule
(Eq. 2) are to be replaced by fresh values, also called _nonces_ in the
protocol security literature [5, 9]. As in our previous work [14], we use
nonces whenever unique identification is required, for example for drone
identification.

Let $\mathcal{W}$ and $\mathcal{W}^{\prime}$ be multisets of timestamped
facts. A rule
$\mathcal{W}\mid\mathcal{C}\longrightarrow\exists\vec{X}.\,\mathcal{W}^{\prime}$
can be applied to a configuration $\mathcal{S}$ if there is a ground
substitution $\sigma$ such that $\mathcal{W}\sigma\subseteq\mathcal{S}$ and
that $\mathcal{C}\sigma$ is true. The resulting configuration is

$\big{(}\,(\mathcal{S}\setminus\mathcal{W})\cup\mathcal{W}^{\prime}\,\big{)}\sigma\
,$

where variables $\vec{X}$ are fresh. More precisely, given a rule $r$, an
instance of a rule is obtained by substituting constants for all variables
appearing in the pre- and post-condition of the rule. This substitution
applies to variables appearing in terms inside facts, to variables
representing fresh values, and to time variables used to specify timestamps of
facts.

An instance of an instantaneous rule can only be applied if all the
constraints in its guard are satisfied. For example, since $0+2<5$ (when
instantiating $T^{\prime}$ as the timestamp of the fact $\,P(p2,5,6)@0$ ) rule

$\small\begin{array}[]{l}Time@T,{\color[rgb]{0.65,0,0}P(I,X,Y)@T^{\prime}},{\color[rgb]{0.65,0,0}Dr(Id,X,Y,E+1)@T}\mid\\{~{}T^{\prime}+2<T~{}\\}\longrightarrow\\\
\qquad\qquad\qquad
Time@T,{\color[rgb]{0,0.44,0.57}P(I,X,Y)@T},{\color[rgb]{0,0.44,0.57}Dr(Id,X,Y,E)@(T+1)}\end{array}$

is applicable to configuration

$\\{\
Time@5,\,Dr(d1,1,2,10)@5,\,Dr(d2,5,6,7)@5,\,P(p1,1,1)@3,\,P(p2,5,6)@0~{}\\}\,,$

resulting in configuration

$\\{\
Time@5,\,Dr(d1,1,2,10)@5,\,Dr(d2,5,6,6)@6,\,P(p1,1,1)@3,\,P(p2,5,6)@5~{}\\}\,,$

but it is not applicable to the following configuration

$\\{\ Time@5,\,Dr(d1,1,2,10)@5,\,Dr(d2,5,5,8)@5,\,P(p1,1,1)@3,\,P(p2,5,6)@4\
\\}\ $

because there are no $\mathcal{P}(p,x,y)@T^{\prime}$ facts in the
configuration such that its timestamp $T^{\prime}$ satisfies the given
constraint, $~{}T^{\prime}+2<T$, involving the global time $T$. Namely,
$3+2~{}{\not}{<}~{}5$ and $4+2~{}{\not}{<}~{}5$.

Following [9] we say that a timestamped fact $F@T$ is _consumed_ by a rule $r$
if that fact occurs more times on the left side than on the right side of the
rule $r$. A timestamped fact $F@T$ is _created_ by some rule $r$ if this fact
occurs more times on the right side than on the left side of the rule $r$.
Hence, facts ${F_{1}@T_{1}^{\prime}},\ldots,{F_{n}@T_{n}^{\prime}}$ are
consumed by rule (Eq. 2) while facts
${Q_{1}@(T+d_{1})},\ldots,{Q_{m}@(T+d_{m})}$ are created by this rule. Note
that a fact $F$ can appear in a rule with different timestamps, but for the
above notions we count instances of the same timestamped fact $F@T$. In a
rule, we usually color red the consumed facts and blue the created facts.

###### Remark 1

Using constraints we are able to formalize time-sensitive properties and
problems that involve explicit time requirements. The set of constraints may,
however, be empty, i.e., rules may have no constraints attached.

We write $\mathcal{S}\longrightarrow_{r}\mathcal{S}^{\prime}$ for the one-step
relation where the configuration $\mathcal{S}$ is rewritten into
$\mathcal{S}^{\prime}$ using an instance of rule $r$. For a set of rules
$\mathcal{R}$, we define
$\mathcal{S}\longrightarrow_{\mathcal{R}}^{*}\mathcal{S}^{\prime}$ to be the
transitive reflexive closure of the one-step relation on all rules in
$\mathcal{R}$. We omit the subscript $\mathcal{R}$, when it is clear from the
context, and simply write
$\mathcal{S}\longrightarrow^{*}\mathcal{S}^{\prime}$.

Note that due to the nature of multiset rewriting, there are various aspects
of non-determinism in the model. For example, different actions and even
different instantiations of the same rule may apply to the same configuration
$\mathcal{S}$, leading to different resulting configurations
$\mathcal{S}^{\prime}$.

######  Definition 4 (Timed MSR System)

A _timed MSR system_ $\mathcal{T}$ is a set of rules containing only
instantaneous rules (Eq. 2) and the $Tick$ rule (Eq. 1).

A trace of a timed MSR system is constructed by a sequence of its rules. In
this paper, we consider both finite and infinite traces. A _finite trace_ of a
timed MSR system $\mathcal{T}$ starting from an initial configuration
$\mathcal{S}_{0}$ is a sequence

$\mathcal{S}_{0}\longrightarrow\mathcal{S}_{1}\longrightarrow\mathcal{S}_{2}\longrightarrow\cdots\longrightarrow\mathcal{S}_{n}$

and an _infinite trace_ of $\mathcal{T}$ starting from an initial
configuration $\mathcal{S}_{0}$ is a sequence

$\mathcal{S}_{0}\longrightarrow\mathcal{S}_{1}\longrightarrow\mathcal{S}_{2}\longrightarrow\cdots\longrightarrow\mathcal{S}_{n}\longrightarrow\cdots$

where for all $i\geq 0$,
$\mathcal{S}_{i}\longrightarrow_{r_{i}}\mathcal{S}_{i+1}$ for some
$r_{i}\in\mathcal{T}$. When a configuration $\mathcal{S}$ apperas in a trace
$P$ we write $\mathcal{S}\in P$.

We will pay particular attention to periods of time represented by traces.
Since time advances by one unit of time per $Tick$ rule, a finite (infinite)
number of $Tick$ rules in a trace represents a finite (infinite) time period.
One can easily imagine traces containing a finite number of $Tick$ rules and
an infinite number of instantaneous rules. Such traces would represent an
infinite number of actions performed in a finite time interval. In this paper
we are not interested in such traces and focus on so called _infinite time
traces_.

######  Definition 5 (Infinite Time Trace)

A trace $P$ of a timed MSR $\mathcal{T}$ is an  _infinite time trace_ if the
time tends to infinity in $P$, i.e., $(\forall n\in\mathbb{N})\
(\exists~{}\mathcal{S}\in P)$ such that $Time@T\in\mathcal{S}$ and $T>n$.

Since in any trace, the global time ticks in single time units, it follows
immediately that any infinite time trace is an infinite trace, and it contains
an infinite number of $Tick$ rules.

We have shown in our previous work [21, 14, 20, 15, 18] that problems
involving MSR, such as checking whether a configuration can be reached, are
undecidable if no further restrictions are imposed. These problems are
undecidable already when considering only finite traces. However, these
problems are decidable for balanced MSR systems [21, 20] that assume an upper-
bound, $k$, on the size of facts formally defined below.

######  Definition 6 (Balanced System)

A timed MSR system $\mathcal{T}$ is _balanced_ if for all instantaneous rules
$r\in\mathcal{T}$, $r$ creates the same number of facts as it consumes, i.e.,
the instantaneous rules are of the form:

$\begin{array}[]{l}Time@T,\,\mathcal{W},{\color[rgb]{0.65,0,0}\,F_{1}@T_{1}^{\prime}},\ldots,{\color[rgb]{0.65,0,0}\,F_{n}@T_{n}^{\prime}}\
\mid\ \,\mathcal{C}\ \longrightarrow\\\ \ \ \exists\vec{X}.~{}[\
Time@T,\,\mathcal{W},{\color[rgb]{0,0.44,0.57}\,Q_{1}@(T+d_{1})},\ldots,{\color[rgb]{0,0.44,0.57}\,Q_{n}@(T+d_{n})}\,]\
.\end{array}$ (4)

By consuming and creating facts, rewrite rules can increase and decrease the
number of facts in configurations throughout a trace. However, in balanced MSR
systems, rule application does not affect the number of facts in a
configuration. That is, enabling configuration has the same number of facts as
the resulting configuration. Hence, the number of facts in configurations is
constant throughout a trace.

######  Definition 7 (Size of a Fact)

The size of a timestamped fact $P@T$, written $|P@T|$ is the total number of
alphabet symbols appearing in $P$.

For instance, $|P(s(z),f(a,X),a)@12|=7$. For our complexity results, we assume
a bound, $k$, on the size of facts. Without this bound (among other
restrictions), any interesting decision problem is shown undecidable by
encoding the Post correspondence problem [9]. Note that the value of the
timestamp is not considered in the size of facts. For the complexity results,
the (unbounded) time values of timestamps are handled using the abstractions
and the symbolic representation of the problems.

###  2.1 Progressing Timed Systems

Following [16], we discuss a particular class of timed MSR systems, called
_progressing timed MSR systems_ (PTSes), in which only a finite number of
actions can be carried out in a bounded time interval. This is a natural
condition for many systems, similar similar to the _finite-variability
assumption_ used in the temporal logic and timed automata literature.

######  Definition 8 (Progressing Timed System)

A timed MSR system $\mathcal{A}$ is a _progressing timed MSR system (PTS)_ if
$\mathcal{T}$ is balanced and for all instantaneous rules $r\in\mathcal{T}$:

  * i)

Rule $r$ creates _at least one_ fact with timestamp greater than the global
time, i.e., in (Eq. 2), $d_{i}\geq 1$ for at least one $i\in\\{1,\dots,n\\}$;

  * ii)

Rule $r$ consumes _only_ facts with timestamps in the past or at the current
time, i.e., in (Eq. 2), the set of constraints $\mathcal{C}$ contains the set

$\mathcal{C}_{r}=\\{~{}T\geq T_{i}^{\prime}\mid F_{i}@T_{i}^{\prime},~{}1\leq
i\leq n~{}\\}\ .$

For the sake of readability, from this point on we assume that for all rules
$r$ the set of their constraints implicitly contains the set
$\mathcal{C}_{r}$, as shown in Definition 8, and do not always write
$\mathcal{C}_{r}$ explicitly in our specifications.

The following rule, which denotes the action of a drone taking a photo of a
point of interest, is an example of a rule in a PTS:

$\begin{array}[]{l}Time@T,{\color[rgb]{0.65,0,0}~{}P(I,X,Y)@T^{\prime}},{\color[rgb]{0.65,0,0}~{}Dr(Id,X,Y,E+1)@T}~{}\mid~{}\\{~{}T^{\prime}<T~{}\\}\longrightarrow\\\
\qquad\qquad\qquad
Time@T,{\color[rgb]{0,0.44,0.57}~{}P(I,X,Y)@T},{\color[rgb]{0,0.44,0.57}~{}Dr(Id,X,Y,E)@(T+1)}\end{array}$

Note that the constraint $T^{\prime}<T$ is used to prevent drones from
repeatedly photographing the same point of interest at the same time to save
energy. Also, the created future fact prevents the same drone from performing
the same action in the same time unit.

The following proposition [16] establishes a bound on the number of instances
of instantaneous rules appearing between two consecutive instances of $Tick$
rules in a trace of a PTS. This bound is then used to formalize the intuition
that PTSes always move things forward.

###### Proposition 1

Let $\mathcal{T}$ be a PTS, $\mathcal{S}_{0}$ an initial configuration and $m$
the number of facts in $\mathcal{S}_{0}$. For all traces $\mathcal{P}$ of
$\mathcal{T}$ starting from $\mathcal{S}_{0}$, let

$\mathcal{S}_{i}\longrightarrow_{Tick}\mathcal{S}_{i+1}\longrightarrow\cdots\longrightarrow\mathcal{S}_{j}\longrightarrow_{Tick}\mathcal{S}_{j+1}$

be any subtrace of $\mathcal{P}$ with exactly two instances of the $Tick$
rule, one at the beginning and the other at the end. Then $j-i<m$. [16]

###### Proof

The statement easily follows from Definition 8. Let $\mathcal{P}$ be an
arbitrary trace in $\mathcal{T}$ and

$\mathcal{S}_{i}\longrightarrow_{Tick}\mathcal{S}_{i+1}\longrightarrow\cdots\longrightarrow\mathcal{S}_{j}\longrightarrow_{Tick}\mathcal{S}_{j+1}$

an arbitrary subtrace of $\mathcal{P}$ with exactly two instances of the
$Tick$ rule. All the rules between $Tick$ rules in the above subtrace are
instantaneous.

Since $\mathcal{T}$ is a PTS, the application of any instantaneous rule
creates at least one future fact and consumes at least one present or past
fact. In other words, an application of an instantaneous rule reduces the
total number of past and present facts in the configuration.

Since the system $\mathcal{T}$ is balanced, all the above configurations
$\mathcal{S}_{i},\dots,\mathcal{S}_{j}$ have the same number of facts, $m$.
Recall also that the fact $Time$ does not change when the instantaneous rules
are applied. Thus, since there are at most $m-1$ present or past facts
different from $Time$ in any $\mathcal{S}_{k}$, $i<k\leq j$, a series of at
most $m-1$ instantaneous rules can be applied between two $Tick$ rules. ∎

According to the above statement, in a PTS an unbounded number of
instantaneous rules cannot be applied in a bounded interval of time. Also,
from the above result we can conclude that infinite traces in PTSes represent
infinite time periods. In particular, this means that in traces of PTSes there
are no phenomena similar to Zeno paradox. This is stated in the following
proposition.

###### Proposition 2

Let $\mathcal{T}$ be a PTS. All infinite traces of $\mathcal{T}$ are infinite
time traces, i.e., traces where time tends to infinity. [16]

###### Proof

Assume that in some infinite trace $\mathcal{P}$ of a PTS $\mathcal{T}$ the
current time does not exceed some value $M$. Then, since timestamps are
natural numbers, and time advances by a single time unit, there are at most
$M$ time ticks in $\mathcal{P}$.

According to Proposition 1 there are at most $m-1$ instantaneous rules between
any $Tick$ rule and the next $Tick$ rule in $\mathcal{P}$.

Consequently, in total, there are at most $(M+1)\cdot(m-1)+M$ rules in
$\mathcal{P}$, i.e., $\mathcal{P}$ is a finite trace. Contradiction. ∎

Finally, notice that the PTS model has many syntactic conditions, e.g.,
balanced condition (Definition 6), the form of time constraints (Eq. 3), the
form of instantaneous rules (Eq. 2). Each of these conditions has been
carefully developed. As we have shown in our previous work [20], relaxing any
of these conditions leads to undecidability of important verification
problems, such as the reachability problem, over finite traces. Clearly, these
conditions are also needed for infinite traces.

The additional challenge in allowing infinite traces is to make sure that time
advances in such a way that traces represent arbitrarily large time periods.
Our definition of PTS is a simple and elegant way to enforce this. Moreover,
as we show in Section 3, it is still possible to specify many interesting
examples with our PTS model, including our motivating example, and still prove
the decidability of our verification problems involving infinite traces
(Section 6).

##  3 Programming Drone Behavior using PTS

$\begin{array}[]{l}Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0.65,0,0}\,Dr(Id,X,Y,E+1)@T}\,\mid\,doMove\,(Id,X,Y,E+1,T,T_{1},\ldots,T_{n},north)\\\
\qquad\qquad\longrightarrow
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0,0.44,0.57}\,Dr(Id,X,Y+1,E)@(T+1)}\\\\[5.0pt]
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0.65,0,0}\,Dr(Id,X,Y+1,E+1)@T}\longrightarrow\\\
\qquad\qquad\mid
doMove\,(Id,X,Y+1,E+1,T,T_{1},\ldots,T_{n},south)\longrightarrow\\\
\qquad\qquad\qquad
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0,0.44,0.57}\,Dr(Id,X,Y,E)@(T+1)}\\\\[5.0pt]
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0.65,0,0}\,Dr(Id,X+1,Y,E+1)@T}\longrightarrow\\\
\qquad\qquad\mid
doMove\,(Id,X+1,Y,E+1,T,T_{1},\ldots,T_{n},west)\longrightarrow\\\
\qquad\qquad\qquad
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0,0.44,0.57}\,Dr(Id,X,Y,E)@(T+1)}\\\\[5.0pt]
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0.65,0,0}\,Dr(Id,X,Y,E+1)@T}\mid
doMove\,(Id,X,Y,E+1,T,T_{1},\ldots,T_{n},east)\\\ \qquad\qquad\longrightarrow
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0,0.44,0.57}\,Dr(Id,X,Y,E)@(T+1)}\\\\[5.0pt]
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0.65,0,0}\,Dr(Id,x_{b},y_{b},E)@T}\mid
doCharge\,(Id,E,T,T_{1},\ldots,T_{n})\longrightarrow\\\ \qquad\qquad
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n}),{\color[rgb]{0,0.44,0.57}\,Dr(Id,x_{b},y_{b},E+1)@(T+1)}\\\\[5.0pt]
Time@T,\,P(p_{1},X_{1},Y_{1})@T_{1},\ldots,{\color[rgb]{0.65,0,0}\,P(p_{i},X,Y)@T_{i}},\ldots,P(p_{n},X_{n},Y_{n}<EMAIL_ADDRESS>\qquad\mid\
doClick\,(Id,X,Y,E,T,T_{1},\ldots,T_{i},\ldots,T_{n})\longrightarrow
Time@T,\\\\[3.0pt] \qquad\ \ \
P(p_{1},X_{1},Y_{1})@T_{1},\ldots,{\color[rgb]{0,0.44,0.57}\,P(p_{i},X,Y)@T},\ldots,\,P(p_{n},X_{n},Y_{n})@T_{n},{\color[rgb]{0,0.44,0.57}\,Dr(Id,X,Y,E-1)@(T+1)}\\\\[5.0pt]
Time@T,{\color[rgb]{0.65,0,0}\,Dr(Id,X,Y,E)@T}\mid
hasWind\,(X,Y,north)\longrightarrow
Time@T,{\color[rgb]{0,0.44,0.57}Dr(Id,X,Y+1,E)@(T+1)}\\\\[5.0pt]
Time@T,{\color[rgb]{0.65,0,0}\,Dr(Id,X,Y+1,E)@T}\mid
hasWind\,(X,Y,south)\longrightarrow
Time@T,{\color[rgb]{0,0.44,0.57}Dr(Id,X,Y,E)@(T+1)}\\\\[5.0pt]
Time@T,{\color[rgb]{0.65,0,0}\,Dr(Id,X+1,Y,E)@T}\mid
hasWind\,(X,Y,west)\longrightarrow
Time@T,{\color[rgb]{0,0.44,0.57}\,Dr(Id,X,Y,E)@(T+1)}\\\\[5.0pt]
Time@T,{\color[rgb]{0.65,0,0}\,Dr(Id,X,Y,E)@T}\mid
hasWind\,(X,Y,east)\longrightarrow
Time@T,{\color[rgb]{0,0.44,0.57}\,Dr(Id,X+1,Y,E)@(T+1)}\end{array}$ Figure 1:
Macro rules specifying the scenario where drones take pictures of points of
interest. Here $\mathcal{P}(p_{1},\ldots,p_{n})$ denotes
$P(p_{1},X_{1},Y_{1})@T_{1},\ldots,P(p_{n},X_{n},Y_{n})@T_{n}$. Moreover, we
assume that the Drone stay in a grid of size $x_{max}\times y_{max}$ and have
at most $e_{max}$ energy units.

Following [16], Figure 1 depicts the macro rules of our motivating scenario
where drones are moving on a fixed grid of size $x_{max}\times y_{max}$, have
at most $e_{max}$ energy units and take pictures of some points of interest.
We assume that there are $n$ such points $p_{1},\ldots,p_{n}$, where $n$ is
fixed, a base station is at position $(x_{b},y_{b})$, and that the drones
should regularly take pictures so that all pictures are recent. That is, at
any time, each of the points of interest should have been photographed in the
last $M$ time units, for some given $M$.

Clearly if drones non-deterministically choose to move in some direction
without a particular strategy, they will fail to achieve the assigned goal. A
strategy of a drone can be specified using time constraints.

For this example, the strategy would depend on the difference $T-T_{i}$, for
$1\leq i\leq n$, specifying the elapsed time since the last picture of the
point $p_{i}$ was taken. This can be specified with the following set of time
constraints:

$\mathcal{T}(d_{1},\ldots,d_{n})=\\{~{}T-T_{1}=d_{1},\ldots,T-T_{n}=d_{n}~{}\\}$

where for all $1\leq i\leq n$ we instantiate $d_{i}$ by values in
$\\{0,\ldots,M\\}$.

For example, the macro rule with
$doMove\,(Id,X,Y,E+1,T,T_{1},\ldots,T_{n},north)$ in Figure 1 is replaced by
the set of rules:

$\small\begin{array}[]{l}Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n})@T,{\color[rgb]{0.65,0,0}\,Dr(d1,0,0,1)@T}\\\
\qquad\qquad\qquad\qquad\qquad\qquad\qquad\ \ \mid\
\mathcal{T}(0,\ldots,0),\,DoMv\,(d1,0,0,1,0,\ldots,0,north)\\\\[2.0pt]
\quad\qquad\longrightarrow
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n})@T,{\color[rgb]{0,0.44,0.57}\,Dr(Id,0,1,0)@(T+1)}\\\\[5.0pt]
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n})@T,{\color[rgb]{0.65,0,0}\,Dr(d1,0,0,1)@T}\\\
\qquad\qquad\qquad\qquad\qquad\qquad\qquad\ \ \ \mid\
\mathcal{T}(0,\ldots,1),\,DoMv\,(d1,0,0,1,0,\ldots,1,north)\\\\[2.0pt]
\quad\qquad\longrightarrow
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n})@T,{\color[rgb]{0,0.44,0.57}\,Dr(Id,0,1,0)@(T+1)}\\\
\qquad\cdots\\\
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n})@T,{\color[rgb]{0.65,0,0}\,Dr(d2,x_{max},y_{max}-1,e_{max})@T}\\\
\qquad\qquad\qquad\mid\
\mathcal{T}(M,\ldots,M),\,DoMv\,(d2,x_{max},y_{max}-1,e_{max},M,\ldots,M,north)\\\\[2.0pt]
\quad\qquad\longrightarrow\
Time@T,\,\mathcal{P}(p_{1},\ldots,p_{n})@T,{\color[rgb]{0,0.44,0.57}\,Dr(Id,x_{max},y_{max},e_{max}-1)@(T+1)}\\\
\end{array}$

where $doMove$ returns a tautology or an unsatisfiable constraint depending on
the desired behavior of the drone.

Finally, macro rules for moving the drone, taking a picture, charging, and
macro specifying winds are similarly defined.

While most of the rules have the expected result, we only explain the click
and wind rules. The click rule is applicable if the drone is at the position
of some point of interest. If applied, the timestamp of the fact
$P(p_{i},X,Y)$ is updated to the current time $T$. The wind rule is similar to
the move rules moving the drone to some direction, but does not cause the
drone to consume its energy.

In our implementation in [16] we used a more sophisticated approach described
in [31] using soft-constraints to specify a drone’s strategy. It can be
translated into a PTS that incorporates the strategy described above.

##### Other Examples

Besides examples involving drones, other exampels also seem to be progressing.
For example, in our previous work [20], we specify a monitor for clinical
trials using our timed MSR system framework with discrete time. This
specification is progressing.

There are a number of other examples which we have been investigating and that
are progressing. For example, [30] models a simplified version of a package
delivery systems inspired by Amazon’s Prime Air service, and [31] models a
patrolling bot which moves from one point to another. All these examples seem
to be progressing.

##  4 Quantitative Temporal Properties

Following [16], we begin the Section 4.1 by discussing critical
configurations, a language used to define desirable properties of systems.
This is a key concept in our framework, used to describe explicit timing
constraints that a system should satisfy. In Section 4.2 we discuss lazy time
sampling, which is a condition on traces that intuitively enforces that
systems react at the expected time. Then in Section 4.3, we discuss a number
of verification problems.

###  4.1 Critical Configurations and Compliant Traces

Critical configurations specifications are used for specifying bad
configurations that should be avoided by a system.

######  Definition 9 (Critical Configuration)

_Critical configuration specification_ is a set of pairs

$\mathcal{CS}=\\{~{}\langle\mathcal{S}_{1},\mathcal{C}_{1}\rangle,\ldots,\langle\mathcal{S}_{n},\mathcal{C}_{n}\rangle~{}\\}\
.$

Each pair $\langle\mathcal{S}_{j},\mathcal{C}_{j}\rangle$ is of the form:

$\langle~{}\\{F_{1}@T_{1},\ldots,F_{p_{j}}@T_{p_{j}}\\},\mathcal{C}_{j}~{}\rangle$

where $T_{1},\ldots,T_{p_{j}}$ are time variables, $F_{1},\ldots,F_{p_{j}}$
are facts (possibly containing variables) and $\mathcal{C}_{j}$ is a set of
time constraints involving only the variables $T_{1},\ldots,T_{p_{j}}$.

Given a critical configuration specification, $\mathcal{CS}$, we classify a
configuration $\mathcal{S}$ as _critical_ w.r.t. $\mathcal{CS}$ if for some
$1\leq i\leq n$, there is a grounding substitution, $\sigma$, such that:

  * •

$\mathcal{S}_{i}\sigma\subseteq\mathcal{S}$;

  * •

All constraints in $\mathcal{C}_{i}\sigma$ are satisfied.

The substitution application ($\mathcal{S}\sigma$) is defined as usual [10],
i.e., by mapping time variables in $\mathcal{S}$ to natural numbers, nonce
names to nonce names (renaming of nonces), and non-time variables to terms.
Notice that nonce renaming is assumed, since the particular nonce name should
not matter for classifying a configuration as critical. Nonce names cannot be
specified in advance, since they are freshly generated in a trace, i.e.,
during the execution of the process being modelled.

###### Example 1

We can specify usual safety conditions which do not involve time. For example,
a drone should never run out of energy. This can be specified by using the
following set of critical configuration specification:

$\\{~{}\langle~{}\\{Dr(Id,X,Y,0)@T\\},\emptyset~{}\rangle\mid
Id\in\\{d1,d2\\},X\in\\{0,\ldots,x_{max}\\},Y\in\\{0,\ldots,y_{max}\\}~{}\\}\
.$

###### Example 2

The following critical configuration specification specifies a quantitative
property involving time:

$\begin{array}[]{l}\\{~{}\langle~{}\\{P(p_{1},x_{1},y_{1})@T_{1},Time@T\\},\\{\,T>T_{1}+M\,\\}~{}\rangle,\ldots\\\
\qquad\qquad\ldots,\langle~{}\\{P(p_{n},x_{n},y_{n})@T_{n},Time@T\\},\\{\,T>T_{n}+M\,\\}~{}\rangle~{}\\}\
.\end{array}$

Together with the specification in Figure 1, this critical configuration
specification specifies that the last pictures of all points of interest (
i.e., $p_{1},\ldots,p_{n}$ located at $(x_{1},y_{1}),\ldots,(x_{n},y_{n})$ )
should have timestamps no more than $M$ time units old.

###### Example 3

Let the facts $St(Id,x_{b},y_{b})@T_{1}$ and $St(empty,x_{b},y_{b})@T_{1}$
denote, respectively, that at time $T_{1}$ the drone $Id$ entered the base
station located at $(x_{b},y_{b})$ to recharge, and that the station is empty.
Moreover, assume that only one drone may be positioned in a station to
recharge, which would be specified by adding the following rules specifying
the drone landing and take off:

$\begin{array}[]{l}Time@T,{\color[rgb]{0.65,0,0}\,Dr(Id,X,Y)@T},{\color[rgb]{0.65,0,0}\,St(empty,X,Y)@T_{1}}\longrightarrow\\\
\quad
Time@T,{\color[rgb]{0,0.44,0.57}\,Dr(Id,X,Y<EMAIL_ADDRESS>Time@T,{\color[rgb]{0.65,0,0}\,Dr(Id,X,Y)@T},{\color[rgb]{0.65,0,0}\,St(Id,X,Y)@T_{1}}\longrightarrow\\\
\quad
Time@T,{\color[rgb]{0,0.44,0.57}\,Dr(Id,X,Y)@(T+1)},{\color[rgb]{0,0.44,0.57}\,St(empty,X,Y)@T}\\\
\end{array}$

Then, the critical configuration specification

$\\{~{}\langle\\{St(Id,X,Y)@T_{1},Time@T\\},\\{\,T>T_{1}+M_{1}\,\\}\,\rangle\mid
Id\in\\{d1,d2\\}\,\\}$

specifies that one drone should not remain in a base station for too long
(more than $M_{1}$ time units) preventing other drones to charge.

###### Example 4

Fresh values may be useful in specifying various critical configurations which
may involve identification, history of events or communication protocols. For
example, drones may communicate between themselves to coordinate their
flights. They may also use cryptographic protocols with other agents in the
system, e.g., to send pictures of points of interest to be stored on the
system data base. Such applications and requirements are easily formalized
using fresh values.
For example, drones must be uniquely identified, i.e., should not have the
same $Id$:

$\\{~{}\langle{~{}\\{Dr(Id,X,Y,E)@T,~{}\\{Dr(Id,X^{\prime},Y^{\prime},E^{\prime})@T^{\prime}\\},\emptyset~{}}\rangle\\}\
.$

Also, in case recharging of batteries is separately managed and billed, even
visits to the recharge stations should be uniquely identified for correct
billing. Similarly, pictures of points of interest may require identification
for documentation. In that case, rules given in Figure 1 can easily be
modified to include fresh values, e.g., by replacing $P(p_{i},X,Y)$ facts with
$P(n,p_{i},X,Y)$ facts in all rules, and including creation of fresh value $n$
in the rule involving $doClick$ constraint.

######  Definition 10 (Compliant Trace)

A trace $\mathcal{P}$ of a timed MSR system is _compliant_ w.r.t. a given
critical configuration specification $\mathcal{CS}$ if $\mathcal{P}$ does not
contain any configuration that is critical w.r.t. $\mathcal{CS}$.

Note that if the critical configuration specification is empty, no
configuration is critical, i.e., all traces are compliant.

For simplicity, when the corresponding critical configuration specification is
clear from the context, we will elide it and use terminology critical
configuration. Also, when it is clear from the context, we often elide the
timed MSR system and the critical configuration specification with respect to
which we consider critical configurations, and simply say that a trace is
compliant.

###  4.2 Time Sampling

Following [16], in order to define sensible quantitative verification
properties, we need to assume some conditions on when the Tick rule is
applicable. Otherwise, any MSR system allows traces containing only instances
of $Tick$ rules:

$\mathcal{S}_{1}\longrightarrow_{Tick}\mathcal{S}_{2}\longrightarrow_{Tick}\mathcal{S}_{3}\longrightarrow_{Tick}\mathcal{S}_{4}\longrightarrow_{Tick}\cdots$

In such a trace, the system never acts to avoid critical configurations and
would easily contain a critical configuration $\mathcal{S}_{j}$, related to
some constraint $T>T^{\prime}+d$, involving global time $T$ and sufficiently
large $j$.

Imposing a _time sampling_ is one way to avoid such traces where the time
simply ticks. Time sampling is used, for example, in the semantics of
verification tools such as Real-Time Maude [26]. In particular, time sampling
dictates when the $Tick$ rule must be applied and when it cannot be applied.
Such a treatment of time is used for both dense and discrete times in
searching and model checking timed systems.

######  Definition 11 (Lazy Time Sampling (l.t.s.))

A (possibly infinite) trace $\mathcal{P}$ of a timed MSR system $\mathcal{T}$
uses _lazy time sampling_ if for any occurrence of the $Tick$ rule
$\mathcal{S}_{i}\longrightarrow_{Tick}\mathcal{S}_{i+1}$ in $\mathcal{P}$, no
instance of any instantaneous rule in $\mathcal{T}$ can be applied to the
configuration $\mathcal{S}_{i}$.

In lazy time sampling instantaneous rules are given a higher priority than the
$Tick$ rule. Under this time sampling, a drone should carry out one of the
rules in Figure 1 at each time while time can only advance when all drones
have carried out their actions for that moment. This does not mean, however,
that the drones will satisfy their goal of always having recent pictures of
the points of interest as this would depend on the behavior of the system,
i.e., the actions carried out by the drones.

In the remainder of this paper, we focus on the lazy time sampling. We leave
it to future work to investigate whether similar results hold for other time
sampling schemes.

###  4.3 Verification Problems

Four properties are discussed in this section: Realizability and Survivability
from [16] and the new properties of reliability and recoverability. Figure 2
illustrates these properties, which we define below. Since the names of the
properties sound similar in English, we also introduce one-letter names for
the properties for better readability and differentiation.

The first property we discuss is realizability. It guarantees that the given
system can achieve the assigned goal under the given time constraints and
design specifications, e.g., that drones can repeatedly collect up-to-date
images of the sensitive locations.

Realizability is useful for increasing confidence in a specified system, since
a system that is not realizable cannot accomplish the given tasks (specified
by a critical specification) and the designer would therefore have to
reformulate it.

However, if a system is shown to be realizable, the trace, $\mathcal{P}$, that
proves realizability could also provide insights into the sequence of actions
that lead to accomplishment of the specified tasks. This can be used to refine
the specification and reduce possible non-determinism.

######  Definition 12 (Realizability / $Z$ property)

A timed MSR system $\mathcal{T}$ satisfies _realizability_ with respect to an
initial configuration $\mathcal{S}_{0}$, a critical configuration
specification $\mathcal{CS}$ and the l.t.s. if there _exists_ a compliant
infinite time trace from $\mathcal{S}_{0}$ that uses the l.t.s. 111 For
simplicity, in the rest of the paper, for properties of systems and
configurations, we will not always explicitly state the critical configuration
specification, initial configuration, and/or time sampling with respect to
which the property is considered. For example, when it is clear from the
context, we simply say that a system satisfies $Z$ property or is
_realizable_.
Also, when for a property of an MSR $\mathcal{T}$ we only consider traces that
use lazy time sampling, we also say that $\mathcal{T}$ _uses the lazy time
sampling_. [16]

The $Z$ property of a timed MSR $\mathcal{T}$ w.r.t.
$\mathcal{S}_{0},\mathcal{CS}$ and l.t.s. can be expressed using the formula:

$F_{\text{$Z$~{}}}(\mathcal{T},\mathcal{S}_{0}):=\exists\,t\in\textsf{T}^{\mathcal{T},\mathcal{S}_{0}}.[t\in\textsf{T}_{time}^{\mathcal{T}}\cap\textsf{T}_{lts}^{\mathcal{T}}\cap\textsf{T}_{c}^{\mathcal{T}}],$

where $\textsf{T}^{\mathcal{T},\mathcal{S}_{0}}$ is the set of all traces of
$\mathcal{T}$ starting from $\mathcal{S}_{0}$,
$\textsf{T}_{time}^{\mathcal{T}}$ is the set of all infinite time traces of
$\mathcal{T}$, $\textsf{T}_{lts}^{\mathcal{T}}$ is the set of all traces of
$\mathcal{T}$ that use the l.t.s. and $\textsf{T}_{c}^{\mathcal{T}}$ is the
set of all traces of $\mathcal{T}$ compliant w.r.t. $\mathcal{CS}$.

Open distributed systems are inherently non-deterministic due to, e.g., the
influence of the environment with winds. Therefore, it is important to know
whether the system can avoid critical configurations despite non-determinism.
We call this property _survivability._

######  Definition 13 (Survivability / $S$ property)

A timed MSR $\mathcal{T}$ satisfies _survivability_ w.r.t. an initial
configuration $\mathcal{S}_{0}$, a critical configuration specification
$\mathcal{CS}$ and the l.t.s. if it satisfies realizability with respect to
$\mathcal{S}_{0}$, $\mathcal{CS}$, and the l.t.s. and if _all_ infinite time
traces from $\mathcal{S}_{0}$ that use the l.t.s. are compliant. [16]

Using the above notation, the $S$ property of a timed MSR $\mathcal{T}$ can be
expressed with:

$F_{\text{$S$~{}}}(\mathcal{T},\mathcal{S}_{0}):=F_{\text{$Z$~{}}}(\mathcal{T},\mathcal{S}_{0})\land\forall\,t\in\textsf{T}^{\mathcal{T},\mathcal{S}_{0}}.[t\in\textsf{T}_{time}^{\mathcal{T}}\cap\textsf{T}_{lts}^{\mathcal{T}}\Rightarrow
t\in\textsf{T}_{c}^{\mathcal{T}}].$

Although survivability is a desirable property, much more so than
realizability, it can sometimes be a rather severe requirement for a system,
or even unachievable. Hence, when designing a system, one may want to
compromise and consider less demanding properties. For example, one may want
to avoid configurations that appear as “dead-ends”, i.e., configurations that
necessarily lead to critical configurations. We call such configurations
_points-of-no-return_. For example, drones should not fly so far that it is no
longer possible to reach a recharging station due to energy consumption.

(a) $Z$ property (b) $S$ property (c) point-of-no-return (d) $V$ property (e)
$L$ property

Figure 2: Illustration of properties of (a) realizability, (b) survivability,
(d) recoverability, and (e) reliability, as well as configurations that are a
point-of-no-return (c). Green lines represent compliant traces that use lazy
time sampling, while red lines represent traces that use lazy time sampling,
but are not compliant. Red circles represent critical configurations, while
green circles are not critical. Quantification marked with $t\to\infty$
denotes quantification over infinite time traces.

######  Definition 14 (Point-of-No-Return)

Given a timed MSR system $\mathcal{T}$, a configuration $\mathcal{S}$ is
called a _point-of-no-return_ with respect to a critical configuration
specification $\mathcal{CS}$ and the l.t.s. if $\mathcal{S}$ is _not_ critical
with respect to $\mathcal{CS}$, and if _all_ infinite traces of $\mathcal{T}$
starting with $\mathcal{S}$ and using the l.t.s. are not compliant with
respect to $\mathcal{CS}$.

The set of all configurations that are points-of-no-return of a timed MSR
$\mathcal{T}$, $\textsf{C}_{pon}^{\mathcal{T}}$, can be described as
$\textsf{C}_{pon}^{\mathcal{T}}:=\\{\mathcal{S}\mid\mathcal{S}\notin\textsf{C}_{cr}^{\mathcal{T}}\land\forall\,t.[t\in\textsf{T}^{\mathcal{T},\mathcal{S}}\cap\textsf{T}_{\infty}^{\mathcal{T}}\cap\textsf{T}_{lts}^{\mathcal{T}}\
\Rightarrow\ t\notin\textsf{T}_{c}^{\mathcal{T}}]\\},$ where
$\textsf{C}_{cr}^{\mathcal{T}}$ is the set of all critical configurations of
$\mathcal{T}$ and $\textsf{T}_{\infty}^{\mathcal{T}}$ is the set of all
infinite traces of $\mathcal{T}$.

There exists no compliant infinite trace from a point-of-no-return that uses
the l.t.s. A point-of-no-return itself is not critical, but must eventually
lead to a critical configuration on every infinite trace that uses the l.t.s.
Therefore, configurations such as points-of-no-return are not desirable w.r.t.
goal achievement, i.e., points-of-no-return should be avoided when searching
for (infinite) compliant traces.

###### Remark 2

A point-of-no-return represents the system that still satisfies the required
conditions, but it will inevitably fall into a bad state where this is no
longer the case. Therefore, to better distinguish between points-of-no-return
and critical configurations, the condition that a point-of-no-return is not
critical is included in the definition.

Using the notion of points-of-no-return, we introduce new properties of our
systems.

######  Definition 15 (Recoverability / $V$ property)

A timed MSR system $\mathcal{T}$, satisfies _recoverability_ with respect to
an initial configuration $\mathcal{S}_{0}$, a critical configuration
specification $\mathcal{CS}$ and the l.t.s. if it satisfies realizability with
respect to $\mathcal{S}_{0}$, $\mathcal{CS}$ and the l.t.s. and if no point-
of-no-return is reachable from $\mathcal{S}_{0}$ on a compliant trace that
uses the l.t.s. That is, if a configuration $\mathcal{S}$ is reachable from
$\mathcal{S}_{0}$ on a compliant trace that uses the l.t.s., then
$\mathcal{S}$ is not a point-of-no-return.

The $V$ property of a timed MSR $\mathcal{T}$ can be expressed with the
following formula:

$F_{\text{$V$~{}}}(\mathcal{T},\mathcal{S}_{0}):=F_{\text{$Z$~{}}}(\mathcal{T},\mathcal{S}_{0})\land[\forall\,t\in\textsf{T}^{\mathcal{T},\mathcal{S}_{0}}\cap\textsf{T}_{c}^{\mathcal{T}}\cap\textsf{T}_{lts}^{\mathcal{T}}.\forall\mathcal{S}\in
t.\mathcal{S}\notin\textsf{C}_{pon}^{\mathcal{T}}].$

Configurations that are points-of-no-return should be avoided. For example, a
drone may enter an area where it may end up with empty batteries due to
frequent high winds. Such points should be avoided. In fact, with the $V$
property we want to ensure that all finite compliant traces from the initial
configuration that use the l.t.s. can be extended to infinite compliant traces
that use the l.t.s.

Next, with the reliability property, we want to ensure that as long as one
follows a compliant trace, there is a way to extend the trace to a compliant
infinite time trace. In our drone scenario, a reliable system should be
designed so that as long as the drones follow instructions, including rules
for flying in high winds, there is always a way for the drones to avoid
critical configurations.

######  Definition 16 (Reliability / $L$ property)

A timed MSR system $\mathcal{T}$ satisfies _reliability_ with respect to an
initial configuration $\mathcal{S}_{0}$, a critical configuration
specification $\mathcal{CS}$, and the l.t.s. if it satisfies realizability
with respect to $\mathcal{S}_{0}$, $\mathcal{CS}$, and the l.t.s. and if for
_any_ configuration $\mathcal{S}$ reachable from $\mathcal{S}_{0}$ on a
_compliant_ trace that uses the l.t.s., there exists a compliant infinite time
trace from $\mathcal{S}$ that uses the l.t.s.

The $L$ property of a timed MSR $\mathcal{T}$ can be expressed with the
following formula:

$\begin{array}[]{l}F_{\text{$L$~{}}}(\mathcal{T},\mathcal{S}_{0}):=F_{\textrm{$Z$~{}}}(\mathcal{T},\mathcal{S}_{0})\
\land\\\ \qquad\qquad\quad[\forall
t\in\textsf{T}^{\mathcal{T},\mathcal{S}_{0}}\cap\textsf{T}_{c}^{\mathcal{T}}\cap\textsf{T}_{lts}^{\mathcal{T}}.\forall\mathcal{S}\in
t.\exists\,t^{\prime}\in\textsf{T}^{\mathcal{T},\mathcal{S}}.~{}t^{\prime}\in\textsf{T}_{c}^{\mathcal{T}}\cap\textsf{T}_{lts}^{\mathcal{T}}\cup\textsf{T}_{time}^{\mathcal{T}}].\end{array}$

A timed MSR system that satisfies the $L$ property represents a system that is
always able to avoid points-of-no-return. Such a system satisfies the $Z$
property, but it may not satisfy the $S$ property. Indeed, the class of
systems satisfying the $Z$ property is a proper superclass of the class of
systems satisfying the $L$ property. Systems satisfying the $L$ property also
satisfy the $V$ property, while the class of systems satisfying the $V$
property is a proper superclass of the class of systems satisfying the $S$
property. We present these results in Section 5, for general MSR systems and
PTSes.

####  4.3.1 Time-Bounded Versions of Verification Problems

Motivated by bounded model checking, we also investigate the time-bounded
versions of the above problems. Instead of infinite traces, in time-bounded
versions of the verification problems we consider traces that have exactly a
fixed number of occurrences of Tick rules. Time bounded version of
realizability and survivability were introduced in [16], while time bounded
version of reliability is novel here.

######  Definition 17 ($n$-Time Realizability / $n$-$Z$ property)

A timed MSR system $\mathcal{T}$ satisfies _$n$ -$Z$ property_ with respect to
the l.t.s., a critical configuration specification $\mathcal{CS}$, and an
initial configuration $\mathcal{S}_{0}$ if there _exists_ a compliant trace,
$\mathcal{P}$, from $\mathcal{S}_{0}$ that uses the l.t.s. such that global
time advances by exactly $n$ time units in $\mathcal{P}$. [16]

######  Definition 18 ($n$-Time Survivability / $n$-$S$ property)

A timed MSR system $\mathcal{T}$ satisfies _$n$ -time survivability property_
with respect to the l.t.s., a critical configuration specification
$\mathcal{CS}$ and an initial configuration $\mathcal{S}_{0}$ if it satisfies
$n$-$Z$ property and if _all_ traces with exactly $n$ instances of the $Tick$
rule starting with $\mathcal{S}_{0}$ and using the l.t.s. are compliant.

Analogously, we define the $n$-time bounded version of the reliability
problem. We consider all compliant traces covering _at most_ $n$ time units,
and extend them to compliant traces over _exactly_ $n$ time units.

######  Definition 19 ($n$-Time Reliability/ $n$-$L$ property)

A timed MSR system $\mathcal{T}$ satisfies _$n$ -time reliability_ with
respect to an initial configuration $\mathcal{S}_{0}$, a critical
configuration specification $\mathcal{CS}$, and the l.t.s. if it satisfies
$n$-$Z$ property with respect to $\mathcal{S}_{0}$, $\mathcal{CS}$, and the
l.t.s. and if for any configuration $\mathcal{S}$, reachable from
$\mathcal{S}_{0}$ on a compliant trace $\mathcal{P}$ that uses the l.t.s. and
has at most $n$ instances of the $Tick$ rule, there exists a trace
$\mathcal{P}^{\prime}$ that uses the l.t.s. such that:

  1. i)

$\mathcal{P}^{\prime}$ extends $\mathcal{P}$;

  2. ii)

$\mathcal{P}^{\prime}$ is compliant;

  3. iii)

$\mathcal{P}^{\prime}$ has exactly $n$ instances of the $Tick$ rule.

Since the notion of a point-of-no-return is defined to be inseparable from
infinite traces, it is not appropriate for the time-bounded version of the
verification problems. That is, time-bounded version of the recoverability
system problem makes little sense. Moreover, as we show in Section 5, for
PTSes problems of reliability and recoverability coincide. Hence, we do not
consider the bounded version of recoverability problem separately.

##  5 Relations Among Properties of Timed MSR

In this section we formally relate all the different properties defined in
Section 4.3.

In order to compare these properties we review the machinery introduced in our
previous work [20] called $\delta$-representations. This machinery is also
used in Section 6 to obtain complexity results for the corresponding
verification problems.

###  5.1 $\delta$-representations

Some of our results, for a given timed MSR $\mathcal{T}$, an initial
configuration $\mathcal{S}_{0}$ and a critical configuration specification
$\mathcal{CS}$, will mention the value $D_{max}$ which is an upper-bound on
the natural numbers appearing in $\mathcal{S}_{0}$, $\mathcal{T}$ and
$\mathcal{CS}$. The value of $D_{max}$ can be inferred syntactically by simply
inspecting the timestamps of $\mathcal{S}_{0}$, the $D$ values in timestamps
of rules (which are of the form $T+D$) and constraints in $\mathcal{T}$ and
$\mathcal{CS}$ (which are of the form $T_{1}>T_{2}\pm D$, $T_{1}=T_{2}\pm D$
and $T_{1}\geq T_{2}\pm D$). For example, the $D_{max}=1$ for the
specification in Figure 1.

For our results we assume a bound on the size of facts. For example, in our
specification in Figure 1, we can take the bound
$k=|x_{max}|+|y_{max}|+|e_{max}|+5$.

Notice, however, that we do not always impose an upper bound on the values of
timestamps. Also, we allow an unbounded number of fresh values to appear in a
trace.

###### Definition 20

Let $\mathcal{S}=\\{\,Q_{1}@t_{1},\,Q_{2}@t_{2},\ldots,\,Q_{n}@t_{n}\,\\}$ be
a configuration of a timed MSR $\mathcal{T}$ written in canonical way where
the sequence of timestamps $t_{1},\ldots,t_{n}$ is non-decreasing. (For the
case of equal timestamps, we sort the facts in alphabetical order, if
necessary.) The _$\delta$ -representation_ of $\mathcal{S}$ for a given
$D_{max}$ is

$\delta_{\mathcal{S},D_{max}}=[~{}Q_{1},\,\delta_{Q_{1},Q_{2}},\,Q_{2},\ldots,\,Q_{n-1},\,\delta_{Q_{n-1},Q_{n}},\,Q_{n}~{}]\
.$

Here, for a given natural number $D_{max}$, $\delta_{P,Q}$ is the _truncated
time difference_ of two timed facts $P@t_{1}$ and $Q@t_{2}$ with $t_{1}\leq
t_{2}$, defined as follows:

$\delta_{P,Q}=\left\\{\begin{array}[]{ccl}t_{2}-t_{1}&,&\ \textrm{ provided
}~{}t_{2}-t_{1}\leq D_{max}\\\ \infty&,&\ \textrm{ otherwise
}\end{array}\right.\ .$

For simplicity, when $D_{max}$ is clear from the context, we sometimes write
$\delta_{\mathcal{S}}$ instead of $\delta_{\mathcal{S},D_{max}}$.

In our previous work [19, 20], we showed that a $\delta$-representation is an
equivalence class on configurations. Namely, for a given $D_{max}$, we declare
$\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ equivalent, written
$\mathcal{S}_{1}\equiv_{D_{max}}\mathcal{S}_{2}$, if and only if their
$\delta$-representations are exactly the same, up to nonce renaming, i.e.,
$\mathcal{S}_{1}\sigma=\mathcal{S}_{2}$, where $\sigma$ is a bijection on the
set of nonce names.

This equivalence relation is well-defined with respect to time constrains,
i.e., configurations that have the same $\delta$-representation satisfy
exactly the same set of constraints. Here, when saying that configurations
satisfy the same constraint, we implicitly mean that time variables of the
constraint refer to the same facts in both configurations. Therefore, we can
say that a $\delta$-representation satisfies a constraint or does not.
Similarly, we say that a $\delta$-representation is critical iff it is the
$\delta$-representation of a critical configuration.

Also, the equivalence among configurations is well-defined with respect to
application of rules, i.e., application of rules on $\delta$-representations
is unambiguous. Therefore we can consider traces over
$\delta$-representations. For details on the concrete procedure of how to
apply a rule on a given $\delta$-representation see [20, Section 4.3].

We naturally extend the notion of a compliant trace and say that a trace over
$\delta$-representations is compliant iff it does not contain any critical
$\delta$-representation. Also, we say that a trace over
$\delta$-representations uses the l.t.s. if $Tick$ rule is applied to a
$\delta$-representation in that trace only when no instantaneous rule is
applicable.

Moreover, in [20, Theorem 4.1] we have shown that there is a bisimulation
between (compliant) traces over configurations and (compliant) traces over
their $\delta$-representations in the following sense:
$\mathcal{S}_{1}\longrightarrow_{*}\mathcal{S}_{2}$ iff
$\delta_{\mathcal{S}_{1}}\longrightarrow_{*}\delta_{\mathcal{S}_{2}}$ .

When considering concrete problems and corresponding bisimulations, the bound
$D_{max}$ is inferred from numerical values appearing in the problem
specification. This ensures that all configurations in traces are _future
bounded_ , i.e., do not contain facts $F@t_{F}$ such that
$\delta_{Time,F}=\infty$. This is important for faithful representation of
time advances. For more details see [20, Section 4.3].

For self-containment of the paper, in the proof of the following result from
[16] we present main proof ideas used in [20] and, moreover, we additionally
address the l.t.s.

###### Proposition 3

For any timed MSR $\mathcal{T}$, a critical configuration specification
$\mathcal{C}\mathcal{S}$ and an initial configuration $\mathcal{S}_{0}$ the
equivalence relation between configurations is well-defined with respect to
the rules of the system (including time advances), the l.t.s. and critical
configurations.
Namely, to any compliant trace starting from the given initial configuration
$\mathcal{S}_{0}$ corresponds a compliant trace over $\delta$-representations
starting from $\delta_{\mathcal{S}_{0}}$. In particular, a trace over
configurations uses the l.t.s. iff the corresponding trace over
$\delta$-representations uses the l.t.s. [16]

###### Proof

We firstly show that application of rules on $\delta$-representations is
independent of the choice of configuration from the same class. Assume
$\mathcal{S}_{1}$ and $\mathcal{S}_{2}$ are equivalent configurations, and
assume that $\mathcal{S}_{1}$ is transformed to $\mathcal{S}^{\prime}_{1}$ by
means of a rule $\alpha$, as shown in the diagram below. Recall that
equivalent configurations satisfy the same set of constraints. Hence, the rule
$\alpha$ is applicable to $\mathcal{S}_{2}$ and will transform
$\mathcal{S}_{2}$ into some $\mathcal{S}_{2}^{\prime}$:

$\begin{array}[]{cccc}\mathcal{S}_{1}&\to_{\alpha}&\mathcal{S}_{1}^{\prime}\\\\[4.0pt]
\biginterleave&&\\\\[4.0pt] \mathcal{S}_{2}&\to_{\alpha}&\
\mathcal{S}_{2}^{\prime}\end{array}$

It remains to show that $\mathcal{S}_{1}^{\prime}$ is equivalent to
$\mathcal{S}_{2}^{\prime}$. We consider the two types of rules for $\alpha$,
namely, time advances and instantaneous rules.

Let the time advance transform ${\mathcal{S}_{1}}$ into
${\mathcal{S}_{1}}^{\prime}$, and $\mathcal{S}_{2}$ to
$\mathcal{S}_{2}^{\prime}$. Since only the timestamp $T$ denoting the global
time in $Time@T$ is increased by 1, and the rest of the configuration remains
unchanged, only truncated time differences involving $Time$ change in the
resulting $\delta$-representations. Because of the equivalence
$S_{1}\equiv_{D_{max}}S_{2}$ , for a fact $P@T_{P}^{1}$ in $\mathcal{S}_{1}$
with $T_{P}^{1}\leq T^{1}$, $Time@T^{1}$ and $\delta_{P,Time}=t$, we have
$P@T_{P}^{2}$ with ${T}_{P}^{2}\leq{T^{2}}$, $Time@{T^{2}}$ and
$\delta_{P,Time}=t$ in $\mathcal{S}_{2}$ as well. Therefore, we have

$\delta_{P,Time}=\left\\{\begin{array}[]{ccl}t+1&,&\ \textrm{ provided }\
t+1\leq D_{max}\\\ \infty&,&\ \textrm{ otherwise }\end{array}\right.$

both in $\mathcal{S}_{1}^{\prime}$ and $\mathcal{S}_{2}^{\prime}$. On the
other hand, for any future fact $Q@T^{Q}$ with $\delta_{Time,Q}=t$ in
$\mathcal{S}_{1}$ and in $\mathcal{S}_{2}$, we get $\delta_{Time,Q}=t-1$ in
both $\mathcal{S}_{1}^{\prime}$ and $\mathcal{S}_{2}^{\prime}$. Therefore,
${\mathcal{S}_{1}}^{\prime}$ and $\mathcal{S}_{2}^{\prime}$ are equivalent.
Recall that since all configurations in the trace are future bounded,
$t<\infty$, so $t-1$ is well-defined.

The reasoning for the application of instantaneous rules is similar. Each
created fact in $\mathcal{S}_{1}^{\prime}$ and $\mathcal{S}_{2}^{\prime}$ is
of the form $P@(T^{1}+d)$ and $P@(T^{2}+d)$ , where $T^{1}$ and $T^{2}$
represent global time in $\mathcal{S}_{1}$ and $\mathcal{S}_{2}$,
respectively. Therefore each created fact has the same difference, $d$, to the
global time in the corresponding configuration. This implies that the created
facts have the same truncated time differences to the remaining (unchanged)
facts. Namely, $\delta_{Time,P}=d<\infty$, hence for $P@t_{P}$, $R@t_{R}$ and
$Time@t$ with $t\leq t_{R}\leq t_{P}$,

$\delta_{R,P}=\delta_{Time,P}-\delta_{Time,R}\ .$

Notice here that $\delta_{Time,R}<\infty$ because all configurations are
future bounded, so the above difference is well-defined (finite). Similarly,
when $t\leq t_{P}\leq t_{R}$,

$\delta_{P,R}=\delta_{Time,R}-\delta_{Time,P}\ .$

Hence ${\mathcal{S}_{1}}^{\prime}$ and $\mathcal{S}_{2}^{\prime}$ are
equivalent. Therefore, application of rules on $\delta$-representations
defined through corresponding configurations is well-defined, i.e., the
abstraction of configurations to $\delta$-representations w.r.t. application
of rules is complete.

The abstraction is also sound. Namely, from a compliant trace over
$\delta$-representations, we can extract a concrete compliant trace over
configurations. Although any given $\delta$-representation corresponds to an
infinite number of configurations, for a given initial configuration
$\mathcal{S}_{0}$, we have the initial $\delta$-representation
$\delta_{0}=\delta_{\mathcal{S}_{0}}$. The existence of a trace over
configurations corresponding to the given (possibly infinite) trace over
$\delta$-representations is then easily proven by induction.

Since equivalent configurations satisfy the same set of constraints,
$\mathcal{S}_{1}$ is a critical configuration if and only if $\mathcal{S}_{2}$
is a critical configuration, i.e., if and only if $\delta_{\mathcal{S}_{1}}$
is critical. By induction on the length of the (sub)trace, it follows that,
given a timed MSR and a critical configuration specification
$\mathcal{C}\mathcal{S}$, any (possibly infinite) trace over configurations is
compliant if and only if the corresponding trace over $\delta$-representations
is compliant.

Notice that, using the l.t.s. in a trace $\mathcal{P}$, $Tick$ rule is applied
to some $\mathcal{S}_{i}$ in $\mathcal{P}$ if and only if no instantaneous
rule can be applied to $\mathcal{S}_{i}$. Since $\mathcal{S}_{i}$ and its
$\delta$-representation, $\delta_{\mathcal{S}_{i}}$, satisfy the same set of
constraints, it follows that $Tick$ rule is applied to
$\delta_{\mathcal{S}_{i}}$ iff $Tick$ rule is applied to $\mathcal{S}_{i}$.
Hence, a trace over configurations uses the l.t.s. iff the corresponding trace
over $\delta$-representations uses the l.t.s. ∎

Following the above result, in the case of balanced timed MSRs, we can work on
traces constructed using $\delta$-representations. Moreover, the following
lemma [16] establishes a bound on the number of different
$\delta$-representations.

###### Lemma 1

[16] Let $\mathcal{T}$ be a timed MSR constructed over a finite alphabet
$\Sigma$ with $J$ predicate symbols and $E$ constant and function symbols. Let
$m$ be the number of facts in the initial configuration $\mathcal{S}_{0}$, $k$
an upper-bound on the size of the facts, $\mathcal{CS}$ a critical
configuration specification and $D_{max}$ an upper-bound on the numerical
values of $\mathcal{S}_{0},\mathcal{T}$, and $\mathcal{CS}$.
The number of different $\delta$-representations, denoted by
$L_{\Sigma}(m,k,D_{max})$, is such that

$L_{\Sigma}(m,k,D_{max})\leq(D_{max}+2)^{(m-1)}J^{m}(E+2mk)^{mk}.$

###  5.2 Time-Bounded v.s. Unbounded Verification Problems for Timed MSR

It is obvious, by definition, that the $Z$ property implies the $n$-$Z$
property. We now show that for a sufficiently large $n$, the converse
implication also holds, i.e., the $n$-$Z$ property implies the $Z$ property.
The same implications hold for the other properties.

######  Proposition 4 (Realizability v.s. $n$-Time Realizability)

Let $\mathcal{T}$ be a timed MSR that uses the l.t.s., $\mathcal{S}_{0}$ an
initial configuration and $\mathcal{CS}$ a critical configuration
specification. Then, $\mathcal{T}$ satisfies the $Z$ property iff $\forall n$,
$\mathcal{T}$ satisfies the $n$-$Z$ property.

Moreover, there exists $M$ such that if $\mathcal{T}$ satisfies the $M$-$Z$
property, then $\mathcal{T}$ satisfies the $Z$ property. (In particular, the
above claim holds for $M=L_{\Sigma}(m,k,D_{max})$.

###### Proof

Per definition, the $Z$ property implies the $n$-$Z$ property for any $n$.

We now prove the second statement. The first statement then easily follows.

From Proposition 3 it follows that for the above problems we can consider
traces constructed over $\delta$-representations. As per Lemma 1, the number
of different $\delta$-representations is bounded by
$l=L_{\Sigma}(m,k,D_{max})$, where $m$ is the number of facts in
$\mathcal{S}_{0}$, $k$ is an upper-bound on the size of facts and $D_{max}$ is
an upper-bound on the numeric values of $\mathcal{S}_{0},\mathcal{T}$ and
$\mathcal{CS}$.

Assume $\mathcal{T}$ satisfies the $M$-$Z$ property, where
$M=L_{\Sigma}(m,k,D_{max})$. Then, there is a compliant trace $\mathcal{P}$
from $\delta_{\mathcal{S}_{0}}$ that uses the l.t.s. and contains exactly $M$
$Tick$ rules. Trace $\mathcal{P}$ contains a series of instantaneous rules
separated by $Tick$ rules. That is, $\mathcal{P}$ contains $M+1$ blocks of
$\delta$-representations, formed at each of the $M$ instances of $Tick$ rules
in $\mathcal{P}$. Since there are at most $M$ different
$\delta$-representations in $\mathcal{T}$, at least one
$\delta$-representation $\delta_{1}$ appears in two blocks. Therefore, a
subtrace between the two appearances of $\delta_{1}$ contains a $Tick$ rule,
$\delta_{1}\longrightarrow\cdots\longrightarrow_{Tick}\cdots\longrightarrow\delta_{1}\,$,
and represents a loop in $\mathcal{P}$.

The above subtrace is compliant, uses the l.t.s. and contains a $Tick$ rule.
Repeating this loop indefinitely results in a compliant infinite time trace
that uses the l.t.s. The resulting trace shows that $\mathcal{T}$ satisfies
the $Z$ property. ∎

######  Proposition 5 (Survivability v.s. $n$-Time Survivability)

Let $\mathcal{T}$ be a timed MSR that uses the l.t.s., $\mathcal{S}_{0}$ an
initial configuration and $\mathcal{CS}$ a critical configuration
specification. Then, $\mathcal{T}$ satisfies the $S$ property iff $\forall n$,
$\mathcal{T}$ satisfies the $n$-$S$ property.
Moreover, there exists $M$ such that if $\mathcal{T}$ satisfies the $M$-$S$
property, then $\mathcal{T}$ satisfies the $S$ property.

###### Proof

Assume that $\mathcal{T}$ satisfies the $M$-$S$ property, where
$M=L_{\Sigma}(m,k,D_{max})$. Hence, all traces with $M$ ticks are compliant.
Assume $\mathcal{T}$ is does not satisfy the $S$ property. Then there is an
infinite time trace $\mathcal{P}$ from $\mathcal{S}_{0}$ that uses the l.t.s.
which is not compliant, i.e., there is a critical configuration
$\mathcal{S}_{1}$ in $\mathcal{P}$. Because $\mathcal{T}$ satisfies the
$M$-$S$ property, there are more then $M$ ticks in the subtrace
$\mathcal{S}_{0}\longrightarrow\cdots\longrightarrow\mathcal{S}_{1}$ of
$\mathcal{P}$.

Since there are more than $M$ rules (and $\delta$-representations) in the
above subtrace $\mathcal{P}^{\prime}$, some $\delta$-representation appears at
least twice in $\mathcal{P}^{\prime}$, i.e., there is a loop in
$\mathcal{P}^{\prime}$. By removing all loops in $\mathcal{P}^{\prime}$ we
obtain a trace $\mathcal{P}^{\prime\prime}$ from $\mathcal{S}_{0}$ to
$\mathcal{S}_{1}$ that uses the l.t.s. and contains at most $M$ rules.
Consequently, there are at most $M$ ticks in $\mathcal{P}^{\prime\prime}$.

The trace $\mathcal{P}^{\prime\prime}$ is not a compliant since it contains
$\mathcal{S}_{1}$. This is in contradiction with the $M$-$S$ property of
$\mathcal{T}$.

Per definitions, the $S$ property implies the $n$-$S$ property for any $n$.
The first statement is then a simple consequence of the second statement and
definitions. ∎

######  Proposition 6 (Reliability v.s. $n$-Time Reliability)

Let $\mathcal{T}$ be a timed MSR that uses the l.t.s., $\mathcal{S}_{0}$ an
initial configuration and $\mathcal{CS}$ a critical configuration
specification. Then, $\mathcal{T}$ satisfies the $L$ property iff $\forall n$,
$\mathcal{T}$ satisfies the $n$-$L$ property.
Moreover, there exists $M$ such that if $\mathcal{T}$ satisfies the $M$-$L$
property, then $\mathcal{T}$ satisfies the $L$ property.

###### Proof

As in Proposition 4, we consider traces constructed over
$\delta$-representations. We show the second statement. The first statement
follows from the second statement and definitions.

Let $M=L_{\Sigma}(m,k,D_{max})$. Assume $\mathcal{T}$ satisfies the $M$-$L$
property. Then $\mathcal{T}$ satisfies the $M$-$L$ property and, by the proof
of Proposition 5.2, it satisfies the $L$ property. Namely, a compliant trace
$P$ with $M$ $Tick$ rules that uses the l.t.s. is its own compliant extension,
showing the $M$-$L$ property.

We still need to show that an arbitrary compliant trace from
$\delta_{\mathcal{S}_{0}}$ that uses the l.t.s., $\mathcal{P}$, can be
extended to a compliant infinite time trace that uses thel.t.s. Let $m$ be the
number of $Tick$ rules in $\mathcal{P}$.

Since $\mathcal{T}$ satisfies the $M$-$L$ property, $\mathcal{P}$ can be
extended to a compliant trace $\mathcal{P}^{\prime}$ that uses the l.t.s. and
contains exactly $M$ $Tick$ rules. As in the proof of Proposition 4, we can
conclude that there is a $\delta$-representation $\delta^{\prime}$ in
$\mathcal{P}^{\prime}$ that appears at least twice with a $Tick$ rule between
the two appearances of $\delta^{\prime}$ in $\mathcal{P}^{\prime}$. Repeating
the subtrace of $\mathcal{P}^{\prime}$ between two appearances of
$\delta^{\prime}$ indefinitely, creates an infinite time compliant trace from
$\delta_{\mathcal{S}_{0}}$ that uses the l.t.s. and shows the $L$ property of
$\mathcal{T}$. ∎

###  5.3 Relations Among Different Properties of Timed MSR and PTS

In this Section we formally relate different properties defined over infinite
traces. In general, we can distinguish all these properties for timed MSR, but
only some for PTSes, as stated below.

###### Proposition 7

Let $\mathcal{T}$ be a timed MSR system that uses the l.t.s.,
$\mathcal{S}_{0}$ an initial configuration and $\mathcal{CS}$ a critical
configuration specification.

If $\mathcal{T}$ satisfies the $L$ property, then $\mathcal{T}$ satisfies the
$V$ property.

If $\mathcal{T}$ satisfies the $V$ property, then $\mathcal{T}$ does not
necessarily satisfy the $L$ property.

###### Proof

Let $\mathcal{T}$ be a timed MSR system that satisfies the $L$ property.
Assume $\mathcal{T}$ does not satisfy the $V$ property. Then, since
$\mathcal{T}$ satisfies the $Z$ property, there is a compliant trace from
$\mathcal{S}_{0}$ to some point-of-no-return $\mathcal{S}_{P}$ that uses the
l.t.s. Since $\mathcal{T}$ satisfies the $L$ property, there is a compliant
infinite time trace from $\mathcal{S}_{P}$ that uses the l.t.s. As
$\mathcal{S}_{P}$ is a point-of-no-return, this contradicts the notion of
point-of-no-return.
We give an example of a timed MSR system, $\mathcal{T}$, that satisfies the
$V$ property, but does not that satisfy the $L$ property.
Let $\mathcal{S}_{0}^{\prime}=\\{Time@0,C@1\\}$,
$\mathcal{CS}^{\prime}=\emptyset$, and let $\mathcal{T}^{\prime}$ contain only
the following instantaneous rules:

$\displaystyle Time@T,\,{\color[rgb]{0.65,0,0}C@T^{\prime}}\mid T^{\prime}\leq
T\ \longrightarrow\ \ Time@T,\,{\color[rgb]{0,0.44,0.57}\,D@T}$ (5a)
$\displaystyle Time@T,\,{\color[rgb]{0.65,0,0}C@T^{\prime}}\mid T^{\prime}\leq
T\ \longrightarrow\ \ Time@T,\,{\color[rgb]{0,0.44,0.57}\,A@T}$ (5b)
$\displaystyle Time@T,\,{\color[rgb]{0.65,0,0}A@T^{\prime}}\ \
\longrightarrow\ \ Time@T,\,{\color[rgb]{0,0.44,0.57}\,B@T}$ (5c)
$\displaystyle Time@T,\,{\color[rgb]{0.65,0,0}B@T^{\prime}}\ \
\longrightarrow\ \ Time@T,\,{\color[rgb]{0,0.44,0.57}\,A@T}$ (5d)

The system $\mathcal{T}^{\prime}$ satisfies the $Z$ property since there is a
compliant infinite time trace from $\mathcal{S}_{0}^{\prime}$ that uses the
l.t.s.:

$\small\begin{array}[]{ll}Time@0,\,{C@1}\ \longrightarrow_{Tick}\
Time@1,\,{C@1}\ \longrightarrow_{(\ref{eq:ex03-0})}\ Time@1,\,{D@1}\
\longrightarrow_{Tick}\\\ \quad Time@2,\,{D@1}\ \longrightarrow_{Tick}\
Time@3,\,{D@1}\ \longrightarrow_{Tick}\ Time@4,\,{D@2}\
\longrightarrow_{Tick}\dots\end{array}$ (6)

There is only one other infinite trace form $\mathcal{S}_{0}$ that uses the
l.t.s.:

$\small\begin{array}[]{ll}Time@0,\,{C@1}\ \longrightarrow_{Tick}\
Time@1,\,{C@1}\ \longrightarrow_{(\ref{eq:ex03-1})}\ Time@1,\,{A@1}\
\longrightarrow_{(\ref{eq:ex03-2})}\\\ \quad Time@1,\,{B@1}\
\longrightarrow_{(\ref{eq:ex03-3})}\ Time@1,\,{A@1}\
\longrightarrow_{(\ref{eq:ex03-2})}\ Time@1,\,{B@2}\
\longrightarrow_{(\ref{eq:ex03-3})}\dots\end{array}$ (7)

Its subtrace obtained from $\mathcal{S}_{0}$ by applying the $Tick$ rule
followed by the rule $({\ref{eq:ex03-1}})$ reaches the configuration
$Time@1,A@1$. This subtrace is compliant but it cannot be extended to a
compliant infinite time trace that uses the l.t.s. Hence,
$\mathcal{T}^{\prime}$ does not satisfy the $L$ property.
However, $\mathcal{T}^{\prime}$ trivially satisfies the $V$ property since
there are no critical configurations and, hence, no points-of-no-return. ∎

Notice that the properties of timed MSR defined in Section 4.3 involve
infinite time traces that use the l.t.s. Recall that for any given PTS
$\mathcal{T}$ and any configuration $\mathcal{S}$, there exists an infinite
time trace of $\mathcal{T}$ that starts with $\mathcal{S}$ and uses the l.t.s.

Although $V$ and $L$ are different properties of timed MSR systems in general,
it turns out that for the class of PTSes these properties coincide.

###### Proposition 8

Let $\mathcal{T}$ be a PTS that uses the l.t.s., $\mathcal{S}_{0}$ an initial
configuration, and $\mathcal{CS}$ a critical configuration specification.

System $\mathcal{T}$ satisfies the $L$ property iff $\mathcal{T}$ satisfies
the $V$ property.

###### Proof

Since a PTS is a timed MSR system, it follows from Proposition 7 that a PTS,
which satisfies the $L$ property, also satisfies the $V$ property.
Assume that a PTS $\mathcal{T}$ does not satisfy the $L$ property. If
$\mathcal{S}_{0}$ is critical, then $\mathcal{T}$ does not satisfy the $Z$
property and consequently, does not satisfy the $V$ property. If
$\mathcal{S}_{0}$ is not critical, there is a compliant trace from
$\mathcal{S}_{0}$ to some configuration $\mathcal{S}_{1}$ that uses the l.t.s.
which cannot be extended to a compliant infinite time trace that uses the
l.t.s.

Then, $\mathcal{S}_{1}$ is a point-of-no-return. Namely, if $P$ is an infinite
trace from $\mathcal{S}_{1}$ that uses the l.t.s., by Proposition 2, $P$ is an
infinite time trace that uses the l.t.s. Then, $P$ is not compliant. Since the
point-of-no-return $\mathcal{S}_{1}$ is reachable from $\mathcal{S}_{0}$ on a
compliant trace using the l.t.s., $\mathcal{T}$ does not satisfy the $V$
property. ∎

We show that the remaining properties are different even for PTSes.
Furthermore, we show relations among the properties for PTSes and for timed
MSR systems in general. We first show that $L$ and $S$ are different
properties of PTSes, and, consequently, different properties of timed MSR
systems.

###### Proposition 9

Let $\mathcal{T}$ be a PTS that uses the l.t.s., $\mathcal{S}_{0}$ an initial
configuration and $\mathcal{CS}$ a critical configuration specification.

If $\mathcal{T}$ satisfies the $S$ property, then $\mathcal{T}$ satisfies the
$L$ property.

If $\mathcal{T}$ satisfies the $L$ property, it may not satisfy the $S$
property.

###### Proof

Assume that $\mathcal{T}$ satisfies the $S$ property, but does not satisfy the
$L$ property. Then, since $\mathcal{T}$ satisfies the $Z$ property, there
exists a compliant trace, $\mathcal{P}$, from $\mathcal{S}_{0}$ to some
configuration $\mathcal{S}_{1}$ that cannot be extended to a compliant
infinite time trace that uses the l.t.s. Let $\mathcal{P}^{\prime}$ be an
infinite time trace which is an extension of $\mathcal{P}$ that uses the
l.t.s. Such a trace $\mathcal{P}^{\prime}$ exists due to Proposition 2, but it
is not compliant.
Since $\mathcal{T}$ satisfies the $S$ property, all infinite time traces from
$\mathcal{S}_{0}$ that use the l.t.s. are compliant, including
$\mathcal{P}^{\prime}$. Contradiction.
The following example of a PTS satisfies the $L$ property, but does not
satisfy the $S$ property.

Let $\mathcal{S}_{0}=\\{Time@0,A@0,B@0\\}$,
$\mathcal{CS}=\\{~{}\langle~{}\\{B@T,D@T^{\prime}\\},\emptyset~{}\rangle\\}$
and let PTS $\mathcal{T}$ contain only the following instantaneous rules:

$\displaystyle
Time@T,\,{\color[rgb]{0.65,0,0}A@T^{\prime}},\,B@T^{\prime\prime}\mid\\{T^{\prime}\leq
T,T^{\prime\prime}\leq T\\}$
$\displaystyle\longrightarrow\,Time@T,\,B@T^{\prime\prime},{\color[rgb]{0,0.44,0.57}\,C@(T+1)}$
(8a) $\displaystyle
Time@T,\,{\color[rgb]{0.65,0,0}A@T^{\prime}},\,B@T^{\prime\prime}\mid\\{T^{\prime}\leq
T\\}$
$\displaystyle\longrightarrow\,Time@T,\,B@T^{\prime\prime},{\color[rgb]{0,0.44,0.57}\,D@(T+1)}$
(8b) $\displaystyle
Time@T,\,{\color[rgb]{0.65,0,0}B@T^{\prime}},\,{\color[rgb]{0.65,0,0}C@T^{\prime\prime}}\mid\\{T^{\prime}\leq
T,T^{\prime\prime}\leq T\\}$
$\displaystyle\longrightarrow\,Time@T,\,{\color[rgb]{0,0.44,0.57}A@T},{\color[rgb]{0,0.44,0.57}\,B@(T+1)}$
(8c)

The following trace from $\mathcal{S}_{0}$ uses the l.t.s. and is not
compliant:

$Time@0,A@0,B@0\ \longrightarrow_{(\ref{eq:ex-2})}\ Time@0,B@0,D@1\ .$
Hence, $\mathcal{T}$ does not satisfy the $S$ property.

To show that $\mathcal{T}$ satisfies the $L$ property, we first show that
$\mathcal{T}$ satisfies the $Z$ property. The following trace from
$\mathcal{S}_{0}$ is a compliant infinite time trace that uses the l.t.s.:

${\small\begin{array}[]{l}Time@0,A@0,B@0\ \longrightarrow_{(\ref{eq:ex-1})}\ \
Time@0,B<EMAIL_ADDRESS>\ \ \longrightarrow_{Tick}\ \
Time@1,B@0,C@1\ \longrightarrow_{(\ref{eq:ex-3})}\ \ Time@1,A@1,B@2\
\longrightarrow_{Tick}\\\\[2.0pt] \ \ \ \ \longrightarrow_{Tick}\ \
Time@2,A@1,B@2\ \longrightarrow_{(\ref{eq:ex-1})}\ \ Time@2,B@2,C@3\
\longrightarrow_{Tick}\dots\end{array}}$

Next, assume $\mathcal{P}$ is a compliant trace from $\mathcal{S}_{0}$ to some
$\mathcal{S}_{1}$ that uses the l.t.s. Then $\mathcal{P}$ does not contain
rule (8b), which always results in a critical configuration. Hence, only rules
(8a), (8c) and $Tick$ are used in $\mathcal{P}$, so $\mathcal{S}_{1}$ is
either $\\{\,Time@t,\,{A@t^{\prime}},\,B@t^{\prime\prime}\,\\}$ or
$\\{\,Time@t,\,B@t^{\prime},\,{C@t^{\prime\prime}}\,\\}.$ Using only the rules
(8a), (8c) and $Tick$, the trace $\mathcal{P}$ can be extended to a compliant
infinite time trace that use the l.t.s. Hence, $\mathcal{T}$ satisfies the $L$
property. ∎

However, the above does not hold for general MSR systems, i.e., MSR systems
that satisfy the $S$ property do not necessarily satisfy the $L$ property.

###### Proposition 10

Let $\mathcal{T}$ be a timed MSR that uses the l.t.s., $\mathcal{S}_{0}$ an
initial configuration and $\mathcal{CS}$ a critical configuration
specification.

If $\mathcal{T}$ satisfies the $S$ property, it may not satisfy the $L$
property.

If $\mathcal{T}$ satisfies the $L$ property, it may not satisfy the $S$
property.

###### Proof

Let $\mathcal{T}^{\prime}$, $\mathcal{S}_{0}^{\prime}$ and
$\mathcal{CS}^{\prime}$ be as specified in the proof of Proposition 7. Recall
that $\mathcal{T}^{\prime}$ does not satisfy the $L$ property.

The system $\mathcal{T}^{\prime}$ satisfies the $S$ property. Namely, there
are only two infinite traces from $\mathcal{S}_{0}^{\prime}$ that use the
l.t.s., traces (6) and (7) specified in the proof of Proposition 7. However,
trace (7) is not an infinite time trace, so there is only one infinite time
trace from $\mathcal{S}_{0}^{\prime}$ that uses the l.t.s., trace (6).
Therefore, since trace (6) is compliant, $\mathcal{T}^{\prime}$ satisfies the
$S$ property.

By Proposition 9 there is a PTS, and therefore an MSR, that satisfies the $L$
property but does not satisfy the $S$ property. ∎

Next, we show how the $V$ property relates to the $Z$ property.

###### Proposition 11

Let $\mathcal{T}$ be a timed MSR that uses the l.t.s., $\mathcal{S}_{0}$ an
initial configuration, and $\mathcal{CS}$ a critical configuration
specification.

If $\mathcal{T}$ satisfies the $V$ property, then $\mathcal{T}$ satisfies the
$Z$ property.

A system $\mathcal{T}$ that satisfies the $Z$ property may not satisfy the $V$
property.

###### Proof

Assume $\mathcal{T}$ satisfies the $V$ property. Then, $\mathcal{T}$ satisfies
the $Z$ property by definition.

We prove the other statement by providing an example of a PTS that satisfies
the $Z$ property, but does not satisfy the $V$ property. Let
$\mathcal{S}_{0}^{\prime\prime}=\\{Time@0,A@0\\}$,
$\mathcal{CS}^{\prime\prime}=\\{~{}\langle\\{D@T\\},\emptyset~{}\rangle\\}$
and let PTS $\mathcal{T}^{\prime\prime}$ contain only the following
instantaneous rules:

$\displaystyle Time@T,\,{\color[rgb]{0.65,0,0}A@T^{\prime}}\ \mid\
\,\\{T^{\prime}\leq T\\}\ \longrightarrow\ \
Time@T,\,{\color[rgb]{0,0.44,0.57}\,B@(T+1)}$ (9a) $\displaystyle
Time@T,\,{\color[rgb]{0.65,0,0}A@T^{\prime}}\ \mid\ \,\\{T^{\prime}\leq T\\}\
\longrightarrow\ \ Time@T,\,{\color[rgb]{0,0.44,0.57}\,C@(T+1)}$ (9b)
$\displaystyle Time@T,\,{\color[rgb]{0.65,0,0}B@T^{\prime}}\ \mid\
\,\\{T^{\prime}\leq T\\}\ \longrightarrow\ \
Time@T,\,{\color[rgb]{0,0.44,0.57}\,A@(T+1)}$ (9c) $\displaystyle
Time@T,\,{\color[rgb]{0.65,0,0}C@T^{\prime}}\ \mid\ \,\\{T^{\prime}\leq T\\}\
\longrightarrow\ \ Time@T,\,{\color[rgb]{0,0.44,0.57}\,D@(T+1)}$ (9d)

The following trace, which uses the l.t.s., shows the $Z$ property of
$\mathcal{T}^{\prime\prime}$:

$\small\begin{array}[]{l}Time@0,\,{A@0}\,\longrightarrow_{(\ref{eq:ex1-3})}\,Time@0,{\,B@1}\
\longrightarrow_{Tick}\,Time@1,{\,B@1}\ \longrightarrow_{(\ref{eq:ex1-4})}\\\
\ \ Time@1,{\,A@2}\ \longrightarrow_{Tick}\,Time@2,{\,A@2}\
\longrightarrow_{(\ref{eq:ex1-3})}\,Time@2,{\,B@3}\
\longrightarrow_{Tick}\dots\end{array}$
The configuration $\widetilde{\mathcal{S}}=\\{Time@0,C@1\\}$ is reachable from
$\mathcal{S}_{0}^{\prime\prime}$ by a compliant trace that uses the l.t.s.:
$Time@0,\,{\color[rgb]{0.65,0,0}{A@0}}\ \longrightarrow_{(\ref{eq:ex1-1})}\
Time<EMAIL_ADDRESS>$\widetilde{\mathcal{S}}$ is a
point-of-no-return as rule (9d) is the only instantaneous rule that can be
applied after a $Tick$, so all infinite traces from $\widetilde{\mathcal{S}}$
that use the l.t.s. contain the critical configuration $\\{Time@1,D@2\\}$.

Since $\widetilde{\mathcal{S}}$ is a point-of-no-return,
$\mathcal{T}^{\prime\prime}$ does not satisfy the $V$ property. ∎

###### Remark 3

Notice that requiring the $Z$ property in the definition of the $L$ property
(Definition 16) is redundant in the sense that the $Z$ property would follow
from the $L$ property anyway.

Namely, the non-critical initial configuration $\mathcal{S}_{0}$ is trivially
reachable from $\mathcal{S}_{0}$ on a compliant trace that uses the l.t.s.
Then, the $L$ property of $\mathcal{T}$ would imply the existence of a
compliant infinite time trace from $\mathcal{S}_{0}$ that uses the l.t.s.
Hence, $\mathcal{T}$ would satisfy the $Z$ property.

Similarly, the $Z$ property would follow from the $V$ property, even if it was
not required by definition (Definition 15), provided that the initial
configuration was not critical. Namely, the set of compliant traces from a
critical configuration is empty, so in the case of a critical initial
configuration, the system would not satisfy the $Z$ property but the $V$
property would hold because of universal quantification over the empty set.

Assuming that $\mathcal{S}_{0}$ is not critical, $\mathcal{S}_{0}$ is
trivially reachable from $\mathcal{S}_{0}$ on a compliant trace that uses the
l.t.s. Then, the $V$ property of $\mathcal{T}$ implies that $\mathcal{S}_{0}$
is not a point-of-no-return. Then, as per definition of a point-of-no-return,
there is a compliant infinite trace, $\mathcal{P}$, from $\mathcal{S}_{0}$
that uses the l.t.s. As per Proposition 2, $\mathcal{P}$ is a compliant
infinite time trace from $\mathcal{S}_{0}$ that uses the l.t.s. Hence,
$\mathcal{T}$ satisfies the $Z$ property.

Therefore, it was not necessary to include the condition of the $Z$ property
in Definitions 15 and 16. We do so to keep these notions intuitive in the
sense that these properties are more restrictive that the $Z$ property.

Using transitivity of the subset relation, we can infer relations among all
our properties for both PTSes and timed MSR systems in general. We summarize
our results in the following corollaries.

###### Corollary 1

Let ${}^{~{}}_{reali}Z_{ability}^{~{}MSR}$ ,
${}^{~{}}_{re}L_{iability}^{~{}MSR}$ , ${}^{~{}}_{reco}V_{erability}^{~{}MSR}$
and $S_{urvivability}^{~{}MSR}$ be the classes of timed MSR systems satisfying
the $Z$ , $L$ , $V$ and $S$ properties, respectively, w.r.t. the l.t.s. Then,
the following relations hold:

$S_{urvivability}^{~{}MSR}\ {\neq}^{~{}}_{re}L_{iability}^{~{}MSR}\ \subset\
^{~{}}_{reco}V_{erability}^{~{}MSR}\ \subset\
^{~{}}_{reali}Z_{ability}^{~{}MSR}$

###### Proof

The statement follows directly from the Propositions 10, 7, and 11. ∎

###### Corollary 2

Let ${}^{~{}}_{reali}Z_{ability}^{~{}PTS}$ ,
${}^{~{}}_{re}L_{iability}^{~{}PTS}$ , ${}^{~{}}_{reco}V_{erability}^{~{}PTS}$
and $S_{urvivability}^{~{}PTS}$ be the classes of PTSes satisfying the $Z$ ,
$L$ , $V$ and $S$ properties, respectively, w.r.t. the l.t.s. Then the
following proper subset relations hold:

$S_{urvivability}^{~{}PTS}\ \subset\ ^{~{}}_{re}L_{iability}^{~{}PTS}\ =\
^{~{}}_{reco}V_{erability}^{~{}PTS}\ \subset\
^{~{}}_{reali}Z_{ability}^{~{}PTS}$

###### Proof

The statement follows directly from the Propositions 9 and 8, and the proof of
proposition 11. ∎

###### Corollary 3

Let ${}^{~{}}_{reali}nZ_{ability}^{~{}PTS}$ ,
${}^{~{}}_{re}nL_{iability}^{~{}PTS}$ and $nS_{urvivability}^{~{}PTS}$ be the
classes of PTSes satisfying the $n$-$Z$ , $n$-$L$ and $n$-$S$ properties,
respectively, w.r.t. the l.t.s. Then, the following proper subset relations
hold:

$n\mathcal{S}_{urvivability}^{~{}PTS}\ \subset\
^{~{}}_{re}nL_{iability}^{~{}PTS}\ \subset\
^{~{}}_{reali}nZ_{ability}^{~{}PTS}\ .$

###### Proof

Let a PTS $\mathcal{T}$ satisfy the $n$-$S$ property. We check that
$\mathcal{T}$ satisfies the $n$-$L$ property. Let $\mathcal{S}$ be a
configuration that is reachable from $\mathcal{S}_{0}$ on a compliant trace
$\mathcal{P}$ that uses the l.t.s. and has at most $n$ instances of the $Tick$
rule. Since $\mathcal{T}$ is a PTS, only a bounded number of instantaneous
rules can be applied before a $Tick$ rule appears in a trace that uses the
l.t.s. (Proposition 1). Hence, the trace $\mathcal{P}$ can be extended to a
compliant trace $\mathcal{P}^{\prime}$ that contains exactly $n$ instances of
the $Tick$ rule and uses the l.t.s. Since $\mathcal{T}$ satisfies the $n$-$S$
property, $\mathcal{P}^{\prime}$ is compliant. Consequently, $\mathcal{T}$
satisfies the $n$-$L$ property.

Now, let $\mathcal{T}$ satisfy the $n$-$L$ property. Then, the trivial trace
of length 1 from $\mathcal{S}_{0}$ (containing only $\mathcal{S}_{0}$) can be
extended to a compliant trace $\mathcal{P}^{\prime}$ that contains exactly $n$
instances of the $Tick$ rule and uses the l.t.s. Hence, $\mathcal{T}$
satisfies the $n$-$Z$ property.

To show that the inclusions are proper, we give examples of PTSes that satisfy
one, but not the other property. The PTS given in the proof of Proposition 11
is an example of a system that satisfies the $n$-$Z$ property, $\forall n>0$,
which does not satisfy even the $1$-$S$ property. Similarly, the PTS given in
the proof of Proposition 9 satisfies the $n$-$L$ property, $\forall n>0$, but
it does not even satisfy the $1$-$S$ property. ∎

##  6 Complexity Results for PTSes

In this section we investigate the complexity of the verification problems
defined in Section 4.3 for progressing timed systems. Recall that the $L$ and
$V$ properties for PTS coincide.

###  6.1 PSPACE-Completeness of Verification Problems for PTSes

We again point out that in our previous work [14, 20, 18, 32] we only dealt
with finite traces. The additional challenge in addressing the complexity of
the $Z$ and $S$ problems in [16] and the new verification problems $L$ and $V$
in this paper, is to deal with infinite traces.

Assume throughout this section the following:

  * •

$\Sigma$ – A finite alphabet with $J$ predicate symbols and $E$ constant and
function symbols;

  * •

$\mathcal{T}$ – A progressing timed MSR constructed over $\Sigma$;

  * •

$\mathcal{S}_{0}$ – An initial configuration;

  * •

$m$ – The number of facts in the initial configuration $\mathcal{S}_{0}$;

  * •

$\mathcal{CS}$ – A critical configuration specification constructed over
$\Sigma$;

  * •

$k$ – An upper-bound on the size of facts;

  * •

$D_{max}$ – An upper-bound on the numeric values of
$\mathcal{S}_{0},\mathcal{T}$ and $\mathcal{CS}$.

For the $Z$ problem and the $S$ problem, PSPACE-completeness for PTSes was
proved in [16, 17]. PSPACE-hardness of the $L$ problem for PTSes can be shown
by adequately adapting our previous work [21, 17].

######  Proposition 12 ($L$ problem for PTSes is PSPACE hard)

The $L$ problem for PTSes that use the l.t.s. is PSPACE-hard.

###### Proof

The $Z$ problem is an instance of the problem of checking whether a
configuration is not a point-of-no-return. Recall that a system satisfies the
$Z$ property if there exists a compliant infinite time trace $\mathcal{P}$
from the initial configuration in which global time tends to infinity. Since
$\mathcal{T}$ is progressing, we obtain the condition on time (time tends to
infinity) from Proposition 2. Indeed, a system satisfies the $Z$ property if
and only if the initial configuration is not a point-of-no-return. Since
PSPACE and co-PSPACE are the same complexity class and the $Z$ property is
PSPACE-hard, the problem of determining whether a configuration is a point-of-
no-return is PSPACE-hard.

Since the $L$ property problem comprises checking whether a configuration is a
point-of-no-return, it is PSPACE-hard. ∎

Infinite traces over configurations of PTSes are infinite time traces
(Proposition 2). The same holds for traces over $\delta$-representations of
PTSes. For our verification problems we, therefore, need to construct an
infinite compliant trace. The following lemma establishes a criterion.

###### Lemma 2

For a PTS $\mathcal{T}$ assume
$\Sigma,\mathcal{S}_{0},m,\mathcal{CS},k,D_{max}$ as described above. If there
is a compliant trace (constructed using $\delta$-representations) starting
with the $\delta$-representation of $\mathcal{S}_{0}$ with length
$L_{\Sigma}(m,k,D_{max})$, then there is an _infinite_ compliant trace
starting with the $\delta$-representation of $\mathcal{S}_{0}$. [16]

###### Proof

Since there are only $L_{\Sigma}(m,k,D_{max})$ different
$\delta$-representations, a trace of length greater than
$L_{\Sigma}(m,k,D_{max})$ necessarily contains the same
$\delta$-representations twice, that is, there is a loop in the trace. By
repeating the $\delta$-representations appearing in the loop, we can construct
an infinite trace which is necessarily compliant. ∎

For our complexity results we use some auxiliary functions with configurations
or $\delta$-representations as their arguments, as suitable. For our next
results involving the four properties, assume that for any given timed MSR
$\mathcal{T}$, an initial configuration $\mathcal{S}_{0}$ and a critical
configuration specification $\mathcal{CS}$ we have two functions, and
$\mathcal{X}$, which check, respectively, whether a rule in $\mathcal{T}$ is
applicable to a given $\delta$-representation and whether a
$\delta$-representation is critical with respect to $\mathcal{CS}$. Moreover,
for a given timed MSR $\mathcal{T}$, let $\mathcal{L}$ be a function
implementing the l.t.s. a $\delta$-representation of system $\mathcal{T}$, and
returns 1 when the $Tick$ must be applied and 0 when it must not be applied
according to the l.t.s. We assume that , $\mathcal{X}$, and $\mathcal{L}$ run
in Turing space bounded by a polynomial in $m,k,\log_{2}(D_{max})$. Notice
that for our examples this is the case, as such functions can be constructed
because the system is balanced and facts are of bounded size.

Because of Lemma 2, we can show that the $Z$ problem is in PSPACE by searching
for compliant traces of length $L_{\Sigma}(m,k,D_{max})$ (stored in binary).
To do so, we rely on the fact that PSPACE and NPSPACE are the same complexity
class [29].

######  Proposition 13 (Realizability for PTSes is in PSPACE)

For a PTS $\mathcal{T}$ assume
$\Sigma,\mathcal{S}_{0},m,\mathcal{CS},k,D_{max}$, $,\mathcal{X}$, and
$\mathcal{L}$ as described above.

There is an algorithm that, given an initial configuration $\mathcal{S}_{0}$,
decides whether $\mathcal{T}$ satisfies the $Z$ property with respect to the
l.t.s., $\mathcal{CS}$, and $\mathcal{S}_{0}$ and the algorithm runs in a
space bounded by a polynomial in $m,k$ and $log_{2}(D_{max})$.

The polynomial is in fact $\log_{2}(L_{\Sigma}(m,k,D_{max}))$. [16]

We now consider the $S$ problem. Recall that in order to prove that
$\mathcal{T}$ satisfies the $S$ property with respect to the l.t.s., a
critical configuration specification $\mathcal{CS}$ and an initial
configuration $\mathcal{S}_{0}$, we must show that $\mathcal{T}$ satisfies the
$Z$ property w.r.t. the l.t.s., $\mathcal{CS}$ and $\mathcal{S}_{0}$, and that
all infinite traces $\mathcal{P}$ that use the l.t.s. and start with
$\mathcal{S}_{0}$ are compliant with respect to $\mathcal{CS}$, and that the
global time in $\mathcal{P}$ tends to infinity (Definition 13).

Checking that a system satisfies the $Z$ property is PSPACE-complete as we
have just shown. Moreover, the property that time tends to infinity follows
from Proposition 2 for progressing timed MSR. It remains to show that all
infinite traces using the l.t.s. are compliant, which reduces to checking that
_no critical configuration is reachable_ from the initial configuration
$\mathcal{S}_{0}$ by a trace that uses the l.t.s. This property can be decided
in PSPACE by relying on the fact that PSPACE, NPSPACE and co-PSPACE are all
the same complexity class [29]. Therefore, the $S$ problem is also in PSPACE.

######  Proposition 14 (Survivability for PTSes is in PSPACE)

For a PTS $\mathcal{T}$ assume
$\Sigma,\mathcal{S}_{0},m,\mathcal{CS},k,D_{max}$, $,\mathcal{X}$, and
$\mathcal{L}$ as described above.

There is an algorithm that decides whether $\mathcal{T}$ satisfies the the $S$
property with respect to the l.t.s., $\mathcal{CS}$ and $\mathcal{S}_{0}$
which runs in space bounded by a polynomial in $m,k$ and $log_{2}(D_{max})$.
[16]

We now investigate the complexity of the $L$ problem for PTSes, that is for
the problem of deciding whether a given PTS satisfies the $L$ property. This
problem coincides with the $V$ problem for PTSes. Recall that a configuration
$\mathcal{S}$ is a point-of-no-return iff there is no compliant infinite time
trace from $\mathcal{S}$ that uses the l.t.s.

######  Proposition 15 (Reliability for PTSes is in PSPACE)

For a PTS $\mathcal{T}$ assume
$\Sigma,\mathcal{S}_{0},m,\mathcal{CS},k,D_{max}$, $,\mathcal{X}$, and
$\mathcal{L}$ as described above.

There is an algorithm that, given an initial configuration $\mathcal{S}_{0}$,
decides whether $\mathcal{T}$ satisfies the $L$ property with respect to the
l.t.s., $\mathcal{CS}$ and $\mathcal{S}_{0}$ and the algorithm runs in space
bounded by a polynomial in $m,k$ and $log_{2}(D_{max})$.

###### Proof

We first propose an algorithm that, for a fixed system $\mathcal{T}$ and a
fixed critical configuration specification $\mathcal{CS}$, checks whether some
$\delta$-representation corresponds to a configuration that is a point-of-no-
return w.r.t. $\mathcal{T}$ and $\mathcal{CS}$.

Following PSPACE-completeness of the $Z$ problem [16, 17], let $REAL$ denote
the $Z$ problem PSPACE algorithm over $\delta$-representations. (For details,
see the proof of [17, Theorem 1].) When given $\delta$-representation
$\mathcal{W}$, as input, the algorithm $REAL(\mathcal{W})$ returns ACCEPT if
and only if there is an infinite time trace of $\mathcal{T}$ that starts with
$\mathcal{W}$, uses the l.t.s., and is compliant w.r.t. $\mathcal{CS}$, and it
runs in polynomial space w.r.t. the given parameters, $m,k$ and
$log_{2}(D_{max})$. Since PSPACE and co-PSPACE are the same complexity class
[29], we switch the ACCEPT and FAIL and obtain a deterministic algorithm
$NOTREAL$ that runs in polynomial space w.r.t. $m,k$ and $log_{2}(D_{max})$.
The algorithm $NOTREAL(\mathcal{W})$ accepts if and only if there is no
compliant infinite time trace from $\mathcal{W}$ that uses the l.t.s.

Then, using $NOTREAL$ we construct the algorithm $PON$ that checks whether the
given $\delta$-representation $\mathcal{W}$ corresponds to a point-of-no-
return. Let $PON$ be the following algorithm, which takes a
$\delta$-representation $\mathcal{W}$ as input:

>   1. 1.
>
> If $\mathcal{X}(W)=1$, i.e., if $W$ represents a critical configuration,
> then return FAIL, otherwise continue;
>
>   2. 2.
>
> If $NOTREAL(W)=1$, i.e., if $W$ represents a point-of-no-return, then return
> ACCEPT, otherwise return FAIL.
>
>

When given $\delta$-representation $\mathcal{W}$, as input, the algorithm
$PON(\mathcal{W})$ accepts if and only if $\mathcal{W}$ is a
$\delta$-representation of a point-of-no-return w.r.t. $\mathcal{T}$ and
$\mathcal{CS}$. Since $\mathcal{X}$ and $NOTREAL$ run in the polynomial space
w.r.t. $m,k$ and $log_{2}(D_{max})$, $PON$ is a deterministic algorithm that
also runs in such a polynomial space.

Next, we check that for any configuration $\mathcal{S}$ reachable from
$\mathcal{S}_{0}$ using the l.t.s., there is a compliant infinite time trace
from $\mathcal{S}$, i.e., that $\mathcal{S}$ is not a point-of-no-return. The
following algorithm accepts when no point-of-no-return is reachable from
$\mathcal{S}_{0}$ in $\mathcal{T}$ on a compliant trace that uses the l.t.s.,
and fails otherwise. It begins with $i=0$ and $W_{0}$ set to be the
$\delta$-representation of $\mathcal{S}_{0}$, and iterates the following
sequence of operations:

>   1. 1.
>
> If $W_{i}$ represents a critical configuration, i.e., if
> $\mathcal{X}(W_{i})=1$, then return FAIL, otherwise continue;
>
>   2. 2.
>
> If $W_{i}$ represents a point-of-no-return, i.e., if $PON(W_{i})=1$, then
> return FAIL, otherwise continue;
>
>   3. 3.
>
> If $i>L_{\Sigma}(m,k,D_{max})$, then ACCEPT; else continue;
>
>   4. 4.
>
> If $\mathcal{L}$$(W_{i})=1$, then replace $W_{i}$ by $W_{i+1}$ obtained from
> $W_{i}$ by applying the $Tick$ rule; Otherwise non-deterministically guess
> an instantaneous rule, $r$, from $\mathcal{T}$ applicable to $W_{i}$, i.e.,
> such a rule $r$ that $(r,W_{i})=1$. If so, replace $W_{i}$ with the
> $\delta$-representation $W_{i+1}$ resulting from applying the rule $r$ to
> the $\delta$-representation $W_{i}$. Otherwise, continue;
>
>   5. 5.
>
> Set $i=i+1$.
>
>

Since $PON$, $,\mathcal{X}$ and $\mathcal{L}$ run in Turing space bounded by a
polynomial in $m$, $k$ and $\log_{2}(D_{max})$, it follows that the above
algorithm runs in deterministic polynomial space. ∎

###### Theorem 6.1

Let $\Sigma$ be a finite alphabet, $\mathcal{T}$ a PTS, $\mathcal{S}_{0}$ an
initial configuration, $m$ the number of facts in $\mathcal{S}_{0}$,
$\mathcal{CS}$ a critical configuration specification, $k$ an upper-bound on
the size of facts, and $D_{max}$ an upper-bound on the numeric values in
$\mathcal{S}_{0},\mathcal{T}$ and $\mathcal{CS}$. Let the functions
$,\mathcal{X}$, and $\mathcal{L}$ run in Turing space bounded by a polynomial
in $m,k,\log_{2}(D_{max})$ and return 1, respectively, when a rule in
$\mathcal{T}$ is applicable to a given $\delta$-representation, when a
$\delta$-representation is critical with respect to $\mathcal{CS}$, and when a
$Tick$ rule should be applied to the given $\delta$-representation using the
l.t.s.

The $L$ problem for PTSes that use the l.t.s. is PSPACE-complete when assuming
a bound on the size of facts.

###### Proof

The result follows directly from Propositions 12 and 15. ∎

###### Remark 4

The PSPACE-completeness of the $Z$ and $S$ problems obtained in [16] follows
directly from Propositions 13 and 14, and the lower bound proof from [17,
Appendix C].

###  6.2 Complexity Results for Time-Bounded Problems

We now consider the $n$-time versions of the problems defined in Section 4.3.

The following lemma establishes an upper-bound on the length of traces with
exactly $n$ instances of $Tick$ rules for PTSes. This bound is immediately
obtained from Proposition 1.

###### Lemma 3

Let $n$ be fixed. Let $\mathcal{T}$ be a PTS, $\mathcal{S}_{0}$ an initial
configuration and $m$ the number of facts in $\mathcal{S}_{0}$. For all traces
$\mathcal{P}$ of $\mathcal{T}$ that start with $\mathcal{S}_{0}$ and contain
exactly $n$ instances of the Tick rule, the length of $\mathcal{P}$ is bounded
by $(n+1)*m+n$. [16]

###### Proof

Assume that there are exactly $n$ time ticks in $\mathcal{P}$. As per
Proposition 1 there are at most $m-1$ instantaneous rules between any $Tick$
and the next $Tick$ rule in $\mathcal{P}$. Consequently, in total there are at
most $(n+1)\cdot m+n$ rules in $\mathcal{P}$. ∎

###### Remark 5

For our bounded versions of the $Z$ , $L$ and $S$ problems we use auxiliary
functions with configurations as their arguments. For simplicity, we still use
the same notation, $,\mathcal{X}$, and $\mathcal{L}$ , as types of arguments
are clear from the context. We will assume that , $\mathcal{X}$, and
$\mathcal{L}$ run in time bounded by a polynomial in $m$ and $k$, and return
1, respectively, when a rule in $\mathcal{T}$ is applicable to a given
configuration, when a configuration is critical with respect to
$\mathcal{CS}$, and when a $Tick$ rule should be applied to the given
configuration using the l.t.s. Notice that for our examples one can construct
such functions.

For NP-hardness, we encode the NP-hard problem 3-SAT as an the $n$-$Z$ problem
similar to our previous work [13, 12].

###### Proposition 16

The $n$-$Z$ problem for PTSes w.r.t. the l.t.s. is NP-hard. [16, 17]

###### Proof

Assume we are given a formula $\widetilde{C}_{n}=(l_{11}\lor l_{12}\lor
l_{13})\land\cdots\land(l_{n1}\lor l_{n2}\lor l_{n3})$ in 3-CNF, i.e., in a
conjunctive normal form with exactly 3 literals in each clause. Recall that
each literal, $l_{ij}$, is either an atomic formula, $v_{k}$ or its negation,
$\neg v_{k}$.

Let $p$ be the number of variables and $n$ the number of clauses in $F$.

We construct an initial configuration $\mathcal{S}_{0}$ and a progressing
timed MSR $\mathcal{T}$ that uses the l.t.s. to check whether $F$ is
satisfiable or not.

We set $\mathcal{CS}=\emptyset$ and the initial configuration as

$\mathcal{S}_{0}=\\{\
Time@0,\,V_{1}@0,\ldots,\,V_{p}@0,\,I_{\widetilde{C}_{n}})@0\ \\}\ .$

Here, and henceforth, the fact $I_{C}$ represents a conjunctive normal form
$C$.

With $V_{1}$,…,$V_{n}$, we generate, non-deterministically, the truth values
to be assigned to $x_{1}$,…,$x_{n}$:

$\begin{array}[]{@{}l}Time@T,\
{\color[rgb]{0.65,0,0}V_{i}@T_{i}}\,\mid\,\\{~{}T_{i}\leq T~{}\\}\
\longrightarrow\ Time@T,\ {\color[rgb]{0,0.44,0.57}A_{i,1}@(T+1)}\\\ Time@T,\
{\color[rgb]{0.65,0,0}V_{i}@T_{i}}\,\mid\,\\{~{}T_{i}\leq T~{}\\}\
\longrightarrow\ Time@T,\ {\color[rgb]{0,0.44,0.57}A_{i,0}@(T+1)}\end{array}$
(10)

where $A_{i,1}$ stands for: “1 is assigned to $x_{i}$, ” and $A_{i,0}$ means:
“0 is assigned to $x_{i}$. ” Intuitively, these rules construct an
interpretation for the variables in $F$.

To cut our presentation, we introduce the following abbreviation

$x_{i}^{\varepsilon}:=\left\\{\begin{array}[]{rl}{}x_{i},&\quad\mbox{for\ \
$\varepsilon=1$}.\\\ {}\neg x_{i},&\quad\mbox{for\ \
$\varepsilon=0$}.\end{array}\right.$ (11)

For each disjunct $(x_{k_{1}}^{\varepsilon_{1}}\lor
x_{k_{2}}^{\varepsilon_{2}}\lor x_{k_{3}}^{\varepsilon_{3}})$, let
$A_{k_{1},\varepsilon_{1}}$, $A_{k_{2},\varepsilon_{2}}$,
$A_{k_{3},\varepsilon_{3}}$ be the facts that makes the disjunct “true”.
Notice that there are only three such facts for each disjunct.

Now we “compute” the value of the CNF $\widetilde{C}_{n}$ starting from the
left-most disjuncts by repeatedly erasing the correct disjuncts, replacing
$I_{(x_{k_{1}}^{\varepsilon_{1}}\lor x_{k_{2}}^{\varepsilon_{2}}\lor
x_{k_{3}}^{\varepsilon_{3}})\land C}$ with the shorter $I_{C}$, as follows

$\begin{array}[]{@{}l}Time@T,\,{\color[rgb]{0.65,0,0}A_{k_{1},\varepsilon_{1}}@T_{1}},\
{\color[rgb]{0.65,0,0}I_{(x_{k_{1}}^{\varepsilon_{1}}\lor
x_{k_{2}}^{\varepsilon_{2}}\lor x_{k_{3}}^{\varepsilon_{3}})\land
C}@T_{2}}\,\mid\,\\{\,T_{1}\leq T,\ T_{2}\leq T\,\\}\\\ \longrightarrow\
Time@T,\,{\color[rgb]{0,0.44,0.57}A_{k_{1},\varepsilon_{1}}@T_{1}},\
{\color[rgb]{0,0.44,0.57}I_{C}@(T+1)}\\\
Time@T,\,{\color[rgb]{0.65,0,0}A_{k_{2},\varepsilon_{2}}@T_{1}},\
{\color[rgb]{0.65,0,0}I_{(x_{k_{1}}^{\varepsilon_{1}}\lor
x_{k_{2}}^{\varepsilon_{2}}\lor x_{k_{3}}^{\varepsilon_{3}})\land
C}@T_{2}}\,\mid\,\\{\,T_{1}\leq T,\ T_{2}\leq T\,\\}\\\ \longrightarrow\
Time@T,\,{\color[rgb]{0,0.44,0.57}A_{k_{2},\varepsilon_{2}}@T_{1}},\
{\color[rgb]{0,0.44,0.57}I_{C}@(T+1)}\\\
Time@T,\,{\color[rgb]{0.65,0,0}A_{k_{3},\varepsilon_{3}}@T_{1}},\
{\color[rgb]{0.65,0,0}I_{(x_{k_{1}}^{\varepsilon_{1}}\lor
x_{k_{2}}^{\varepsilon_{2}}\lor x_{k_{3}}^{\varepsilon_{3}})\land
C}@T_{2}}\,\mid\,\\{\,T_{1}\leq T,\ T_{2}\leq T\,\\}\\\ \longrightarrow\
Time@T,\,{\color[rgb]{0,0.44,0.57}A_{k_{3},\varepsilon_{3}}@T_{1}},\
{\color[rgb]{0,0.44,0.57}I_{C}@(T+1)}\end{array}$ (12)

By inspection, the constructed $\mathcal{T}$ is a progressing timed MSR.

The CNF $\widetilde{C}_{n}$ is satisfiable iff there is a trace that in $2n$
time steps leads from $S_{0}$ into a configuration, which include
$I_{\emptyset}@T$. Namely, we spend $n$ time steps, see (10), to generate the
truth values, and the next $n$ time steps, see (12), to get the correct values
of all $n$ disjuncts.

Hence, the $2n$-$Z$ property problem is NP-hard. ∎

For the $n$-$S$ problem we obtain a new lower bound complexity result.

###### Proposition 17

The $n$-$S$ problem for PTSes w.r.t. the l.t.s. is both NP-hard and coNP-hard.

###### Proof

Recall the 3-SAT encoding from the proof of Proposition 16, showing that the
$n$-$Z$ problem is NP-hard. Since in the encoding the critical configuration
specification is empty, $\mathcal{CS}=\emptyset$, all traces are necessarily
compliant. Therefore, the $n$-$S$ problem is NP-hard as well.

##### coNP-hardness

In order to prove that the $n$-$S$ problem is coNP-hard, we will modify our
original system in the following way.

Let all configurations that include $I_{\emptyset}@T$ are declared critical,
i.e., let $\mathcal{CS}^{\prime}=\\{I_{\emptyset}@T\\}$. To circumvent the $Z$
property issues, we add the “dummy” rules, $j=0,1,2,\dots 2n$:

$\begin{array}[]{@{}l}Time@T,\ H_{j}@T_{j}\,\mid\,\\{~{}T_{j}\leq T~{}\\}\
\longrightarrow\ Time@T,\ H_{j+1}@(T+1)\end{array}$ (13)

Also, $H_{0}$ is added to the initial configuration:

$S_{0}^{\prime}=\\{\ Time@0,\ V_{1}@0,\ ...,\ V_{n}@0,\
I_{\widetilde{C}_{n}}@0,\ H@0\\}$ (14)

The $2n$-$Z$ problem is trivial because of (13).

If CNF $\widetilde{C}_{n}$ is satisfiable then there is a trace $\tau$ that in
$2n$ time steps leads from $S_{0}$ into a configuration $S$, which include
$I_{\emptyset}@T$. Naemly, we spend $n$ time steps, see (10), to generate the
truth values, and the next $n$ time steps, see (12), to get the correct values
of all $n$ disjuncts.

Since $S$ is critical, the trace $\tau$ is not compliant, and, hence, our
updated system does not satisfy $2n$-$S$ property.

If CNF $\widetilde{C}_{n}$ is not satisfiable then there is no trace that
leads from $S_{0}$ into a configuration $S$, which include $I_{\emptyset}@T$.
Hence, our system satisfies $2n$-$S$ property, and the $n$-$S$ problem is
coNP-hard.

Bringing the things together we conclude that the $n$-$S$ problem is both NP-
hard and coNP-hard. ∎

The $n$-$Z$ problem is in NP as stated in the following Proposition.

######  Proposition 18 ($n$-$Z$ problem is in NP)

For a PTS $\mathcal{T}$ assume
$\Sigma,\mathcal{S}_{0},m,\mathcal{CS},k,D_{max}$, $,\mathcal{X}$, and
$\mathcal{L}$ as described above.
The $n$-$Z$ problem for $\mathcal{T}$ w.r.t. the l.t.s., $\mathcal{CS}$, and
$\mathcal{S}_{0}$ is NP-complete. [16, 17]

We now provide the upper bound complexity result for the $n$-$S$ problem for
progressing timed MSRs.

Recall that for the $n$-$S$ property, we need to show that:

  1. 1.

$\mathcal{T}$ satisfies $n$-$Z$ property with respect to $\mathcal{CS}$;

  2. 2.

All traces using the l.t.s. with exactly $n$ ticks are compliant with respect
to $\mathcal{CS}$.

######  Proposition 19 ($n$-$S$ problem is in $\Delta_{2}^{p}$ )

For a PTS $\mathcal{T}$ assume
$\Sigma,\mathcal{S}_{0},m,\mathcal{CS},k,D_{max}$, $,\mathcal{X}$, and
$\mathcal{L}$ as described above.

The $n$-$S$ problem for $\mathcal{T}$ w.r.t. the l.t.s., $\mathcal{CS}$ and
$\mathcal{S}_{0}$ is in the class $\Delta_{2}^{p}$ of the polynomial hierarchy
($P^{NP}$) with input $\mathcal{S}_{0}$. [16, 17]

Finally, we provide the complexity upper bound for the $n$-$L$ problem for
PTSes.

######  Proposition 20 ($n$-$L$ problem is in $\Pi_{2}^{p}$ )

For a PTS $\mathcal{T}$ assume $\Sigma,\mathcal{S}_{0}$, $m$, $\mathcal{CS}$,
$k$, $D_{max}$, $,\mathcal{X}$, and $\mathcal{L}$ as described above.

The $n$-$L$ problem for $\mathcal{T}$ w.r.t. the l.t.s., $\mathcal{CS}$ and
$\mathcal{S}_{0}$ is in $\Pi_{2}^{p}$, the second class of the polynomial
hierarchy with input $\mathcal{S}_{0}$.

###### Proof

We formalize the bounded reliability problem with the following predicate
$L_{n}(S_{0},S_{1},\dots,S_{n})$, which means that

> “ The configurations $S_{0}$, $S_{1}$, $S_{2}$, dots, $S_{n}$, form a trace
>
> $S_{0}\rightarrow S_{1}\rightarrow S_{2}\rightarrow\dots\rightarrow S_{n}$
>
> in which all $S_{0}$, $S_{1}$, $S_{2}$, dots, $S_{n}$ are not critical.”

With the initial $S_{0}$, then the system is n-L reliable iff (realizability)

$\exists S^{\prime}_{1}\ \exists S^{\prime}_{2}\ \exists\ \dots\ \exists
S^{\prime}_{n}L_{n}(S_{0},S^{\prime}_{1},\dots,S^{\prime}_{n})$

and (reliability) for any $k$ such that $k=0,1,\dots,n$, the following holds:

$\forall S_{1}\ \forall S_{2}\ \forall\dots\ \forall S_{k}\
(L_{k}(S_{0},S_{1},\dots,S_{k})\longrightarrow\exists S_{k+1}\
L_{k+1}(S_{0},S_{1},\dots,S_{k},S_{k+1}))$

Hence we can rewrite the above statement in the form of $\Pi_{2}^{p}$, the
second class in the polynomial hierarchy,

$\forall x_{1}\ \forall x_{2}\ \forall\dots\ \forall x_{m}\ \exists y_{1}\
\exists y_{2}\ \exists\dots\ \exists y_{m}\
Q(x_{1},x_{2},\dots,x_{m},y_{1},y_{2},\dots,y_{m})$

where $Q(x_{1},x_{2},\dots,x_{m},y_{1},y_{2},\dots,y_{m})$ is recognizable in
polynomial time.

∎

The obtained complexity result for the time-bounded verification problem of
$L$ problem is stated in the next theorem.

###### Theorem 6.2

Assume $\Sigma$ a finite alphabet, $\mathcal{T}$ a PTS, $\mathcal{S}_{0}$ an
initial configuration, $m$ the number of facts in $\mathcal{S}_{0}$,
$\mathcal{CS}$ a critical configuration specification and $k$ an upper-bound
on the size of facts. Let functions $,\mathcal{X}$, and $\mathcal{L}$ run in
Turing time bounded by a polynomial in $m$ and $k$ and return 1, respectively,
when a rule in $\mathcal{T}$ is applicable to a given configuration, when a
configuration is critical with respect to $\mathcal{CS}$, and when a $Tick$
rule should be applied to the given configuration.

The $n$-$Z$ problem for $\mathcal{T}$ w.r.t. the l.t.s., $\mathcal{CS}$, and
$\mathcal{S}_{0}$ is NP-complete with input $\mathcal{S}_{0}$.

The $n$-$S$ problem for $\mathcal{T}$ w.r.t. the l.t.s., $\mathcal{CS}$, and
$\mathcal{S}_{0}$ is both NP-hard and coNP-hard with input $\mathcal{S}_{0}$.
Furthermore, the $n$-$S$ problem for $\mathcal{T}$ w.r.t. the l.t.s.,
$\mathcal{CS}$, and $\mathcal{S}_{0}$ is in the class $\Delta_{2}^{p}$ of the
polynomial hierarchy ($P^{NP}$) with input $\mathcal{S}_{0}$.

The $n$-$L$ problem for $\mathcal{T}$ w.r.t. the l.t.s., $\mathcal{CS}$ and
$\mathcal{S}_{0}$ is in the class $\Pi_{2}^{p}$ of the polynomial hierarchy
with input the $\mathcal{S}_{0}$.

##  7 Related and Future Work

In this paper, we study a subclass of timed MSR systems called progressing
timed systems introduced in [16], which is defined by imposing syntactic
restrictions on MSR rules.

We discuss two verification problems, namely realizability and survivability,
introduced in [16], and also consider two new properties, reliability and
recoverability, defined over infinite traces. We show that these problems are
PSPACE-complete for progressing timed systems, and when we additionally impose
a bound on time, the realizability becomes NP-complete, the survivability is
in $\Delta_{2}^{p}$, the reliability is in $\Pi_{2}^{p}$ class of the
polynomial hierarchy, and the survivability is both NP-hard and coNP-hard. The
lower bound for the $n$-time reliability is left for future work.

These problems involve quantitative temporal properties of timed systems and
explicit time constraints, and to the best of our knowledge have not been
studied in the rewriting literature. We review some of the formalisms for
specifying quantitative temporal properties of timed systems such as timed
automata, temporal logic, and rewriting.

Others have proposed languages for specifying properties that allow explicit
time constraints. We review some of these formalisms, such as timed automata,
temporal logic, and rewriting.

Our progressing condition is related to the finite-variability assumption used
in the temporal logic and timed automata literature [11, 23, 24, 2, 3],
requiring that in any bounded interval of time, there can be only finitely
many observable events or state changes. Similarly, progressing systems have
the property that only a finite number of instantaneous rules can be applied
in any bounded interval of time (Proposition 1). Such a property seems to be
necessary for the decidability of many temporal verification problems.

The work [1, 6] classifies (sets of) traces as safety, liveness, or properties
that can be reduced to subproblems of safety and liveness. Following this
terminology, properties that relate to our verification problems over infinite
traces contain both elements of safety and elements of liveness. We do not see
how this can be expressed precisely in terms of [1, 6]. We leave this
investigation to future work.

As discussed in detail in the Related Work section of our previous work [20],
there are some important differences between our timed MSR model and timed
automata [2, 3], both in terms of expressive power and decidability proofs.
For example, a description of a timed MSR system uses first order formulas
with variables, whereas timed automata can only refer to transitions on ground
states. That is, timed MSR is essentially a first-order language, while timed
automata are propositional. Replacing a first order description of timed MSR
by all its instantiations, would lead to an exponential explosion.
Furthermore, in contrast with the timed automata paradigm, in timed MSR we can
naturally manipulate facts both in the past, in the future, as well as in the
present.

The temporal logic literature has proposed many languages for the
specification and verification of timed systems. Many temporal logics contain
quantitative temporal operators, e.g., [24, 23], including time-constrained
temporal operators. Metric Temporal Logic (MTL) [22] involves (bounded or
unbounded) timing constraints on temporal operators similar to our time
constraints. The growing literature on MTL explores the expressivity and
decidability of fragments of such temporal logics [27]. However, the temporal
logic literature does not discuss notions similar to e.g., realizability or
survivability. In addition to that, an important feature of our model is that
the specifications are executable. As we have shown through experiments in
[16], it is feasible to analyze fairly large progressing systems using the
rewriting logic tool Maude [7].

Real-Time Maude [26] is a tool for simulation and analysis of real-time
systems. Rewrite rules are partitioned into instantaneous rules and rules that
advance time, with instantaneous rules taking priority. Our lazy time sampling
is inspired by such management of time in traces. Time advance rules in Real-
Time Maude may place a bound on the amount of time to advance, but do not
determine a specific amount, thus, allowing the system to be continuously
observed. Time sampling strategies are used to implement search and model-
checking analysis. Ölveczky and Messeguer [25] investigate conditions under
which the maximal time sampling strategy used in Real-Time Maude is complete.
One of the required conditions is tick-stabilizing, which is similar to
progressing and the finite variability assumption in that one assumes a bound
on the number of actions that can be applied in a finite time.

Cardenas  _et al._ [4] discuss possible verification problems of cyber-
physical systems in the presence of malicious intruders. They discuss
surviving attacks, such as denial of service attacks on control mechanisms of
devices. We believe that our progressing timed systems can be used to define
meaningful intruder models and formalize the corresponding survivability
notions. This may lead to automated analysis of such systems similar to the
successful use of the Dolev-Yao intruder model [8] for protocol security
verification. Given the results of this paper, the decidability of any
security problem would most likely involve a progressing timed intruder model.
We intend to investigate the security aspects of this work in the future. For
example, the introduction of timed intruder models [14], and resource-bounded
intruder models [32] may enable verification of whether intruders can cause
PTSes to reach hazardous situations, e.g., harm to people or crashes.

We believe that some of our properties, in particular survivability, can be
interpreted using game theory. We find that our model has some features that
are better suited for applications relating to TSDSes, in particular explicit
time, quantitative time conditions and nonces. It would be interesting to
investigate connections and differences between our rewriting approach to
these problems and the game theory approach.

Finally, we have already done some preliminary research into ways to extend
this work to dense time domains. We expect our results to hold for dense time
domains as well, given our previous work [18, 33, 32]. There, instead of the
$Tick$ rule (Eq. 1), we assume a $Tick$ rule of the form
$Time@T\longrightarrow Time@(T+\varepsilon)$, where $\varepsilon$ can be
instantiated by any positive real number. The assumption of dense time is a
challenge that considerably increases the machinery needed to prove our
results, but we are confident of finding ways to combine the results of [18]
with those presented in this paper. Similarly, for our future work, we intend
to investigate extensions of our models with probabilities.

_Acknowledgments:_ Ban Kirigin is supported in part by the Croatian Science
Foundation under the project UIP-05-2017-9219. The work of Max Kanovich was
partially supported by EPSRC Programme Grant EP/R006865/1: “Interface
Reasoning for Interacting Systems (IRIS).” Nigam is partially supported by NRL
grant N0017317-1-G002, and CNPq grant 303909/2018-8. Scedrov was partially
supported by the U. S. Office of Naval Research under award numbers
N00014-20-1-2635 and N00014-18-1-2618. Talcott was partially supported by the
U. S. Office of Naval Research under award numbers N00014-15-1-2202 and
N00014-20-1-2644, and NRL grant N0017317-1-G002.

## References

  * [1] B. Alpern and F. B. Schneider.  Recognizing safety and liveness.  Distributed Computing, 2(3):117–126, 1987.
  * [2] R. Alur and T. A. Henzinger.  Logics and models of real time: A survey.  In Real-Time: Theory in Practice, REX Workshop, pages 74–106, 1991.
  * [3] R. Alur and P. Madhusudan.  Decision problems for timed automata: A survey.  In SFM, pages 1–24, 2004.
  * [4] A. A. Cárdenas, S. Amin, and S. Sastry.  Secure control: Towards survivable cyber-physical systems.  In ICDCS, pages 495–500, 2008.
  * [5] I. Cervesato, N. A. Durgin, P. Lincoln, J. C. Mitchell, and A. Scedrov.  A meta-notation for protocol analysis.  In CSFW, pages 55–69, 1999.
  * [6] M. R. Clarkson and F. B. Schneider.  Hyperproperties.  Journal of Computer Security, 18(6):1157–1210, 2010.
  * [7] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott.  All About Maude: A High-Performance Logical Framework, volume 4350 of LNCS.  Springer, 2007.
  * [8] D. Dolev and A. Yao.  On the security of public key protocols.  IEEE Transactions on Information Theory, 29(2):198–208, 1983.
  * [9] N. A. Durgin, P. Lincoln, J. C. Mitchell, and A. Scedrov.  Multiset rewriting and the complexity of bounded security protocols.  Journal of Computer Security, 12(2):247–311, 2004.
  * [10] H. B. Enderton.  A mathematical introduction to logic.  Academic Press, 1972.
  * [11] M. Faella, A. Legay, and M. Stoelinga.  Model checking quantitative linear time logic.  Electr. Notes Theor. Comput. Sci., 220(3):61–77, 2008.
  * [12] M. Kanovich, T. Ban Kirigin, V. Nigam, and A. Scedrov.  Progressing collaborative systems.  In FCS-PrivMod, 2010.