<figure><img src="image_1.png" /></figure>

HAL
open science

# On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems

Ievgen Ivanov

► To cite this version:

Ievgen Ivanov. On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems. 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2016, Eindhoven, Netherlands. pp.216-234, 10.1007/978-3-319-40370-0_13 . hal-01446028

HAL Id: hal-01446028

https://inria.hal.science/hal-01446028

Submitted on 25 Jan 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems

Ievgen Ivanov

Taras Shevchenko National University of Kyiv

01601, Kyiv, Volodymyrska st, 60, Ukraine

ivanov.eugen@gmail.com

**Abstract.** We consider two notions of timed bisimulation on states of continuous-time dynamical systems: global and local timed bisimulation. By analogy with the notion of a bisimulation relation on states of a labeled transition system which requires the existence of matching transitions starting from states in such a relation, local timed bisimulation requires the existence of sufficiently short (locally defined) matching trajectories. Global timed bisimulation requires the existence of arbitrarily long matching trajectories. For continuous-time systems the notion of a global bisimulation is stronger than the notion of a local bisimulation and its definition has a non-local character. In this paper we give a local characterization of global timed bisimulation. More specifically, we consider a large class of abstract dynamical systems called Nondeterministic Complete Markovian Systems (NCMS) which covers various concrete continuous and discrete-continuous (hybrid) dynamical models and introduce the notion of an $f^+$-timed bisimulation, where $f^+$ is a so called extensibility measure. This notion has a local character. We prove that it is equivalent to global timed bisimulation on states of a NCMS. In this way we give a local characterization of the notion of a global timed bisimulation.

**Keywords:** bisimulation, cyber-physical system, dynamical system, continuous time, local characterization

## 1 Introduction

The focus of this paper is the notion of bisimulation [1-4] in the domain of continuous-time dynamical systems. A general overview of the history of bisimulation, bisimilarity, coinductive definitions and their relevance to computer science, logic and other fields can be found in [4].

Recall that in the simplest case of labeled transition systems (LTS) [4] bisimulation and bisimilarity can be defined as follows:

A binary relation $R$ on states of an LTS is a bisimulation, if $(q_1, q_2) \in R$ implies that for each state $q'_1$ and a label $a$ such that $q_1 \to^a q'_1$ there exists a state $q'_2$ such that $q_2 \to^a q'_2$ and $(q'_1, q'_2) \in R$, and, conversely, for each state $q'_2$
and a label such that $q_2 \to^a q'_2$ there exists a state $q'_1$ such that $q_1 \to^a q'_1$ and $(q'_1, q'_2) \in R$.

Bisimilarity is the union of all bisimulations.

Associated with these notions is the bisimulation proof method [5, 4], which, in particular, can be used to show behavioral equivalence of processes.

As was pointed out in [4], the features of the definition of bisimulation which make the bisimulation proof method practically interesting are:

- *locality of the checks* in the sense that only immediate transitions from states of a pair $(q_1, q_2) \in R$ need to be examined to verify the conditions of the definition;

- *the lack of hierarchy* on the pairs of the bisimulation (i.e. checks can be done in any order).

Many modifications and extensions of the mentioned definitions were proposed in different contexts [4].

In this paper we are interested in the notions of bisimulation for continuous-time models which are useful for modeling cyber-physical systems [6–9] and giving semantics to related specification and programming languages [10–14]. In this context various definitions of bisimulation relations were proposed [15–21]. A survey and comparison of different approaches can be found in [21, 22].

Most of such approaches consider dynamical system models with an explicit notion of a *global* (continuous) time with respect to which the system’s global state evolves and define some notion of bisimulation on states of such systems.

Such definitions of bisimulation for continuous-time systems can be classified in different ways.

Generally, on one hand there are *reduction-like approaches* which associate a model which has a pre-existing notion of bisimulation (e.g. LTS) with a continuous-time model and consider bisimulation relations for the associated model (in the sense of the pre-existing definition) to be bisimulation relations for the continuous-time model. Approaches of this kind were used for timed automata and several classes of hybrid systems [15] for abstracting infinite-state systems by finite systems and establishing decidability results [15], for abstracting continuous-time linear control systems [16], etc.

On the other hand, there are approaches which define new notions of bisim- ulation *specifically* for the considered classes of continuous-time systems. Ap- proaches of this kind were proposed in [18] for continuous-time linear control systems with disturbances and certain kinds of nonlinear systems, in [19] for dynamical systems in the sense of J.C. Willems behavioral approach [23], in [24, 25] for dynamical systems on manifolds and control and hybrid systems, in [26] for general flow systems.

The way in which a particular definition of bisimulation for continuous-time systems takes into account timing information gives another classification of such definitions.

On one hand, there were proposed time-abstracting bisimulations [27], bisim- ulations of time-abstract transition systems [16], reachability bisimulation [26]
for continuous-time systems which *do not take into account the times* required
by a system to reach a particular state.

On the other hand, *timed bisimulation* definitions require matching of states along trajectories (executions) of a system starting from states related by bisim-ulation at exactly same time moments, e.g. [26, 18]. Intermediate approaches which take into account time information, but do not require exact matching along trajectories starting from states related by a bisimulation were also pro-posed, e.g. *progress bisimulation* [26].

The mentioned approaches to formalization of dynamical systems and the
associated notions of bisimulation and proof methods are quite heterogeneous
and currently lack a uniform treatment (e.g. in terms of coalgebras).

However, comparing various definitions of bisimulation for continuous-time
dynamical/control/hybrid systems to the definition of a bisimulation on the
states of a LTS, an important aspect of these definitions becomes visible: al-
though these definitions do not impose a hierarchy on the pairs (similarly to
bisimulations for LTS [4]), timed bisimulation definitions are *non-local* in the
sense that checking that a pair of states is in a bisimulation relation involves
checking some *“far future” / global properties* of the trajectories of a system
starting in these states (relative to the time moment when these trajectories
start).

In particular, this is true for the bisimulation definitions proposed for abstract types of continuous-time systems, e.g. in [26] the following notion of a timed simulation was introduced for highly abstract *general flow systems*:

If $\Phi_1, \Phi_2$ are general flow systems over value spaces $X_1, X_2$ with the same time line, a binary relation $R$ between $X_1, X_2$ is a timed simulation of $\Phi_1$ by $\Phi_2$, if $\text{dom}(\Phi_1) \subseteq \text{dom}(R)$ and for all $x_1, x'_1 \in X_1$, $x_2 \in X_2$ such that $(x_1, x_2) \in R$ and for all times $t > 0$, if there is a path $\gamma_1 \in \Phi_1(x_1)$ such that $x'_1 = \gamma_1(t)$, then there is $x'_2 \in X_2$ and $\gamma_2 \in \Phi_2(x_2)$ such that $x'_2 = \gamma_2(t)$, $\text{dom}(\gamma_2) = \text{dom}(\gamma_1)$, and $(\gamma_1(s), \gamma_2(s)) \in R$ for all $s \in \text{dom}(\gamma_2) \cap [0, t]$. A relation $R$ is a timed bisimulation between $\Phi_1, \Phi_2$, if both $R$ and $R^{-1}$ are timed simulations (details about the notions used in this definition are given in [26]).

In principle, we agree with definitions of this kind (on both abstract and con-
crete levels), but consider their non-local character undesirable for applications
based on the bisimulation proof method.

Our aim in this paper is to give a *necessary and sufficient condition* (crite-
rion) of a *local* (in time) character for checking that a given relation satisfies a
timed bisimulation definition of this kind. The novelty of the main result is that
local characterization of global timed bisimulation for continuous-time systems
is possible in the very general case and can be given in a uniform way (using
the notion of a so called $f^+$-bisimulation defined below). Local characterization
also makes the notion of bisimulation for systems with continuous-time evolution
close in spirit to the classical notion of bisimulation for LTS (which are most
often used for representing systems with discrete-time evolution) and *allows one
to use a wide variety of well-known methods of local analysis* (in local in time or
in state space) of the behavior of systems defined by differential equations, in-
clusions, certain hybrid (discrete-continuous) formalisms, etc. (e.g. linearization,
various series expansions, approximations, singularity analysis, etc.) *for proving*
*that a given relation is a bisimulation*. Such methods are difficult or impossible to
apply if one tries to prove that a relation is a global timed bisimulation directly
by the definition (since this definition is given in terms of long-term behaviors
of a system instead of short-term behaviors). We also suppose that this result
will be useful for further development of uniform treatment of continuous time
dynamical system models and proof principles related to them using coalgebraic
approach (e.g. definition of bisimulation on continuous-time systems in terms of
coalgebras).

Note that as we have mentioned above, many different definitions of bisim-
ulation for continuous-time systems can be found in the literature. However,
arguably, once a local characterization is obtained for some reasonable formal-
ization X of bisimulation, it may be translated to other formalizations of bisimu-
lation at least when they agree with X (e.g. bisimulation for general flow systems
in the sense of J. Davoren and P. Tabuada [26]). In this paper we do not include
a detailed comparison of different approaches to the definition of bisimulation
for continuous-time systems and local characterization and its limits in each of
such cases, but this remains a topic of further investigation.

To obtain the main result we will consider dynamical systems on a high level of abstraction comparable to the level of the mentioned general flow systems, but use a particular formalization of such systems called *Nondeterministic Complete Markovian Systems* (NCMS).

This formalization was proposed in [28–32] and inspired by the notion of a
solution system from O. Hájek’s Theory of processes [33, 34]. In this formalization
the global non-negative real time scale is assumed and continuous-time systems
are modeled as sets of trajectories considered as functions on real time intervals
which take values in an arbitrary fixed set of states. These sets must satisfy
certain weak assumptions (more details are given in Section 2) [29]:

- be closed under proper restrictions onto intervals;

- satisfy the *Markovian* property which means that if two trajectories meet at one time in one state, their concatenation is a trajectory (note that this Markovian property is not formally related to the probability theory and stochastic processes);

- satisfy the *completeness* property in the following sense: a non-empty chain of trajectories in the sense of a subtrajectory relation has a supremum in the set of trajectories.

One interpretation of the Markovian property is that at any time moment the
set of possible future evolutions of a system depends only on its current state and
time and does not depend on the path by which the system reached the current
state (which is also true for LTS). The definition of Hájek's solution system
is rather similar, but lacks an equivalent of the completeness requirement of
NCMS. But for us completeness is necessary to be able to establish reductions
of global-in-time properties of systems to local-in-time properties.
NCMS are also close to the notion of a TCTL structure in the sense of R. Alur and D. Dill [35], but the definition of the latter TCTL structures lack an equivalent of the completeness assumption. Only with it Markovian property is sufficient for establishing local characterization of bisimulation (informally, Markovian property of NCMS allows joining a finite sequence of trajectories; with completeness it allows joining an infinite sequence of trajectories).

The main reasons we use NCMS are:

- NCMS do not impose restrictions on the structure of the set of states and impose weak restrictions on the system behavior, support nondeterminism and partial trajectories. These features make NCMS promising for computer science and cyber-physical systems applications like semantics of real-time and embedded systems specification languages [30]. In contrast, well-known concrete dynamical system models (classical dynamical systems, switched systems [36], hybrid automata [37, 38]) impose restrictions on the structure of the state space (e.g. assuming that it is a vector space, a manifold, or a related structure) and stronger restrictions on the behavior of a system.

- Concrete continuous-time models (e.g. described by differential equations, switched systems, etc.) can be represented by NCMS [28], similarly to representing different kinds of systems by O. Hájek's solution systems [33, 34]. Some examples of such representations are given in subsection 2.2 below.

- The model of NCMS allows one to reduce some types of global analysis of system behavior to local analysis of system behavior, e.g. prove global properties by checking that certain conditions hold in a neighborhood of each time moment [29]. This is described in more detail in subsection 2.3.

In this paper we will define the notion of a *labeled NCMS* which can be considered as a continuous-time analog of LTS and the notion of a *global timed bisimulation* on the states of a labeled NCMS. We will also define an obvious local version of this notion of a global timed bisimulation which we will call a *local timed bisimulation*. Both notions turn out to be inequivalent in the case of NCMS (local timed bisimulation is strictly weaker than global timed bisimulation). Then we will strengthen the local definition of bisimulation using so-called extensibility measures [29] and call the obtained notion a *$f^+$-timed bisimulation*. This notion will have a local character. Then we will show the equivalence of $f^+$-timed bisimulation and global timed bisimulation, obtaining a local characterization of global timed bisimulation.

The paper is organized in the following way. To make the paper self-contained, we give all necessary preliminaries about NCMS in Section 2. The reader may skip this section or most of it, but consult it whenever necessary. In Section 3 we introduce the notion of a labeled NCMS. In Section 4 we introduce global and local timed simulations and bisimulations on states of labeled NCMS. In Section 5 we formulate and discuss the main result, i.e. the local characterization of global timed bisimulation on states of a labeled NCMS. In Section 6 we give an outline of the proof of the main result. In Section 7 we give conclusions.
# 2 Preliminaries

## 2.1 Notation

We will use the following notation: $\mathbb{N} = \{1, 2, 3, ...\}$ is the set of natural numbers; $\mathbb{R}$ is the set of real numbers; $\mathbb{R}_+$ is the set of nonnegative real numbers; $f: A \to B$ is a total function from a set $A$ to a set $B$; $f: A \stackrel{\sim}{\to} B$ is a partial function from a set $A$ to a set $B$, $2^A$ is the power set of a set $A$; $f|_A$ is the restriction of a function $f$ to a set $A$; $B^A$ is the set of all total functions from a set $A$ to a set $B$; $A^B$ is the set of all partial function from a set $A$ to a set $B$.

For any function $f: A \stackrel{\sim}{\to} B$ we will use the symbol $f(x) \downarrow (f(x) \uparrow)$ to denote that $f(x)$ is defined, or, respectively, is undefined on the argument $x$.

We will not distinguish the notions of a function and a functional binary relation. When we write that a function $f: A \stackrel{\sim}{\to} B$ is total or surjective, we mean that $f$ is total on the set $A$ specifically ($f(x)$ is defined for all $x \in A$), or, respectively, is onto $B$ (for each $y \in B$ there exists $x \in A$ such that $y = f(x)$).

For any $f: A \stackrel{\sim}{\to} B$ denote $dom(f) = \{x | f(x) \downarrow\}$, i.e. the domain of $f$ (note that in some fields like the category theory the domain of a partial function is defined differently).

For any binary relation $R$ denote $R^{-1} = \{(y, x) \mid (x, y) \in R\}$ (the inverse relation).

For any partial functions $f, g$ the notation $f(x) \cong g(x)$ will mean the strong equality: $f(x) \downarrow$ if and only if $g(x) \downarrow$, and $f(x) \downarrow$ implies $f(x) = g(x)$.

Denote by $f \circ g$ the functional composition: $(f \circ g)(x) \cong f(g(x))$.

Denote by $T$ the non-negative real time scale $[0, +\infty)$. We will assume that $T$ is equipped with a topology induced by the standard topology on $\mathbb{R}$.

We will use the symbols $\neg$, $\vee$, $\wedge$, $\Rightarrow$, $\Leftrightarrow$ to denote the logical operations of negation, disjunction, conjunction, implication, and equivalence respectively.

## 2.2 Nondeterministic Complete Markovian Systems

The notion of a Nondeterministic Complete Markovian System (NCMS) was introduced in [28] for studying the existence of global trajectories of dynamical systems. It is close to the notion of a solution system by O. Hájek [33].

Let us denote by $\mathcal{T}$ the set of all intervals in $T$ (connected subsets) which have the cardinality greater than one.

Let $Q$ be a set (a state space) and $Tr$ be some set of functions of the form $s: A \to Q$, where $A \in \mathcal{T}$. We will call the elements of $Tr$ (partial) trajectories.

**Definition 1** ([28, 32]). A set of trajectories $Tr$ is closed under proper restrictions (CPR), if $s|_A \in Tr$ for each $s \in Tr$ and $A \in \mathcal{T}$ such that $A \subseteq dom(s)$.

Let us introduce the following notation: if $f, g$ are partial functions, $f \sqsubseteq g$ means that the graph of $f$ is a subset of the graph of $g$, and $f \sqsupseteq g$ means that the graph of $f$ is a proper subset of $g$.

**Definition 2.** Let $s_1, s_2 \in Tr$ be trajectories. Then:
(1) $s_1$ is called a subtrajectory of $s_2$, if $s_1 \sqsubseteq s_2$;

(2) $s_1$ is called a proper subtrajectory of $s_2 \in Tr$, if $s_1 \sqsubseteq s_2$;

(3) $s_1, s_2$ are called incomparable, if neither $s_1 \sqsubseteq s_2$, nor $s_2 \sqsubseteq s_1$.

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

**Definition 3 ([28, 32]).** A CPR set of trajectories $Tr$ is

(1) Markovian (Fig. 2), if for each $s_1, s_2 \in Tr$ and $t_0 \in T$ such that $t_0 = \sup \operatorname{dom}(s_1) = \inf \operatorname{dom}(s_2)$, $s_1(t_0) \downarrow$, $s_2(t_0) \downarrow$, and $s_1(t_0) = s_2(t_0)$, the following function $s$ belongs to $Tr$: $s(t) = s_1(t)$, if $t \in \operatorname{dom}(s_1)$ and $s(t) = s_2(t)$, if $t \in \operatorname{dom}(s_2)$.

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

<figure><img src="image_3.png" /><figcaption>**Fig. 1.** Markovian property of NCMS. If one (partial) trajectory ends and another begins in a state $q$ at time $t$, then their concatenation is a (partial) trajectory.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>**Fig. 2.** Illustration of the completeness property of NCMS. The limit $s$ of a $\sqsubseteq$-chain of trajectories (illustrated here as curve fragments bounded by dashed ellipses) of a NCMS is itself a trajectory of this NCMS. The graph of $s$ is the union of graphs of elements of the chain.</figcaption></figure>
**Definition 4 ([28, 32]).** A nondeterministic complete Markovian system (NCMS) is a triple $(T, Q, \text{Tr})$, where $Q$ is a set (state space) and $\text{Tr}$ (trajectories) is a set of functions $s: T \to Q$ such that $\text{dom}(s) \in \mathcal{T}$, which is CPR, complete, and Markovian.

The notion of an *LR representation* [28, 32, 29] given below can be used to obtain an overview of the class of all NCMS.

**Definition 5 ([28, 32]).** Let $s_1, s_2: T \to Q$. Then $s_1$ and $s_2$ coincide:

(1) on a set $A \subseteq T$, if $s_1|_A = s_2|_A$ and $A \subseteq \text{dom}(s_1) \cap \text{dom}(s_2)$ (this is denoted as $s_1 \doteq_A s_2$);

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

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

Let $Q$ be a set and $\text{ST}(Q)$ be the set of pairs all $(s, t)$, where $s: A \to Q$ for some $A \in \mathcal{T}$ and $t \in A$.

**Definition 6 ([28, 32]).** A predicate $p: \text{ST}(Q) \to \text{Bool}$ is

(1) left-local, if $p(s_1, t) \Leftrightarrow p(s_2, t)$ whenever $\{(s_1, t), (s_2, t)\} \subseteq \text{ST}(Q)$ and $s_1 \doteq_{t-} s_2$ hold, and, moreover, $p(s, t)$ holds whenever $t$ is the least element of $\text{dom}(s)$;

(2) right-local, if $p(s_1, t) \Leftrightarrow p(s_2, t)$ whenever $\{(s_1, t), (s_2, t)\} \subseteq \text{ST}(Q)$ and $s_1 \doteq_{t+} s_2$ hold, and, moreover, $p(s, t)$ holds whenever $t$ is the greatest element of $\text{dom}(s)$.

Let $\text{LR}(Q)$ denote the set of all pairs $(l, r)$, where $l: \text{ST}(Q) \to \text{Bool}$ is a left-local predicate and $r: \text{ST}(Q) \to \text{Bool}$ is a right-local predicate.

**Definition 7 ([32]).** A pair $(l, r) \in \text{LR}(Q)$ is called a LR representation of a NCMS $\Sigma = (T, Q, \text{Tr})$, if

$$ \text{Tr} = \{s: A \to Q \mid A \in \mathcal{T} \wedge (\forall t \in A \ l(s, t) \wedge r(s, t))\}. $$

The following theorem shows that a NCMS can be represented using predicate pairs.

**Theorem 1 ([32]).**

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

(2) Each NCMS has a LR representation.

Consider some examples of representation of sets of trajectories of well-known continuous and discrete-continuous dynamical models in the form of NCMS.

1. **Ordinary differential equations.** Let $d \in \mathbb{N}$ and $f: \mathbb{R} \times \mathbb{R}^d \to \mathbb{R}^d$ be a continuous function. Let $\text{Tr}$ be the set of all $\mathbb{R}^d$-valued functions such that $\text{dom}(s) \in \mathcal{T}$ (i.e. $s$ is defined on a non-degenerate real interval) such that $s$ is differentiable on the interior of $\text{dom}(s)$ and
- $\frac{d}{dt}s(t) = f(t, s(t))$ holds for each $t$ in the interior of $dom(s)$;

- $\partial_{+}s(t) = f(t, s(t))$, if $t$ is the least element of $dom(s)$;

- $\partial_{-}s(t) = f(t, s(t))$, if $t$ is the greatest element of $dom(s)$,

where $\partial_{-}s(t)$ denotes the left derivative at $t$, and $\partial_{+}s(t)$ denotes the right derivative at $t$. Then $(T, \mathbb{R}^d, Tr)$ is a NCMS.

Indeed, consider predicates $l, r : ST(\mathbb{R}^d) \to \mathit{Bool}$ defined as follows:

- $l(s, t)$ if and only if either $\min dom(s) \downarrow= t$, or $t > \inf dom(s)$ and $\partial_{-}s(t) \downarrow= f(t, s(t))$;

- $r(s, t)$ if and only if either $\max dom(s) \downarrow= t$, or $t < \sup dom(s)$ and $\partial_{+}s(t) \downarrow= f(t, s(t))$.

Obviously, $l(s, t)$ is left-local and $r(s, t)$ is right-local. Moreover, $l(s, t) \wedge r(s, t)$ holds for all $t \in dom(s)$ if and only if $s \in Tr$. Then Theorem 1 implies that $(T, \mathbb{R}^d, Tr)$ is a NCMS. Note that for this result we do not need any assumptions about global existence or uniqueness of solutions of differential equations, because NCMS support partiality and nondeterminism.

2. **Differential inclusions.** Consider a differential inclusion $\dot{x}(t) = F(t, x(t))$, where $F : \mathbb{R} \times \mathbb{R}^d \to 2^{\mathbb{R}^d}$ is a set-valued mapping. Let us introduce an auxiliary variable $y$ and rewrite the inclusion as $$ \begin{cases} \dot{x}(t) = y(t); \\ y(t) \in F(t, x(t)). \end{cases} $$

Let $Q = \mathbb{R}^d \times \mathbb{R}^d$ and $Tr$ be the set of all $Q$-valued functions $s$ such that $dom(s) \in \mathcal{T}$ and there exist functions $x : dom(s) \to \mathbb{R}^d$ and $y : dom(s) \to \mathbb{R}^d$ such that $s(t) = (x(t), y(t))$ and $y(t) \in F(t, x(t))$ for all $t \in dom(s)$ and $x$ is absolutely continuous on each compact segment $[a, b] \subseteq dom(s)$ and satisfies $\dot{x}(t) = y(t)$ almost everywhere (a.e.) on $dom(s)$ in the sense of Lebesgue's measure. Then $(T, Q, Tr)$ is a NCMS. Indeed, consider $l, r : ST(Q) \to \mathit{Bool}$:

- $l(s, t)$ if and only if either $\min dom(s) \downarrow= t$, there exists $t' \in [0, t)$, an absolutely continuous function $x : [t', t] \to \mathbb{R}^d$, and a function $y : [t', t] \to \mathbb{R}^d$ such that $[t', t] \subseteq dom(s)$, $s(\tau) = (x(\tau), y(\tau))$ and $y(\tau) \in F(\tau, x(\tau))$ for all $\tau \in [t', t]$ and $\frac{d}{d\tau}x(\tau) = y(\tau)$ a.e. on $[t', t]$.

- $r(s, t)$ if and only if either $\max dom(s) \downarrow= t$, or there exists $t' > t$, an absolutely continuous function $x : [t, t'] \to \mathbb{R}^d$, and a function $y : [t, t'] \to \mathbb{R}^d$ such that $[t, t'] \subseteq dom(s)$, $s(\tau) = (x(\tau), y(\tau))$ and $y(\tau) \in F(\tau, x(\tau))$ for all $\tau \in [t, t']$ and $\frac{d}{d\tau}x(\tau) = y(\tau)$ a.e. on $[t, t]$.

Obviously, $l(s, t)$ is left-local and $r(s, t)$ is right-local. Moreover, it is easy to check that $l(s, t) \wedge r(s, t)$ holds for all $t \in dom(s)$ if and only if $s \in Tr$. Then $(T, Q, Tr)$ is a NCMS by Theorem 1.

3. **Switched dynamical systems.** Let $d \ge 1$ be a natural number, $I$ be a finite non-empty set (modes of a switched system), and $f_i : T \times \mathbb{R}^d \to \mathbb{R}^d$, $i \in I$ be an indexed family of vector fields (behaviors in each mode). Let $\mathcal{I}$ be the set of all functions $\sigma : T \to I$ (switching signals) which are piecewise-constant on each compact segment $[a, b] \subset T$. Assume that for each $i \in I$, $f_i$ is continuous and bounded on $T \times \mathbb{R}^d$ and there exists a number $L > 0$ such that $||f_i(t, x_1) - f_i(t, x_2)|| \le L||x_1 - x_2||$ for all $x_1, x_2 \in \mathbb{R}^d$, $t \in T$, and $i \in I$ (Lipschitz-continuity). Consider a (nonlinear) switched system

$$ \dot{x}(t) = f_{\sigma(t)}(t, x(t)), \ t \ge 0, \ \sigma \in \mathcal{I}. $$
Note that by Caratheodory existence theorem, for each $x_0 \in \mathbb{R}^d$, $t_0 \in T$, $\sigma \in \mathcal{J}$ the initial value problem $\frac{d}{dt}x(t) = f_{\sigma(t)}(t, x(t))$, $x(t_0) = x_0$ has a unique Caratheodory solution $t \mapsto x(t; t_0; x_0; \sigma)$ defined for all $t \in [t_0, +\infty)$ such that $x(t_0; t_0; x_0; \sigma) = x_0$ (i.e. a function that is absolutely continuous on each compact segment in $[t_0, +\infty)$ and satisfies $\frac{d}{dt}x(t; t_0; x_0; \sigma) = f_{\sigma(t)}(t, x(t; t_0; x_0; \sigma))$ a.e. on $[t_0, +\infty)$).

Let $Q = \mathbb{R}^d \times I$ and $Tr$ be the set of all $Q$-valued functions $s$ such that $dom(s) \in \mathcal{F}$ (i.e. $dom(s)$ is a non-degenerate real interval) and there exist $t_0 \in T$, $x_0 \in \mathbb{R}^d$, $\sigma : dom(s) \to I$ that is piecewise constant on each compact segment in $dom(s)$, and $x : dom(s) \to \mathbb{R}^d$ that is absolutely continuous on each compact segment in $dom(s)$ such that $\frac{d}{dt}x(t) = f_{\sigma(t)}(t, x(t))$ almost everywhere (a.e.) on $dom(s)$ in the sense of Lebesgue's measure and $s(t) = (x(t), \sigma(t))$ for $t \in dom(s)$. Then $(T, Q, Tr)$ is a NCMS.

Indeed, consider predicates $l, r : ST(\mathbb{R}^d) \to Bool$ defined as follows:

- $l(s, t)$ if and only if either $\min dom(s) \downarrow= t$, there exists $t' \in [0, t)$, an absolutely continuous function $x : [t', t] \to \mathbb{R}^d$, and a piecewise-constant function $\sigma : [t', t] \to I$ such that $[t', t] \subseteq dom(s)$, $s(\tau) = (x(\tau), \sigma(\tau))$ for all $\tau \in [t', t]$ and $\frac{d}{d\tau}x(\tau) = f_{\sigma(\tau)}(\tau, x(\tau))$ a.e. on $[t', t]$.

- $r(s, t)$ if and only if either $\max dom(s) \downarrow= t$, or there exists $t' > t$, an absolutely continuous function $x : [t, t'] \to \mathbb{R}^d$, and a piecewise-constant function $\sigma : [t, t'] \to I$ such that $[t, t'] \subseteq dom(s)$, $s(\tau) = (x(\tau), \sigma(\tau))$ for all $\tau \in [t, t']$, and $\frac{d}{d\tau}x(\tau) = f_{\sigma(\tau)}(\tau, x(\tau))$ a.e. on $[t, t']$.

Obviously, $l(s, t)$ is left-local and $r(s, t)$ is right-local. Moreover, it is easy to check that $l(s, t) \wedge r(s, t)$ holds for all $t \in dom(s)$ if and only if $s \in Tr$. Then $(T, Q, Tr)$ is a NCMS by Theorem 1.

Sets of trajectories of some more general switched/hybrid systems (possibly with state-dependent switching) can be represented as NCMS analogously.

## 2.3 Global trajectories of NCMS

The problem of the existence of trajectories of NCMS defined on the whole time domain (global trajectories) was considered in [28, 32, 29]. In [28, 32] a method for proving the existence of a global trajectory in a NCMS was proposed. This method reduces the problem of proving the existence of a global trajectory to the problem of proving the existence of certain locally defined trajectories and can be informally described as follows: (1) guess a “region” (a subset of trajectories) which presumably contains a global trajectory and has a convenient representation in the form of (another) NCMS; (2) prove that this region indeed contains a global trajectory by finding certain locally defined trajectories independently in a neighborhood of each time moment.

Below we briefly state the results which form the basis of this method (Lemma 1 and Theorem 2 given below) which we will use in this paper.

Let $\Sigma = (T, Q, Tr)$ be a fixed NCMS.

**Definition 8** ([29]). $\Sigma$ satisfies
(1) local forward extensibility (LFE) property, if for each $s \in Tr$ of the form $s : [a, b] \rightarrow Q$ ($a < b$) there exists a trajectory $s' : [a, b'] \rightarrow Q$ such that $s' \in Tr$, $s \subseteq s'$ and $b' > b$.

(2) global forward extensibility (GFE) property, if for each trajectory $s$ of the form $s : [a, b] \rightarrow Q$ there is a trajectory $s' : [a, +\infty) \rightarrow Q$ such that $s \subseteq s'$.

**Definition 9 ([29]).** A right dead-end path (in $\Sigma$) is a trajectory $s : [a, b) \rightarrow Q$ ($a, b \in T$, $a < b$) such that there is no $s' : [a, b] \rightarrow Q$, $s' \in Tr$ such that $s \subseteq s'$.

**Definition 10 ([29]).** An escape from a right dead-end path $s : [a, b) \rightarrow Q$ (in $\Sigma$) is a trajectory $s' : [c, d) \rightarrow Q$ ($d \in T \cup \{+\infty\}$) or $s' : [c, d] \rightarrow Q$ ($d \in T$) such that $c \in (a, b)$, $d > b$, and $s(c) = s'(c)$. An escape $s'$ is infinite, if $d = +\infty$.

**Definition 11 ([29]).** A right dead-end path $s : [a, b) \rightarrow Q$ in $\Sigma$ is called strongly escapable, if there exists an infinite escape from $s$.

**Definition 12 ([29]).**

(1) A right extensibility measure is a function $f^+ : \mathbb{R} \times \mathbb{R} \rightarrow \mathbb{R}$ such that $A = \{(x, y) \in T \times T \mid x \le y\} \subseteq \text{dom}(f^+)$, $f(x, y) \ge 0$ for all $(x, y) \in A$, $f^{|_A}$ is strictly decreasing in the first argument and strictly increasing in the second argument, and for each $x \ge 0$, $f^+(x, x) = x$ and $\lim_{y \to +\infty} f^+(x, y) = +\infty$.

(2) A right extensibility measure $f^+$ is called normal, if $f^+$ is continuous on $\{(x, y) \in T \times T \mid x \le y\}$ and there exists a function $\alpha$ of class $K_\infty$ (i.e. the function $\alpha : [0, +\infty) \rightarrow [0, +\infty)$ is continuous, strictly increasing, and $\alpha(0) = 0$, $\lim_{x \to +\infty} \alpha(x) = +\infty$) such that $\alpha(y) < y$ for all $y > 0$ and the function $y \mapsto f^+(\alpha(y), y)$ is of class $K_\infty$.

An example of a right extensibility measure is $f_n^+(x, y) = y + (y - x)^n$ for any $n \in \mathbb{N}$. Let $f^+$ be a right extensibility measure.

**Definition 13 ([29]).** A right dead-end path $s : [a, b) \rightarrow Q$ is called $f^+$-escapable (Fig. 3), if there exists an escape $s' : [c, d] \rightarrow Q$ from $s$ such that $d \ge f^+(c, b)$.

**Lemma 1 ([29]).** $\Sigma$ satisfies GFE if and only if $\Sigma$ satisfies LFE and each right dead-end path is strongly escapable.

**Theorem 2 ([29], About right dead-end path).** Assume that $f^+$ is a normal right extensibility measure and $\Sigma$ satisfies LFE. Then each right dead-end path is strongly escapable if and only if each right dead-end path is $f^+$-escapable.

# 3 Traces on sets of trajectories and labeled NCMS

In the case of labeled transition systems (LTS), labels are some data associated with transitions and traces are sequences of labels along executions of an LTS. We would like to define an analogous notion of a trace for NCMS. The informal idea behind the definition of a trace proposed below is that for continuous-time
<figure><img src="image_5.png" /><figcaption>**Fig. 3.** An $f^+$-escapable right dead-end path $s : [a, b) \to Q$ (curve) and a corresponding escape $s' : [c, d] \to Q$ (a horizontal segment) such that $d \ge f^+(c, b)$.</figcaption></figure>

systems the role of “transitions” play “infinitesimally short trajectories” and “labels” are certain values associated with such trajectories. Thus a trace defines some quantity that evolves in time along a trajectory. This idea of co-evolution of trace and trajectory is formalized in Definition 14 below. Theorem 3 given below shows that this definition implies that at each time moment the value of a trace depends only on the values of the trajectory in vicinity of this time moment supporting the informal ideas of “transitions” and “labels” for NCMS.

**Definition 14 (Trace).** Let $\mathcal{T}r$ be a CPR set of trajectories. A function $\lambda$ on $\mathcal{T}r$ is called a trace on $\mathcal{T}r$, if the following conditions hold:

(1) (Preservation of domain) For each $s \in \mathcal{T}r$, $\lambda(s)$ is a function defined on $\text{dom}(s)$.

(2) (Monotonicity) If $s_1, s_2 \in \mathcal{T}r$ and $s_1 \subseteq s_2$, then $\lambda(s_1) \subseteq \lambda(s_2)$.

We will define a labeled NCMS as a NCMS with a trace on its trajectories.

**Definition 15.** (Labeled NCMS) A labeled NCMS is a pair $(\Sigma, \lambda)$, where $\Sigma = (T, Q, \mathcal{T}r)$ is a NCMS and $\lambda$ is trace on $\mathcal{T}r$.

The most important properties of traces are formulated below.

**Lemma 2 (Image of trace).** The image of a trace on a CPR set of trajectories is a CPR set of trajectories.

**Lemma 3 (Chain-continuity of a trace).** Let $\mathcal{T}r$ be a CPR set of trajectories and $\lambda$ be a trace on $\mathcal{T}r$. Then $\lambda$ is chain-continuous in the following sense: for any non-empty chain $C$ in the poset $(\mathcal{T}r, \subseteq)$ which has the least upper bound $s^* \in \mathcal{T}r$ the set $\{\lambda(s) \mid s \in C\}$ has the least upper bound $\lambda(s^*)$ in the poset $(\{\lambda(s) \mid s \in \mathcal{T}r\}, \subseteq)$.

The following theorem gives a convenient criterion for checking if a function is a trace.
**Theorem 3 (Criterion of a trace).** Let $\mathcal{T}\mathcal{r}$ be a CPR set of trajectories, $Y$ be a set, $\lambda: \mathcal{T}\mathcal{r} \to (T \rightsquigarrow Y)$ be a total function. Then $\lambda$ is a trace on $\mathcal{T}\mathcal{r}$ if and only if the following conditions hold:

(1) $\mathrm{dom}(\lambda(s)) = \mathrm{dom}(s)$ for all $s \in \mathcal{T}\mathcal{r}$;

(2) if $s_1, s_2 \in \mathcal{T}\mathcal{r}, t_0 \in T, s_1 \doteq_{t_0+} s_2$, then $\lambda(s_1)(t_0) = \lambda(s_2)(t_0)$;

(3) if $s_1, s_2 \in \mathcal{T}\mathcal{r}, t_0 \in T, s_1 \doteq_{t_0-} s_2$, then $\lambda(s_1)(t_0) = \lambda(s_2)(t_0)$.

The following lemma gives an obvious example of a trace: pointwise application of a total function on the set of states to a trajectory (projection).

**Lemma 4.** Assume that $\mathcal{T}\mathcal{r}$ is a CPR set of trajectories from $T$ to a set $Q$, $Y$ is a set, $f: Q \to Y$ is a total function, and $\lambda: \mathcal{T}\mathcal{r} \to (T \rightsquigarrow Y)$ is such that $\lambda(s) = f \circ s$ for all $s \in \mathcal{T}\mathcal{r}$. Then $\lambda$ is a trace on $\mathcal{T}\mathcal{r}$.

*Proof.* Follows immediately from Theorem 3. $\square$

However, generally, the value of a trace at time $t$ may depend not only on the value of a trajectory at $t$, but on the values of a trajectory in an arbitrarily small neighborhood of $t$. An example of this kind based on differentiation is given below (informally, this trace measures the speed of change of a trajectory).

*Example 1.* Assume that $n \in \mathbb{N}$, $\mathcal{T}\mathcal{r} \subset T \rightsquigarrow \mathbb{R}^n$ is a CPR set of trajectories and each $s \in \mathcal{T}\mathcal{r}$ is differentiable on $\mathrm{dom}(s) \in \mathcal{T}$, i.e. $s$ is differentiable at each point of the interior of $\mathrm{dom}(s)$, $s$ has the right derivative at the least element of $\mathrm{dom}(s)$, if this element exists, and $s$ has the left derivative at the greatest element of $\mathrm{dom}(s)$, if this element exists.

Let $\lambda: \mathcal{T}\mathcal{r} \to (T \rightsquigarrow \mathbb{R}^n)$ be a function such that for each $s \in \mathcal{T}\mathcal{r}$:

- $\lambda(s)(t) = \frac{d}{dt}s(t)$, if $t$ is in the interior of $\mathrm{dom}(s)$;

- $\lambda(s)(t)$ is the right derivative of $s$ at $t$, if $t$ is the least element of $\mathrm{dom}(s)$;

- $\lambda(s)(t)$ is the left derivative of $s$ at $t$, if $t$ is the greatest element of $\mathrm{dom}(s)$.

Using Theorem 3 it is easy to check that $\lambda$ is a trace on $\mathcal{T}\mathcal{r}$. $\square$

# 4 Timed simulation and bisimulation on NCMS

For any partial function $s$ on $T$ such that $\mathrm{dom}(s) \in \mathcal{T}$, any $t_0 \in T$, and any element $q$ we will write

$q \stackrel{s}{\rightleftharpoons}$, if $\mathrm{dom}(s)$ has the least element $a$ such that $s(a) = q$;

$q \stackrel{s}{\rightleftharpoons}_{t_0}$, if $t_0$ is the least element of $\mathrm{dom}(s)$ and $s(t_0) = q$.

Let $(\Sigma, \lambda)$ be a fixed labeled NCMS, where $\Sigma = (T, Q, \mathcal{T}\mathcal{r})$.

**Definition 16.** Let $s_1, s_2: T \rightsquigarrow Q$ and $R \subseteq Q \times Q$ be a binary relation.

Then the functions $s_1$ and $s_2$ are:

(1) pointwise in $R$, if $\mathrm{dom}(s_1) = \mathrm{dom}(s_2)$ and $(s_1(t), s_2(t)) \in R$ for $t \in \mathrm{dom}(s_1)$;

(2) pointwise in $R$ on a set $A \subseteq T$, if $A \subseteq \mathrm{dom}(s_1) \cap \mathrm{dom}(s_2)$ and $(s_1(t), s_2(t)) \in R$ for all $t \in A$;
(3) pointwise in $R$ in a right neighborhood of $t \in T$, if there exists $t' > t$, such that $s_1, s_2$ are pointwise in $R$ on $[t, t')$;

(4) pointwise in $R$ in a deleted left neighborhood of $t \in T$, if $t > 0$ and there is $t' \in [0, t)$ such that $s_1, s_2$ are pointwise in $R$ on $(t', t)$.

**Definition 17 (Global timed simulation).** A relation $R \subseteq Q \times Q$ is a global timed simulation on $(\Sigma, \lambda)$, if for each $(q_1, q_2) \in R$ and $s_1 \in Tr$ such that $q_1 \stackrel{s_1}{\rightsquigarrow}$ there is $s_2 \in Tr$ such that $q_2 \stackrel{s_2}{\rightsquigarrow}$, $\lambda(s_1) = \lambda(s_2)$, and $s_1, s_2$ are pointwise in $R$.

**Definition 18 (Local timed simulation).** A relation $R \subseteq Q \times Q$ is a local timed simulation on $(\Sigma, \lambda)$, if for each $(q_1, q_2) \in R$, $s_1 \in Tr$, and $t_0 \in T$ such that $q_1 \stackrel{s_1}{\rightsquigarrow} t_0$ there exists $s_2 \in Tr$ such that $q_2 \stackrel{s_2}{\rightsquigarrow} t_0$, $\lambda(s_1) \doteq_{t_0+} \lambda(s_2)$, and $s_1, s_2$ are pointwise in $R$ in a right neighborhood of $t_0$.

**Definition 19 (Timed bisimulation).** A relation $R \subseteq Q \times Q$ is a

(1) local timed bisimulation on $(\Sigma, \lambda)$, if both $R$ and $R^{-1}$ are local timed simulations on $(\Sigma, \lambda)$;

(2) global timed bisimulation on $(\Sigma, \lambda)$, if both $R$ and $R^{-1}$ are global timed simulations on $(\Sigma, \lambda)$.

**Lemma 5.** If $R$ is a global timed simulation on $(\Sigma, \lambda)$, then $R$ is a local timed simulation on $(\Sigma, \lambda)$.

**Lemma 6.** There exists a labeled NCMS $(\Sigma', \lambda')$ and a local timed bisimulation $R_0$ on $(\Sigma', \lambda')$ such that $R_0$ is not a global timed simulation on $(\Sigma', \lambda')$.

**Theorem 4 (About global and local timed bisimulation).**

(1) If $R$ is a global timed bisimulation on $(\Sigma, \lambda)$, then $R$ is a local timed bisimulation on $(\Sigma, \lambda)$.

(2) There is a labeled NCMS $(\Sigma', \lambda')$ and a local timed bisimulation $R_0$ on $(\Sigma', \lambda')$ such that $R_0$ is not a global timed bisimulation on $(\Sigma', \lambda')$.

*Proof.* Follows immediately from Lemma 5, Lemma 6, and Definition 19. $\square$

# 5 Main Result

As before, let $(\Sigma, \lambda)$ be a fixed labeled NCMS, where $\Sigma = (T, Q, Tr)$. Let $f^+$ be a fixed right extensibility measure.

**Definition 20 (f+-timed simulation).** A relation $R \subseteq Q \times Q$ is a f+-timed simulation on $(\Sigma, \lambda)$, if $R$ is a local timed simulation on $(\Sigma, \lambda)$ and for each $s_1, s_2 \in Tr$ and $t_0 \in dom(s_1)$ which satisfy the following conditions:

- $s_1, s_2$ are pointwise in $R$ in a deleted left neighborhood of $t_0$,

- $\lambda(s_1) \doteq_{[t'_0, t_0]} \lambda(s_2)$ for some $t'_0 < t_0$,

there exist $s'_2 \in Tr$, $t_1 \in dom(s_2) \cap dom(s'_2)$, and $t_2 \in T$ such that

(1) $t_1 < t_0$ and $s_2(t_1) = s'_2(t_1)$;

(2) either $t_2 \ge f^+(t_1, t_0)$, or $t_2$ is the maximal element of $dom(s_1)$;

(3) $\lambda(s_1) \doteq_{[t_1, t_2]} \lambda(s'_2)$;

(4) $s_1$ and $s'_2$ are pointwise in $R$ on $[t_1, t_2]$.
**Definition 21 (f$^+$-timed bisimulation).** A relation $R \subseteq Q \times Q$ is a $f^+$-timed bisimulation on $(\Sigma, \lambda)$, if both $R$ and $R^{-1}$ are $f^+$-timed simulations on $(\Sigma, \lambda)$.

The main result of this paper is the following theorem:

**Theorem 5 (Local characterization of global timed bisimulation).** Let $f^+$ be a normal right extensibility measure. A relation $R \subseteq Q \times Q$ is a global timed bisimulation on $(\Sigma, \lambda)$ if and only if $R$ is a $f^+$-timed bisimulation on $(\Sigma, \lambda)$.

This theorem holds for any normal right extensibility measure, for example, $f_1^+(x, y) = y + (y - x) = 2y - x$. The difference between the definition of the $f^+$-timed simulation and global timed simulation is that the latter definition is non-local, i.e. it requires proving the existence of arbitrarily long trajectories $(s_2)$ for proving that $R$ is a simulation which may be hard, if the dynamics of a system is defined by nonlinear differential equations or in other implicit way. The former definition is local in that for proving that $R$ is a simulation one can show the existence of $s_2'$ that satisfies (1)-(4) on an arbitrarily short interval $[t_1, t_2]$ (the condition (2) imposes a lower bound on its length, but e.g. for $f^+ = f_1^+$ this lower bound can be made arbitrarily small by choosing $t_1$ close to $t_0$).

Arguably, the characterization of global timed bisimulation provided by Theorem 5 is non-constructive, because it does not tell how to check the existence of $s_2' \in \mathit{Tr}$, $t_1 \in \mathit{dom}(s_2) \cap \mathit{dom}(s_2')$, and $t_2 \in \mathit{T}$ in Definition 20 (their existence for any $s_1, s_2, t_0$ that satisfy assumptions of this definition is required for proving that a relation is a global timed bisimulation). But this lack of constructivity is, arguably, a consequence of generality of our model of a system (NCMS). So the role of the local characterization provided by Theorem 5 is logical (to give an alternative view of bisimulation in the general case useful e.g. for proving new theorems about bisimulations) instead of being an executable algorithm.

The question of whether Theorem 5 can be a basis of algorithms for checking properties related to bisimulations and bisimilarity for special types dynamical systems (e.g. described by linear systems, etc.) requires separate investigation.

An informal description of how Theorem 5 can be applied is given below.

Let $S$ be a system that travels through the state space $Q = \mathbb{R}^n$ in accordance with a known law of motion $L$ – an ordinary differential equation with input control. The trace of a trajectory is a pointwise application of some output function to the trajectory (in accordance with Lemma 4). $Q$ contains a (possibly infinite) subset $O$ of isolated point obstacles. If $S$ hits an obstacle, its trajectory ends without possibility of continuation. Trajectories which neither hit nor tend to obstacles can be continued indefinitely.

Suppose that we want to prove that under certain assumptions $R = (Q \setminus O) \times (Q \setminus O)$ is a *global* timed bisimulation.

Proof using Definition 17 involves reasoning about the whole set $O$. Under assumptions that are close to functional output-controllability of the system one can prove that $R$ is a *local* bisimulation *without reasoning about obstacles at all*
(see Definition 18). However, this approach is not directly applicable to the case of global timed bisimulation.

For proving that $R$ is a global timed bisimulation one can use $f^+$-timed bisimulation which is equivalent to it. In this case one needs to inspect system behavior *near each obstacle individually*, forgetting about others: take $f^+(x, y) = 2y - x$ and consider Definition 20. The main case is when $s_2$ tends to a some obstacle $X$ as $t \to t_0$ and $s_1$ avoids all obstacles. Definition 20 requires the existence of a control maneuver $s'_2$ that preserves the trace of $s_2$, but not for long after $t_0$ ($t_2 - t_0 \ge t_0 - t_1$ is sufficient). By choosing $t_1$ such that $t_0 - t_1$ is sufficiently small (informally, “last minute collision avoidance”) and taking into account continuity of trajectories of $S$, proving its existence using $L$ does not require reasoning about obstacles from $O$ other than $X$.

# 6 Outline of the proof of the main result

The idea of the proof is to define a family of auxiliary NCMS $\{\Sigma_{s_0,R}(\Sigma, \lambda) \mid s_0 \in Tr\}$ depending on $R$ such that all its members satisfy GFE whenever $R$ is a $f^+$-timed simulation and show that if they satisfy GFE, then $R$ is a global timed simulation on $(\Sigma, \lambda)$. The converse part of the theorem can be proved directly.

We formulate the main steps (milestones) of the proof as a series of lemmas given below (Lemma 7 - Lemma 13). We assume that their statements are self-describing.

**Lemma 7.** Let $f^+$ be a normal right extensibility measure and $R \subseteq Q \times Q$ be a global timed simulation on $(\Sigma, \lambda)$. Then $R$ is a $f^+$-timed simulation on $(\Sigma, \lambda)$.

For each $s_0 \in Tr$ and a relation $R \subseteq Q \times Q$ let us denote:

- $\mathrm{Tr}_{s_0,R}^0(\Sigma, \lambda)$ is the set of all functions $s : T \to Q$ such that $\mathrm{dom}(s) \in \mathcal{T}$ and the following conditions hold:

- $s|_{\mathrm{dom}(s_0)} \in Tr$,

- $\lambda(s|_{\mathrm{dom}(s_0)}) \sqsubseteq \lambda(s_0)$,

- $s_0, s$ are pointwise in $R$ on $\mathrm{dom}(s_0) \cap \mathrm{dom}(s)$.

- $\mathrm{Tr}_{s_0,R}(\Sigma, \lambda) = \{s : T \to Q \mid \mathrm{dom}(s) \in \mathcal{T} \land \exists \hat{s} \in \mathrm{Tr}_{s_0,R}^0(\Sigma, \lambda) \ s \sqsubseteq \hat{s}\}$.

- $\Sigma_{s_0,R}(\Sigma, \lambda) = (T, Q, \mathrm{Tr}_{s_0,R}(\Sigma, \lambda))$.

**Lemma 8.** If $s_0 \in Tr$ and $R \subseteq Q \times Q$, then $\Sigma_{s_0,R}(\Sigma, \lambda)$ is a NCMS.

**Lemma 9.** Let $s_0 \in Tr$ and $R$ be a local timed simulation on $(\Sigma, \lambda)$. Then $\Sigma_{s_0,R}(\Sigma, \lambda)$ is a NCMS which satisfies LFE.

**Lemma 10.** Let $f^+$ be a normal right extensibility measure, $s_0 \in Tr$, and $R$ be a $f^+$-timed simulation on $(\Sigma, \lambda)$. Assume that $s_*$ is a right dead-end path in the NCMS $\Sigma_{s_0,R}(\Sigma, \lambda)$. Then $s_*$ is $f^+$-escapable.

**Lemma 11.** Let $f^+$ be a normal right extensibility measure, $s_0 \in Tr$, and $R$ be a $f^+$-timed simulation on $(\Sigma, \lambda)$. Then $\Sigma_{s_0,R}(\Sigma, \lambda)$ satisfies GFE.
*Proof.* R is a $f^+$-timed simulation on $(\Sigma, \lambda)$, so R is a local timed simulation on $(\Sigma, \lambda)$. Then $\Sigma_{s_0,R}(\Sigma, \lambda)$ is a NCMS which satisfies LFE by Lemma 9. By Lemma 10 each right dead-end path in $\Sigma_{s_0,R}(\Sigma, \lambda)$ is $f^+$-escapable. By Theorem 2 each right dead-end path in $\Sigma_{s_0,R}(\Sigma, \lambda)$ is strongly escapable. Then by Lemma 1 $\Sigma_{s_0,R}(\Sigma, \lambda)$ satisfies GFE. $\square$

**Lemma 12.** Let $R \subseteq Q \times Q$ be a local timed simulation on $(\Sigma, \lambda)$. Assume that for each $s_0 \in Tr$, $\Sigma_{s_0,R}(\Sigma, \lambda)$ is a NCMS which satisfies GFE. Then $R$ is a global timed simulation on $(\Sigma, \lambda)$.

**Lemma 13.** Let $f^+$ be a normal right extensibility measure and $R \subseteq Q \times Q$ be a $f^+$-timed simulation on $(\Sigma, \lambda)$. Then $R$ is a global timed simulation on $(\Sigma, \lambda)$.

*Proof.* By Lemma 11, for each $s_0 \in Tr$, $\Sigma_{s_0,R}(\Sigma, \lambda)$ is a NCMS which satisfies GFE. Because $R$ is a $f^+$-timed simulation on $(\Sigma, \lambda)$, $R$ is a local timed simulation on $(\Sigma, \lambda)$. Then by Lemma 12, $R$ is a global timed simulation on $(\Sigma, \lambda)$. $\square$

*Proof (Proof of Theorem 5).* The “If” part follows from Lemma 13 and the “Only if” part follows from Lemma 7. $\square$

# 7 Conclusions and Future Work

We have obtained a necessary and sufficient condition (criterion) of a local character for checking that a given relation satisfies the definition of a global timed bisimulation for NCMS.

The obtained results can be useful for applying bisimulation proof method to various continuous-time models for establishing equivalence and constructing abstractions of such systems and for further development of uniform treatment of continuous time dynamical system models and proof principles related to them using coalgebraic approach. We plan to develop bisimulation proof method on the basis of the results obtained in this paper and apply it to cyber-physical system verification problems in the forthcoming papers.

# References

1. Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1989)

2. Park, D.: Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-Conference on Theoretical Computer Science, London, UK, Springer-Verlag (1981) 167–183

3. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York, NY, USA (2011)

4. Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst. 31(4) (2009) 15:1–15:41

5. Sangiorgi, D.: On the bisimulation proof method. Mathematical Structures in Comp. Sci. 8(5) (1998) 447–479
6. Shi, J., Wan, J., Yan, H., Suo, H.: A survey of cyber-physical systems. In: Wireless Communications and Signal Processing (WCSP), 2011 International Conference on, IEEE (2011) 1–6

7. Baheti, R., Gill, H.: Cyber-physical systems. The Impact of Control Technology (2011) 161–166

8. Lee, E., Seshia, S.: Introduction to embedded systems: A cyber-physical systems approach. Lulu.com (2013)

9. Sifakis, J.: Rigorous design of cyber-physical systems. In: Embedded Computer Systems (SAMOS), 2012 International Conference on, IEEE (2012) 319–319

10. Bouissou, O., Chapoutot, A.: An operational semantics for Simulink’s simulation engine. In: Proceedings of the 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems, ACM (2012) 129–138

11. Simulink – Simulation and Model-Based Design. http://www.mathworks.com/products/simulink

12. SCADE Suite. http://www.esterel-technologies.com/products/scade-suite

13. Campbell, S., Chancelier, J.P., Nikoukhah, R.: Modeling and Simulation in Scilab/Scicos with ScicosLab 4.4. Springer (2005)

14. Feiler, P., Gluch, D., Hudak, J.: The architecture analysis & design language (AADL): An introduction. Technical Report CMU/SEI-2006-TN-011, Carnegie-Mellon University (2006)

15. Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proceedings of the IEEE 88(7) (2000) 971–984

16. Pappas, G.: Bisimilar linear systems. Automatica 39(12) (2003) 2035–2047

17. van der Schaft, A.: Equivalence of dynamical systems by bisimulation. IEEE Transactions on Automatic Control 49(12) (2004) 2160–2172

18. Schaft van der, A.: Equivalence of hybrid dynamical systems. In: Proceedings of the Sixteenth International Symposium on Mathematical Theory of Networks and Systems, Leuven, Belgium, July 5-9, 2004. (2004)

19. Julius, A., van der Schaft, A.: Bisimulation as congruence in the behavioral setting. In: Proceedings of the 44th IEEE Conference on Decision and Control and the European Control Conference 2005. Seville, Spain, December 12-15, 2005. (2005)

20. Pola, G., Schaft van der, A., Di Benedetto, M.: Equivalence of switching linear systems by bisimulation. International Journal of Control 79(1) (2006) 74–92

21. Schmuck, A., Raisch, J.: Simulation and bisimulation over multiple time scales in a behavioral setting. CoRR abs/1402.3484 (2014)

22. Cuijpers, P.J.L., Reniers, M.A.: Lost in translation: Hybrid-time flows vs. real-time transitions. In: Hybrid Systems: Computation and Control. Springer Science + Business Media (2008) 116–129

23. Polderman, J., Willems, J.: Introduction to mathematical systems theory: a behavioral approach. Springer, Berlin (1997)

24. Haghverdi, E., Tabuada, P., Pappas, G.: Unifying bisimulation relations for discrete and continuous systems. In: Proceedings of the International Symposium MTNS2002, South. (2002)

25. Haghverdi, E., Tabuada, P., Pappas, G.: Bisimulation relations for dynamical, control, and hybrid systems. Theoretical Computer Science 342(2-3) (2005) 229–261

26. Davoren, J., Tabuada, P.: On simulations and bisimulations of general flow systems. In: Hybrid Systems: Computation and Control, 10th International Workshop, HSCC 2007, Pisa, Italy, April 3-5, 2007, Proceedings. (2007) 145–158
27. Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Form. Methods Syst. Des. **18**(1) (2001) 25–68

28. Ivanov, I.: A criterion for existence of global-in-time trajectories of non-deterministic Markovian systems. Communications in Computer and Information Science (CCIS) **347** (2012) 111–130

29. Ivanov, I.: On representations of abstract systems with partial inputs and outputs. In Gopal, T., Agrawal, M., Li, A., Cooper, S., eds.: Theory and Applications of Models of Computation. Volume 8402 of Lecture Notes in Computer Science. Springer International Publishing (2014) 104–123

30. Ivanov, I., Nikitenko, M., Abraham, U.: On a decidable formal theory for abstract continuous-time dynamical systems. Communications in Computer and Information Science (CCIS) **469** (2014) 78–99

31. Ivanov, I.: An abstract block formalism for engineering systems. In: ICTERI. Volume 1000 of CEUR Workshop Proceedings., CEUR-WS.org (2013) 448–463

32. Ivanov, I.: On existence of total input-output pairs of abstract time systems. Communications in Computer and Information Science (CCIS) **412** (2013) 308–331

33. Hájek, O.: Theory of processes, I. Czechoslovak Mathematical Journal **17** (1967) 159–199

34. Hájek, O.: Theory of processes, II. Czechoslovak Mathematical Journal **17**(3) (1967) 372–398

35. Alur, R., Courcoubetis, C., Dill, D.: Model checking in dense real-time. Information and Computation **104** (1993) 2–34

36. Liberzon, D.: Switching in Systems and Control (Systems & Control: Foundations & Applications). Birkhauser Boston Inc. (2003)

37. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical computer science **138**(1) (1995) 3–34

38. Goebel, R., Sanfelice, R.G., Teel, A.: Hybrid dynamical systems. Control Systems, IEEE **29**(2) (2009) 28–93