Multi-timed Bisimulation for Distributed Timed Automata

Abstract

Timed bisimulation is an important technique which can be used for reasoning about behavioral equivalence between different components of a complex real-time system. The verification of timed bisimulation is a difficult and challenging problem because the state explosion caused by both functional and timing constraints must be taken into account. Timed bisimulation was shown decidable for Timed Automata (TA). Distributed TA and TA with Independent Clocks (icTA) were introduced to model Distributed Real-time Systems. They are a variant of TA with local clocks that may not run at the same rate. In this paper, we first propose to extend the theory of Timed Labeled Transition Systems to Multi-Timed Labeled Transition Systems, and relate them by an extension of timed bisimulation to multi-timed bisimulation. We prove the decidability of multi-timed bisimulation and present an EXPTIME algorithm for deciding whether two icTA are multi-timed bisimilar. For multi-timed bisimilarity, an extension of the standard refinement algorithm is described.

1 Introduction

Distributed Real-Time Systems (DTS) are increasing with the scientific and technological advances of computer networks. The high demand for computer networks has caused the development of new complex applications which benefit from the high performance and resources offered by modern telecommunications networks. Current researches in the area of DTS have emerged from the need to specify and analyze the behavior of these systems, where both distributed behavior and timing constraints are present. Formal verification methods, such as model checking, have been used to verify the correctness of complex DTS. Model checking over DTS becomes rapidly intractable because the state space often grows exponentially with the number of components considered. A technique to reduce the state space is to merge states with the same behaviour. For untimed systems, the notion of bisimulation [13] is classically used to this end, and its natural extension for real-time systems, timed bisimulation, was already shown decidable for Timed Automata (TA) [2, 12]. A timed automaton is a finite automaton augmented with real-valued clocks, represented as variables that increase at the same rate as time progresses. TA assume perfect clocks: all clocks have infinite precision and are perfectly synchronized. In this paper, we study two variants of TA called Distributed Timed Automata (DTA) and Timed Automata with Independent Clocks (icTA) proposed by [1, 11, 16] to model DTS, where the clocks are not necessarily synchronized. TA have been used to model DTS such as Controller Area Network [14] and WirelessHART Networks [10]. But, TA, icTA and timed bisimulation are based on a sequential semantics of a Timed Labelled Transition Systems (TLTS), i.e., a run of a TLTS is given by a sequence of actions and timestamps.

Unfortunately, a sequential semantics does not describe completely the behavior of the DTS, because interactions between processes with their associated local clocks that are running at the same rate and distribution of the actions over the components are not considered. Also, model-checking and bisimulation equivalence algorithms have been implemented in tools [19, 20] for the sequential semantics used by the model (e.g., TA, TLTS, etc.). In contrast, behavioral equivalences for DTS have only been introduced in [3]. It is, however, not clear whether such equivalences agree with the distributed timed properties in DTS. Therefore, we propose an alternative semantics to the classical sequential semantics for TLTS and icTA: specifically, a run of a system in our alternative semantics is given by the sequences of pairs (action, tuples of timestamps). We propose an alternative semantics in order to be able to consider a semantics which expresses the distribution of the actions and timestamps over the components. With this alternative, it becomes possible to analyze the local behavior of the components independently, thus enhancing the expressiveness of the TLTS (and icTA). We introduce Multi-Timed Labelled Transition Systems (MLTS), an extension of classical TLTS in order to cope with the notion of multiple local times, and we propose efficient algorithms using refinement techniques [17].

Contributions. One of our main contributions is to incorporate a alternative semantics over sequential semantics for TLTS and icTA. Also, we extend the classical theory of timed bisimulation with the notion multi-timed bisimulation and their corresponding decision algorithms. We also present two algorithms: (i) a forward reachability algorithm for the parallel composition of two icTA, which will help us to minimize the state space exploration by our second algorithm, and (ii) a decision algorithms for multi-timed bisimulation using the zone-based technique [5]. Multi-timed bisimulation is a relation over local clocks (and processes), and cannot be computed with the standard partition refinement algorithm [17]. Instead, our algorithm successively refines a set of zones such that ultimately each zone contains only multi-timed bisimilar pairs of states. Furthermore, we show that our algorithm is EXPTIME-complete. Since TA are a special variant of icTA, our work conservatively extends the expressiveness of TA and TLTS; and since timed bisimulation over TA [19, 20] can be regarded as a special case of multi-timed bisimulation, our decision algorithms could potentially be used to analyze complex DTS.

Structure of the Paper. After recalling preliminary notions in Sect. 2, we introduce our alternative semantics for icTA in Sect. 3, based on multi-timed words consumed by MLTS. Section 4 deals with bisimulation: we first define multi-timed bisimulation, by adapting the classical definition to MLTS, then show its decidability by exhibiting an EXPTIME algorithm. Finally, Sect. 5 compares our work with existing contributions, and Sect. 6 concludes. Due to space constraints, some proofs are not given here, but stay available in a Technical Report available online [15].

2 Preliminaries

We describe in this section the notations needed for formally defining Timed Labelled Transition Systems (TLTS) and Timed Automata TA.

Timed Words. The set of all finite words over a finite alphabet of actions $\varSigma$ is denoted by $\varSigma ^{*}$. Let $\mathbb {N}$, $\mathbb {R}$ and $\mathbb {R}_{\ge 0}$ respectively denote the sets of natural, real and nonnegative real numbers. A timed word [2] over $\varSigma$ is a finite sequence $\theta = ((\sigma _{1}, t_{1}), (\sigma _{2}, t_{2}) \ldots (\sigma _{n}, t_{n}))$ of actions paired with nonnegative real numbers (i.e., $(\sigma _{i}, t_{i}) \in \varSigma \times \mathbb {R}_{\ge 0}$) such that the timestamped sequence $t = t_{1} \cdot t_{2} \cdots t_{n}$ is nondecreasing (i.e., $t_{i} \le t_{i+1}$). We sometimes define $\theta$ as the pair $\theta = (\sigma , t)$ with $\sigma \in \varSigma ^{*}$ and t a sequence of timestamps with the same length.

Clocks. A clock is a real positive variable that increases with time. Let $\textit{X}$ be a finite set of clock names. A clock constraint $\phi \in \varPhi (X)$ is a conjunction of comparisons of a clock with a natural constant c: with $x \in X$, $\textit{c} \in \mathbb {N}$, and $\sim \ \in \ \{<, \ >, \ \le , \ \ge , \ =\}$, $\phi$ is defined by

$$\begin{aligned} \phi \,{::}{=}\,true \ | \ \textit{x} \sim \textit{c} \ | \ \phi _{1} \ \wedge \ \phi _{2} \end{aligned}$$

A clock valuation $\nu \in \mathbb {R}_{\ge 0}^{X}$ over $\textit{X}$ is a mapping $\nu : \textit{X} \rightarrow \mathbb {R}_{\ge 0}$. For a time value $\textit{t} \in \mathbb {R}_{\ge 0}$, we note $\nu + \textit{t}$ the valuation defined by $(\nu + t)(x) = \nu (x) + t$. Given a clock subset $Y \subseteq X$, we note $\nu [Y \rightarrow 0]$ the valuation defined as follows: $\nu [Y \leftarrow 0](x) = 0$ if $x\in Y$ and $\nu [\textit{Y} \leftarrow 0](x) = \nu (x)$ otherwise. The projection of $\nu$ on $\textit{Y}$, written $\nu \rfloor _{\textit{Y}}$, is the valuation over $\textit{Y}$ containing only the values in $\nu$ of clocks in $\textit{Y}$.

Timed Automata (TA). A TA is a tuple $\mathcal {B}= (\varSigma , X, S, s_{0}, \rightarrow _{ta}, I, F)$ where $\varSigma$ is a finite alphabet, X a clock set, S a set of locations with $s_0\in S$ the initial location and $F\subseteq S$ the set of (sink) final states, $\rightarrow _{ta} \subseteq S \times \varSigma \times \varPhi (X) \times 2^{X} \times S$ is the automaton’s transition relation, $I : \textit{S} \rightarrow \varPhi (\textit{X})$ associates to each location a clock constraint as invariant. For a transition $(s,\phi , a , Y, s') \in \rightarrow _{ta}$, we classically write $s \xrightarrow {\phi , a, Y} s'$ and call s and $s'$ the source and target location, $\phi$ is the guard, a the action or label, Y the set of clocks to be reset. During the execution of a TA $\mathcal {B}$, a state is a pair $(s, \nu )\in S\times \mathbb {R}_{\ge 0}^{X}$, where s denotes the current state with its accompanying clock valuation $\nu$, starting at $s_0, \nu _0$ where $\nu _0$ maps each clock to 0. We only consider legal states, i.e. states that satisfy $\nu \vDash \textit{I}(s)$ (i.e. valuations that map clocks to values that satisfy the current state’s invariant).

Timed Transition System ( ). The transition system TLTS $(\mathcal {B})$ generated by $\mathcal {B}$ is defined by TLTS $(\mathcal {B}) = (Q, q_0, \varSigma , \rightarrow _{tlts})$, where Q is a set of legal states over $\mathcal {B}$ with initial state $q_0 = (s_0, \nu _0)$, $\varSigma$ a finite alphabet and $\rightarrow _{tlts}$ $\subseteq$ $\textit{Q} \times (\varSigma \uplus \mathbb {R}_{\ge 0}) \times \textit{Q}$ is the TLTS transition relation defined by: (a) Delay transition: $(s, \nu ) \xrightarrow {t} (s, \nu + t)$ for some $t \in \mathbb {R}_{\ge 0}$, iff $\nu + t$ $\vDash$ $\textit{I}(s)$, (b) Discrete transition: $(s, \nu ) \xrightarrow {a} (s', \nu ')$, iff $\textit{s} \xrightarrow {\phi , a, Y} \textit{s}'$, $\nu \vDash \phi$, $\nu ' \vDash \nu [Y \rightarrow 0]$ and $\nu ' \vDash \textit{I}(s')$.

3 An Alternative Semantics for DTA

In this section, we define an alternative semantics (which we will call multi-timed semantics) for icTA as opposed to the mono-timed semantics of [1]. The main problem with the semantics of [1] is that they use the reference time. The benefits of this new definition are threefold. First, the multi-timed semantics preserves the untimed language of the icTA. Second, the multi-timed semantics can work with multi-timed words. Third, the region equivalence defined in [1] could form a finite time-abstract bisimulation on the multi-timed semantics. Hence, the multi-timed semantics allows to build a region automaton that accepts exactly Untime $(\mathcal {L}(\mathcal {A}))$ for all icTA $\mathcal {A}$ [1]. Thus, we extend TLTS and icTA to their multi-timed version.

3.1 Multi-timed Actions

Let Proc be a non-empty set of processes, then, we denote by $\mathbb {R}_{\ge 0}^{Proc}$ the set of functions from Proc to $\mathbb {R}$, that we call tuples. A tuple $\varvec{d} \in \mathbb {R}_{\ge 0}^{Proc}$ is smaller that $\varvec{d}'$, noted, $\varvec{d} < \varvec{d}'$ iff $\forall i \in Proc\ \varvec{d}_{i} \le \varvec{d}_{i}'$ and $\exists i \in Proc\ \varvec{d}_{i} < \varvec{d}_{i}'$. A Monotone Sequence of Tuples (MST) is a sequence $\varvec{d}$ = $\varvec{d}_1 \varvec{d}_2 \cdots \varvec{d}_{n}$ of tuples of $\mathbb {R}_{\ge 0}^{Proc}$ where: $\forall$ $j \in 1 \cdots n-1$, $\varvec{d}_{j} \le \varvec{d}_{j+1}$. A multi-timed word on $\varSigma$ is a pair $\theta = (\sigma , \varvec{d})$ where $\sigma = \sigma _{1}\sigma _{2} \ldots \sigma _{n}$ is a finite word $\sigma \in \varSigma ^{*}$, and $\varvec{d} = \varvec{d}_{1} \varvec{d}_{2}\ldots \varvec{d}_{n}$ is a MST of the same length. This is the analog of a timed word (or multi-timed action) [2]. A multi-timed word can equivalently be seen as a sequence of pairs in $\varSigma \times \mathbb {R}_{\ge 0}^{Proc}$.

3.2 Multi-timed Labeled Transition Systems

Our multi-timed semantics is defined in terms of runs that record the state and clock values at each transition points traversed during the consumption of a multi-timed word. Instead of observing actions at a global time, a multi-timed word allows to synchronise processes on a common action that may occur at a specific process time.

Definition 1

(Multi-timed Labelled Transition System). A Multi-Timed Labelled Transition System (MLTS) over a set of processes Proc is a tuple $\mathcal {M} = (\textit{Q},\textit{q}_{0}, \varSigma , \rightarrow _{mlts})$ such that: (i) $\textit{Q}$ is a set of states. (ii) $\textit{q}_{0} \in \textit{Q}$ is the initial state. (iii) $\varSigma$ is a finite alphabet. (v) $\rightarrow _{mlts} \subseteq \textit{Q} \times (\varSigma \uplus \mathbb {R}_{\ge 0}^{Proc}) \times \textit{Q}$ is a set of transitions.

The transitions from state to state of a MLTS are noted in the following way: (i) A transition $(q, a, q')$ is denoted $\textit{q} \xrightarrow {a} \textit{q}'$ and is called a $\textit{discrete transition}$, if a $\in$ $\varSigma$ and $(q, a, q')\,\in \,\rightarrow _{mlts}$, (ii) A transition $(q, \varvec{d}, q')$ is denoted $\textit{q} \xrightarrow {\varvec{d}} \textit{q}'$ and is called a $\textit{delay transition}$, if $\varvec{d} \in \mathbb {R}_{\ge 0}^{Proc}$ and $(q, \varvec{d}, q')\,\in \,\rightarrow _{mlts}$.

A run of $\mathcal {M}$ can be defined as a finite sequence of moves, where discrete and continuous transitions alternate: $\rho$ = $q_0 \xrightarrow {\varvec{d}_1} q_0' \xrightarrow {\textit{a}_1} q_1 \xrightarrow {\varvec{d}_2} q_1' \xrightarrow {\textit{a}_2} q_2 \ldots q_{n-1} \xrightarrow {\varvec{d}_{n-1}} q_{n-1}' \xrightarrow {\textit{a}_{n-1}} q_{n}$, where $\forall {0 \le i \le n-1}, q_{i} \in Q, \forall j \le n-1, \varvec{d}_{j} \in \mathbb {R}_{\ge 0}^{Proc}, q_{j}' \in \textit{Q}$ and $a_{j} \in \varSigma$. The multi-timed word of $\rho$ is $\theta = ((a_{1}, {\varvec{t}_{1}}), (a_{2}, {\varvec{t}_{2}}) \ldots , (a_{n}, {\varvec{t}_{n}}))$, where ${\varvec{t}_{i}} = \sum _{j=1}^{i} {\varvec{d}_{j}}$. A multi-timed word $\theta$ is accepted by $\mathcal {M}$ iff there is a maximal initial run whose multi-timed word is $\theta$. The language of $\mathcal {M}$, denoted $\mathcal {L}(\mathcal {M})$, is defined as the set of multi-timed words accepted by some run of $\mathcal {M}$. Note that MLTS are a proper generalisation of TLTS: each TLTS can be seen as a MLTS with a single process and conversely.

For example, consider the two transition systems in Fig. 1: a MLTS on the left ($\mathcal {M}_1$) and two TLTS on the right ($\mathcal {M}_2$ and $\mathcal {M}_3$) with the finite input alphabet $\varSigma = \{a, b, c\}$. In brief, $\mathcal {M}_2$ and $\mathcal {M}_3$ could be considered as the projection of $\mathcal {M}_1$ on the case of process 1 and 2.

Fig. 1.

Multi-timed and Timed Labelled Transition Systems

3.3 A Multi-timed Semantics for icTA

DTA [1, 11] consist of a number of local timed automata. In [1], DTA are not much studied. Instead, their product is first computed, giving rise to the class of icTA ($\mathcal {A} = (\mathcal {B}, \pi )$, where $\mathcal {B}$ is a TA and $\pi$ is a function maps each clock to a process).

Given $\pi : X \rightarrow \textit{Proc}$, a clock valuation and $\varvec{d}$ $\in$ $\mathbb {R}_{\ge 0}^{Proc}$: the valuation $\nu +_{\pi } \varvec{d}$ is defined by $(\nu +_{\pi } \varvec{d})(x)$ = $\nu (x) + \varvec{d}_{\pi (x)}$ for all $x \in X$. A Rate is a tuple $\tau$ = $(\tau _{\textit{q}})_{\textit{q} \in \textit{Proc}}$ of local time functions. Each local time function $\tau _{\textit{q}}$ maps the reference time to the time of process $\textit{q}$, i.e., ${\tau }_{\textit{q}}: \mathbb {R}_{\ge 0} \xrightarrow {} \mathbb {R}_{\ge 0}$. The functions $\mathcal {\tau }_{\textit{q}}$ must be continuous, strictly increasing, divergent, and satisfy $\tau _q(0) = 0$. The set of all these tuples $\tau$ is denoted by $Rates$.

The operational semantics of an icTA has been associated to a sequential semantics. A run of an icTA $\mathcal {A}$ for $\tau \in Rates$ with a sequential semantics as a sequence $(s_1, \nu _1) \xrightarrow {t_1, a_1}$ $(s_2, \nu _2) \xrightarrow { t_2, a_2} (s_2, \nu _3)$ $\ldots (s_{n-1}, \nu _{n-1})$ $\xrightarrow { t_{n-1}, a_{n-1}} (s_n, \nu _n)$ where $\forall 1 \le i \le n$, $s_{i} \in \textit{S}$ and $\forall j \le n-1$, $t_{j} \in \mathbb {R}_{\ge 0}$ and $a_{j} \in \varSigma$. Here, we want to associate operational semantics of a icTA to a MLTS.

Definition 2

Let $\mathcal {A}$ be an icTA and $\tau \in Rates$. Our multi-timed semantics of the icTA $\mathcal {A}$ is given by a MLTS over $\textit{Proc}$, denoted by MLTS($\mathcal {A}, \tau ) = (\textit{Q},\textit{q}_{0},\varSigma ,\rightarrow _{mlts}$). The set of states Q consists of triples composed of a location, a clock valuation and lastly the reference time: $\textit{Q} = \{(\textit{s}, \nu , t) \in \textit{S} \times \mathbb {R}_{\ge 0}^{\textit{X}} \times \mathbb {R}_{\ge 0} \ | \ \nu \,\models \,\textit{I}(\textit{s})\}$. The starting state is $q_0 = (\textit{s}_{0}, \nu _0, 0)$, where $\nu _0$ is the valuation that assigns 0 to all the clocks. $\varSigma$ is the alphabet of $\mathcal {A}$. The transition relation $\rightarrow _{mlts}$ is defined by:

• (i) A transition $(q_i, {\varvec{d}}, q_{i}')$ is denoted $q_{i} \xrightarrow {\varvec{d}} q_{i}'$, and is called a $\textit{delay transition}$, where $q_{i} = (\textit{s}_{i}, \nu _{i}, t_{i})$, $q_{i}' = (\textit{s}_{i}, \nu _{i} +_{\pi } \varvec{d}, t_{i+1})$, $\varvec{d} = \tau (t_{i+1}) - \tau (t_{i})$ and $\forall t \in [t_{i}, t_{i+1}]: \nu _{i} +_{\pi } (\tau (\textit{t}) - \tau (\textit{t}_{i}))\,\models \,\textit{I}(\textit{s}_{i})$.

• (ii) A transition $(q_{i}, \textit{a}, q_{i+1})$ is denoted $q_{i} \xrightarrow {\textit{a}} q_{i+1}$, and is called a $\textit{discrete}$ $\textit{transition}$, where $q_{i} = (\textit{s}_{i}, \nu _{i}, t_{i})$, $q_{i+1} = (\textit{s}_{i+1}, \nu _{i+1}, t_{i+1})$, $a \in \varSigma$, there exists a transition $(s_{i}, a, \phi , Y, s_{i+1}) \in \,\rightarrow _{\textsf {ic}}$, such that $\nu _{i}\,\models \,\phi$, $\nu _{i+1}$ = $\nu _{i} [Y \rightarrow 0]$, $\nu _{i+1}\,\models \,I(s_{i+1})$, $t_{i} = t_{i+1}$.

In Definition 2, we have introduced a multi-timed semantics for icTA, following ideas of [1]. A run of an icTA $\mathcal {A}$ for $\tau$ $\in$ Rates with our multi-timed semantics is an initial path in MLTS $(\mathcal {A}, \tau )$ where discrete and continuous transition alternate. A multi-timed word is accepted by $\mathcal {A}$ for $\tau \in Rates$ iff it is accepted by MLTS $(\mathcal {A}, \tau )$.

Example 1

The Fig. 2(a) shows an icTA $\mathcal {M}$ with the finite input alphabet $\varSigma = \{a,b,c,d\}$, the set of processes Proc = $\{p, q\}$, the set of clocks $\textit{X} = \{x^{p}, y^{q}\}$ and $\tau$ = (2t, t) i.e. $\tau _{p}(t)$ = 2t and $\tau _{q}(t)$ = t. A run of $\mathcal {M}$ on multi-timed word $\theta$ = ((a, (2.0, 1.0))(b, (3.0, 1.5))(c, (4.2, 2.1)) (d, (6.0, 3.0))) is given by $\rho$ $(S_{0}, [x^{p} = 0.0, y^{q} = 0.0], 0.0)$ $(S_{0}, [x^{p} = 2.0, y^{q} = 1.0], 1.0)$ $(S_{1}, [x^{p} = 2.0, y^{q} = 0.0 ], 1.0)$ $(S_{1}, [x^{p} = 3.0, y^{q} = 1.5], 1.5)$ $(S_{2}, [x^{p} = 3.0, y^{q} = 1.5], 1.5)$ $(S_{2}, [x^{p} = 4.2, y^{q} = 1.1], 2.1)$ $(S_{1}, [x^{p} = 4.2, y^{q} = 0.0], 2.1)$ $(S_{1}, [x^{p} = 6.0, y^{q} = 0.9], 3.0)$ $(S_{0}, [x^{p} = 0.0, y^{q} = 0.9], 3.0)$.

Fig. 2.

(a) An icTA $\mathcal {M}$, (b) An counter example of Multi-timed bisimulation

4 Multi-timed Bisimulation

From a distributed approach, a DTS consist of several processes with their associated local clocks that are not running at the same rate. Thus, in order to formalize preservation of distributed timed behavior, we extend the classical definition of timed bisimulation [9] towards a multi-timed semantics. Our motivation for extending the classical definition of timed bisimulation is twofold: first, efficient algorithms checking for timed and time-abstract bisimulation have been discovered [12, 19]. Nonetheless, these algorithms are based on sequential semantics (i.e., TLTS and TA). Second, verifying the preservation of distributed timed behavior in DTS could be used to master the combinatorial explosion of the size of the model due to the composition of the processes.

4.1 Strong Multi-timed Bisimulation

Let $\mathcal {M}_{1}$ and $\mathcal {M}_{2}$ be two MLTS over the same set of actions $\varSigma$ and processes Proc. Let $Q_{\mathcal {M}_{1}}$ (resp., $Q_{\mathcal {M}_{2}}$) be the set of states of $\mathcal {M}_{1}$ (resp., $\mathcal {M}_{2}$). Let $\mathcal {R}$ be a binary relation over $\textit{Q}_{\mathcal {M}_{1}} \times \textit{Q}_{\mathcal {M}_{2}}$. We say that $\mathcal {R}$ is a strong multi-timed bisimulation whenever the following transfer property holds (note that technically this is simply strong bisimulation over $\varSigma \uplus \mathbb {R}^{Proc}_{\ge 0}$):

Definition 3

A strong multi-timed bisimulation over MLTS $\mathcal {M}_{1}$, $\mathcal {M}_{2}$ is a binary relation $\mathcal {R} \subseteq Q_{\mathcal {M}_{1}} \times Q_{\mathcal {M}_{2}}$ such that, for all $\textit{q}_{\mathcal {M}_{1}} \mathcal {R} \textit{q}_{\mathcal {M}_{2}}$, the following holds:

• (i) For every $a \in \varSigma$ and for every discrete transition $\textit{q}_{\mathcal {M}_{1}}$ $\textit{q}_{\mathcal {M}_{1}}'$, there exists a matching discrete transition $\textit{q}_{\mathcal {M}_{2}}$ $\textit{q}_{\mathcal {M}_{2}}'$ such that $\textit{q}_{\mathcal {M}_{1}}' \mathcal {R} \textit{q}_{\mathcal {M}_{2}}'$ and symmetrically.

• (ii) For every $\varvec{d} = (d_1, \ldots , d_n)$ $\in$ $\mathbb {R}_{\ge 0}^{Proc}$, for every delay transition $\textit{q}_{\mathcal {M}_{1}}$ $\textit{q}_{\mathcal {M}_{1}}'$, there exists a matching delay transition $\textit{q}_{\mathcal {M}_{2}}$ $\textit{q}_{\mathcal {M}_{2}}'$ such that $\textit{q}_{\mathcal {M}_{1}}' \mathcal {R} \textit{q}_{\mathcal {M}_{2}}'$ and symmetrically.

Two states $\textit{q}_{\mathcal {M}_{1}}$ and $\textit{q}_{\mathcal {M}_{2}}$ are multi-timed bisimilar, written $\textit{q}_{\mathcal {M}_{1}} \approx \textit{q}_{\mathcal {M}_{2}}$, iff there is a multi-timed bisimulation that relates them. $\mathcal {M}_{1}$ and $\mathcal {M}_{2}$ are multi-timed bisimilar, written $\mathcal {M}_{1}$ $\approx$ $\mathcal {M}_{2}$, if there exists a multi-timed bisimulation relation $\mathcal {R}$ over $\mathcal {M}_{1}$ and $\mathcal {M}_{2}$ containing the pair of initial states.

As a consequence of Definition 3, the notion of multi-timed bisimulation extends to icTA and we have the following definition:

Definition 4

Let $\mathcal {A}$ and $\mathcal {B}$ be two icTA. We say the automata $\mathcal {A}$ and $\mathcal {B}$ are multi-timed bisimilar, denoted $\mathcal {A}$ $\approx$ $\mathcal {B}$, iff $\forall$ $\tau$ $\in$ Rates MLTS($\mathcal {A}, \tau$) $\approx$ MLTS($\mathcal {B}, \tau$).

When there is only one process, the multi-timed bisimulation is the usual timed bisimulation. Consider the two icTA $\mathcal {A}_{p}$ (top) and $\mathcal {A}_{q}$ (bottom) in Fig. 2(b) with the alphabet $\varSigma = \{a\}$, the set of processes Proc = $\{p, q\}$, the set of clocks $\textit{X} = \{x^{p}, y^{q}\}$ and $\tau$ = $(t^{2}, 3t)$ i.e. $\tau _{p}(t)$ = $t^{2}$ and $\tau _{q}(t)$ = 3t. $\mathcal {A}_{p}$ and $\mathcal {A}_{q}$ in Fig. 2(b) depicts an icTA. $\mathcal {A}_{p}$ performs nondeterministically the transition with the guard $x^{p} \le 2$, the action a, resets clock $x^{p}$ to 0 and enters location $s_{1}$. Similarly, $\mathcal {A}_{q}$ performs nondeterministically the transitions with the guard $y^{q} \le 2$, the action a, resets clock $y^{q}$ to 0 and enters location $t_{1}$. We will show that these icTA are not multi-timed bisimilar (Definition 3) ever if their underling TA are bisimilar (and ever isomorphic): We have $(S_{0}, [x^{p} = 0], 0)$ in $\textsf {MLTS}(\mathcal {A}_{p}, \tau _{p})$ and $(T_{0}, [y^{q} = 0], 0)$ since $\mathcal {A}_{p}$ can run the delay transition $(S_{0}, [x^{p} = 0], 0)$ $(S_{0}, [x^{p} = 1.0], 1)$ and $\mathcal {A}_{q}$ in $\textsf {MLTS}(\mathcal {A}_{q}, \tau _{q})$. We have $(S_{0}, [x^{p} = 0], 0)$ $\not \approx$ $(T_{0}, [y^{q} = 0], 0)$ can only match this transition with $(T_{0}, [y^{q} = 0], 0)$ $(T_{0}, [y^{q} = 3], 1)$. From these states $\textsf {MLTS}(\mathcal {A}_{p}, \tau _{p})$ can fire a while $\textsf {MLTS}(\mathcal {A}_{q}, \tau _{q})$ cannot.

4.2 Decidability

Inspired by [12], we show that for given icTA $\mathcal {A}$, $\mathcal {B}$, checking whether $\mathcal {A}$ $\approx$ $\mathcal {B}$ is decidable via a suitable zone graph [12]. In order to define the notion of clock zone over a set of clocks $\textit{X}$, we need to consider the set $\varPhi ^{+}(\textit{X})$ of extended clock constraints.

Definition 5

A clock constraint $\phi$ is a conjunction of comparisons of a clock with a constant c, given by the following grammar, where $\phi$ ranges over $\varPhi ^{+}(\textit{X})$, $\textit{x}_{i}, \textit{x}_{j} \in \textit{X}$, $\textit{c} \in \mathbb {N}$, and $\sim \ \in \ \{<, \ >, \ \le , \ \ge , \ =\}$:

$$\begin{aligned} \phi \,{::}{=}\,true \ | \ \textit{x}_{i} \sim \textit{c} \ | \ \textit{x}_{i} - \textit{x}_{j} \sim \textit{c} \ | \ \phi _{1} \ \wedge \ \phi _{2}. \end{aligned}$$

A clock constraint of the form $\textit{x}_{i} - \textit{x}_{j} \sim \textit{c}$ is called diagonal constraint and $\textit{x}_{i}$, $\textit{x}_{j}$ must belong to the same process. The notion of satisfaction of a clock constraint $\phi$ $\in$ $\varPhi ^{+}(\textit{X})$ by a valuation is given by the clause $\nu$ $\models$ $x_{i} - x_{j}$ $\sim$ c iff $\nu (x_{i}) - \nu (x_{j})$ $\sim$ c.

Informally, a clock zone $\mathcal {Z}$ is a conjunction of extended clock constraints $\phi \in \varPhi ^{+}(\textit{X})$ with inequalities of clock differences and its semantics is the set of clock valuations that satisfy it $[\![\mathcal {Z}]\!]$ = $\{\nu \ \vert \ \nu \,\models \,\phi \}$. We omit the semantics brackets ($[\![\mathcal {Z}]\!]$) when obvious. For any clock zones $\mathcal {Z}$, $\mathcal {Z}'$ and finite set of clocks X, the semantics of the intersection, clock reset, inverse clock reset, time successor and time predecessor events on clock zone can be defined as: (i) $\mathcal {Z} \cap \mathcal {Z}' = \{\nu \ | \ \nu \ \in \ \mathcal {Z} \ \wedge \ \nu \ \in \ \mathcal {Z}' \}$, (ii) $\mathcal {Z}\downarrow _{X} = \{\nu [X \rightarrow 0] \ | \ \nu \ \in \ \mathcal {Z} \ \}$, (iii) $\mathcal {Z}\uparrow _{X} = \{\nu \ | \ \nu [X \rightarrow 0] \ \in \ \mathcal {Z} \ \}$, (iv) $\mathcal {Z}\uparrow = \{\nu +_{\pi } \varvec{d} \ | \ \nu \ \in \ \mathcal {Z} \ and \ \varvec{d} \ \in \ \mathbb {R}_{> 0}^{Proc} \}$, (v) $\mathcal {Z}\downarrow = \{\nu -_{\pi } \varvec{d} \ | \ \nu \ \in \ \mathcal {Z} \ and \ \varvec{d} \ \in \ \mathbb {R}_{> 0}^{Proc} \}$.

A zone graph [12] is similar to a region graph [2] with the difference that each node consists of pair (called a zone) of a location s and a clock zone $\mathcal {Z}$ $(i.e., \ q = (s, \mathcal {Z}))$. For $q = (s, \mathcal {Z})$, we write $(s', \nu )$ $\in$ q if $s = s'$ and $\nu \in \mathcal {Z}$, indicating that a state is included in a zone. Analogously, we can write $(s, \mathcal {Z}) \subseteq (s', \mathcal {Z}')$ to indicate that $s = s'$ and $\mathcal {Z}$ $\subseteq$ $\mathcal {Z}'$. We will use the notation $\textsf {Action}(e)$ to denote the action a of the edge e. Furthermore, we extend the zone operations for an icTA $\mathcal {A}$ in the following way:

Definition 6

Let $q=(s, \mathcal {Z})$ be a zone and $e=(s, a, \phi , Y, s')$ $\in$ $\rightarrow _{icta}$ be a transition of $\mathcal {A}$, then $\textsf {post}(\mathcal {Z},e)$=$\{\nu '| \exists \nu \in \mathcal {Z}, \exists \tau \in Rates, \exists t \in \mathbb {R}_{\ge 0}, (s,\nu ,t) \xrightarrow {e}_{mlts(\mathcal {A},\tau )} (s', \nu ', t)\}$ is the set of valuations that q can reach by taking the transition e.

Definition 7

Let $q=(s, \mathcal {Z}')$ be a zone and $e=(s, a, \phi , Y, s')$ $\in$ $\rightarrow _{icta}$ be a transition of $\mathcal {A}$, then $\textsf {pred}(\mathcal {Z}', e)$=$\{\nu |\exists \nu ' \in \mathcal {Z}', \exists \tau \in Rates, \exists t \in \mathbb {R}_{\ge 0}, (s, \nu , t) \xrightarrow {e}_{mlts(\mathcal {A}, \tau )} (s', \nu ', t)\}$ is the set of valuations that q can reach by executing the transition e.

Intuitively, the zone $(s', \textsf {post}(\mathcal {Z}, e))$ describes the discrete successor of the zone $(s, \mathcal {Z})$ under the transition e, and the zone $(s, \textsf {pred}(\mathcal {Z}', e))$ describes the discrete predecessor of the zone $(s', \mathcal {Z}')$ under the transition e.

Definition 8

(Multi-timed Zone Graph). Given an icTA $\mathcal {A} = (\varSigma , \textit{X}, \textit{S}, \textit{s}_{0},$ $\rightarrow _{\textit{icta}}, \textit{I}, \textit{F}, \pi )$, its symbolic multi-timed zone graph (ZG($\mathcal {A}$)) is a transition system ZG($\mathcal {A}$) = $(Q, q_{0}, (\varSigma \cup \{\uparrow \}), \rightarrow _{\textsf {ZG}})$, where: (i) Q consists of pairs $q = (s, \mathcal {Z})$ where s $\in$ $\textit{S}$, and $\mathcal {Z}$ $\in$ $\varPhi ^{+}(X)$ is a clock zone with $\mathcal {Z} \subseteq I(s)$. (ii) $q_{0} \in Q$ is the initial zone $q_{0} = (s_{0}, \mathcal {Z}_{0})$ with $\mathcal {Z}_{0}$ = $\llbracket \bigwedge _{x \in \textit{X}} x = 0\rrbracket$. (iii) $\varSigma$ is the set of labels of $\mathcal {A}$. (iv) $\rightarrow _{\textsf {ZG}}$ $\subseteq$ $\textit{Q} \times (\rightarrow _{icta} \cup \{\uparrow \} ) \times \textit{Q}$ is a set of transitions, where each transition in ZG($\mathcal {A}$) is a labelled by a transition $e = (s, a, \phi , Y, s')$ $\in$ $\rightarrow _{\textit{icta}}$, where s and $s'$ are the source and target locations, $\phi$ is a clock constraint defining the guard of the transition, a is the action of the edge and Y is the set of clocks to be reset by the transition in the icTA $\mathcal {A}$. For each $e \in \varSigma$, transitions are defined by the rules:

• (i) For every e = $(s, a, \phi , Y, s')$ and clock zone $\mathcal {Z}$, there exists a discrete transition $(q, e, q')$, where $q = (s, \mathcal {Z}) \xrightarrow {e}_{\textsf {ZG}} q'= (s', \textsf {post}(\mathcal {Z}, e))$ if $\textsf {post}(\mathcal {Z}, e)$ $\ne$ $\emptyset$.

• (ii) For a clock zone $\mathcal {Z}$, there exists a delay transition $(q, \uparrow , q')$, where $q = (s, \mathcal {Z}) \xrightarrow {\uparrow }_{\textsf {ZG}} q' = (s, \mathcal {Z}')$ and $\mathcal {Z}' = \mathcal {Z} \uparrow \cap$ I(s).

Note that $\uparrow$ is used here as a symbol to represent symbolic positive delay transitions. Only the reachable part is constructed.

Lemma 1

Let $(s, \mathcal {Z})$ be a zone and $e = (s, a, \phi , Y, s') \in \rightarrow _{icta}$ be a transition of an icTA $\mathcal {A}$, then $\mathcal {Z}\uparrow$, $\mathcal {Z}\uparrow _{x}$, $\mathcal {Z}\downarrow$, $\textsf {post}(\mathcal {Z}, e)$ and $\textsf {pred}(\mathcal {Z}', e)$ are also zones.

Multi-timed Zone Graph Algorithm: In Algorithm 1, we build a reachable multi-timed zone graph (ZG($\mathcal {A}$ $\parallel$ $\mathcal {B}$)) for the parallel composition of two icTA ($\mathcal {A}$ and $\mathcal {B}$). Algorithm 1 build a multi-timed zone graph, starting with the pair $(s_{0}, \mathcal {Z}_{0})$ ($s_{0}$ initial location of the automaton $\mathcal {A}$ with $\mathcal {Z}_{0}$ = ${\llbracket }\bigwedge _{x \in \textit{X}} x = 0\rrbracket$ represents the initial zone). However, the multi-timed zone graph can be infinite, because constants used in zones may grow for ever. Therefore, we use a technique called extrapolation abstraction ($Extra_{LU_{(s)}}^{+}$ (LU-bound)) [4, 7], where L is the maximal lower bound and U is the maximal upper bounds. For every location s of a ZG($\mathcal {A}$), there are bound functions LU and the symbolic zone graph using $Extra_{LU_{(s)}}^{+}$. Then, we build zones of the form $q_{\textsf {ZG}} = (s, Extra_{LU_{(s)}}^{+}(\textsf {post}(\mathcal {Z}, e))$.

Lemma 2

(Completeness). Let $\theta$ = $(s_0, \nu _0, t_0) \xrightarrow {\varvec{d}_0, a_0}$ $(s_1, \nu _1, t_1) \xrightarrow {\varvec{d}_1, a_1}$ $\ldots$ $\xrightarrow {\varvec{d}_{n-1}, a_{n-1}}$ $(s_n, \nu _n, t_n)$ be a run of $\textsf {MLTS}(\mathcal {A}, \tau )$, for some $\tau$ $\in$ Rates. Then, for any state $(s_i, \nu _i, t_i)$ where $0 \le i \le n$, there exists a symbolic zone $(s_i, \mathcal {Z}_i)$ added in Q such that $\nu _i$ $\in$ $\mathcal {Z}_{i}$.

The above lemma tells that the Algorithm 1 over-approximates reachability. Now, we can establish the termination of the Algorithm 1, because there are finitely many $Extra_{LU_{(s)}}^{+}$ zones. Here, we will use Algorithm 1 to over-approximate the co-reachable state space of the two icTA $\mathcal {A}$ and $\mathcal {B}$, on the strongly synchronized product of $\mathcal {A}$ and $\mathcal {B}$. The time complexity of this algorithm is given in terms of the number of clocks, the number of clocks and the number of transitions of the icTA: $O(|S| \times |\rightarrow _{\textsf {icTA}}| \times |X|^{2}))$ where |S| represent the number of states in the icTA $\mathcal {A}$, |X| the number of clocks in $\mathcal {A}$ and $|\rightarrow _{\textsf {icTA}}|$ the number of transitions in $\mathcal {A}$.

Refinement Algorithm: Now, we describe a refinement algorithm with signature to compute the multi-timed bisimulation from their zone graph of their strong product ZG(ZG($\mathcal {A}$ $\parallel$ $\mathcal {B}$)). The passage of arbitrary local times are abstracted by time elapse $\uparrow$ transitions from a zone to successor zones, and discrete transitions. Essentially, our algorithm is based on the refinement technique [6, 17, 19]. The state space Q of ZG($\mathcal {A}$ $\parallel$ $\mathcal {B}$) is divided in zones that initially over-approximate the co-reachable states of $\mathcal {A}$ and $\mathcal {B}$. Algorithm 2 starts from an initial set of zones $\varPi _{0}$ and successively refines these sets such that ultimately each zone contains only bisimilar state pairs.

The runs of a zone graph involve a sequence of moves with discrete and time-elapse $\uparrow$ transitions. The refinement algorithm has thus to deal with the following difficulties: when taking a $\uparrow$ transition, where the clocks in different processes are not perfectly synchronous, it should take into consideration that the time elapse traverses continuously diagonal, almost vertical and horizontal time successor zones. Conversely, when the clocks belonging to the same process (i.e., perfectly synchronous), the time elapsing traverses only continuously diagonal time successor zones. Thus, the time refinement operator presented in [19] is not applicable within our Algorithm 2. Figure 3 presents an example: (a) a time elapsing traversing the clock regions 1 to 3 for synchronous clocks, (b) a time elapsing traversing continuously diagonal, almost horizontal and vertical time successor zones for asynchronous clocks.

Fig. 3.

(a) A time elapsing traversing 0 to 3, (b) Multi-timed time successors.

The discrete refinement operator presented in [19] is also not applicable within our Algorithm 2. Therefore, our algorithm adopts the idea of the signature-based technique [6], which assigns states to equivalence blocks according to a characterizing signature. In each refinement iteration, the set of zones are refined according to a signature. The algorithm in [6], cannot be applied in our setting in a straightforward way, due to its untimed characteristic, while in our case, the time and discrete characteristics should be considered. Based on [6], we introduce a signature refinement operator which refine the set of zones until a fixed point is reached, which is the complete multi-timed bisimulation. Thus, we introduce the timed and discrete predecessor operators.

Definition 9

Let q = $(s, \mathcal {Z})$ and $q'$ = $(s, \mathcal {Z}')$ be two zones, then: $\textsf {TimePred}_{\uparrow }(\mathcal {Z},$ $\mathcal {Z}')$ = $\{\nu \in \mathcal {Z} \ | \ \exists \ \varvec{d} \in \mathbb {R}_{> 0}^{Proc}, \ \exists \ \tau \in Rates, \ \exists \ t, t'' \ge 0, \ t \le t'' \ and \ \forall t', t \le t' \le t'', \ and \ \varvec{d} = \tau (t'') - \tau (t), \ (\nu +_{\pi } \varvec{d}) \in \ \mathcal {Z}', \ and \ \varvec{d}' = \tau (t') - \tau (t) \ then \ (\nu +_{\pi } \varvec{d}') \in \ (\mathcal {Z} \cup \mathcal {Z}') \}$ is the set of valuations in the zone $\mathcal {Z}$ from which a valuation of $\mathcal {Z}'$ can be reached through the elapsing of time, without entering any other zones besides $\mathcal {Z}$ and $\mathcal {Z}'$ (i.e., $\mathcal {Z} \cup \mathcal {Z}'$).

The $\textsf {TimePred}_{\uparrow }(\mathcal {Z}, \mathcal {Z}')$ operator refines $\mathcal {Z}$ selecting the states that can reach $\mathcal {Z}'$.

Lemma 3

Let $q = (s, \mathcal {Z})$, $q' = (s, \mathcal {Z}')$ $\in$ Q be two zones, then $\textsf {TimePred}_{\uparrow }$ $(\mathcal {Z}, \mathcal {Z}')$ is a clock zone.

We use as signature of a state $(s, \nu )$ the set of outgoing transitions from $(s', \nu ')$. Then, a refinement of a zone can be computed by grouping states that have the same signature. The resulting set of zones then represents the multi-timed bisimulation relation: two states $(s, \nu )$ and $(s', \nu ')$ are multi-timed bisimilar iff they are in the same zone with similar outgoing transitions. Formally, this is captured in the following definition:

Definition 10

Let q = $(s, \mathcal {Z})$ be a zone, then the signature of a state $(s, \nu )$ $\in$ q formed by the set of labels of all the edges starting from $(s, \nu )$ is defined as:

$\textsf {ActionSigPred}_{q}(s, \nu )$ = $\{(Action(e)) \ | \ \exists \mathcal {Z}', \ \exists \ \nu ' \in \mathcal {Z}', \ (s, \nu ) \xrightarrow {Action(e)}_{icTA} (s', \nu ') \}$. Also, the signature of the zone q is defined as: $\textsf {ActionSig}(q)$ = $\bigcup _{(s,\nu ) \in q}$ $\textsf {ActionSigPred}_{q}(s, \nu )$.

$\textsf {ActionSigPred}_{q}(s, \nu )$ operator is used to compute the signatures of a state into a zone. Our Algorithm 2 consists of two steps: The initial phase, is responsible for keeping a pair of states in q into zones so that every pair of states $(i.e., ((s_{\mathcal {A}}, s_{\mathcal {B}}),$ $(\nu _{\mathcal {A}}, \nu _{\mathcal {B}})) )$ from the same zone q have the same signature $\textsf {ActionSigPred}_{q}(s_{\mathcal {A}}, \nu _{\mathcal {A}})$ $=$ $\textsf {ActionSigPred}_{q}(s_{\mathcal {B}}, \nu _{\mathcal {B}})$. The refinement phase, consists of computing the timed predecessors (see Definition 11 below) and the discrete signature predecessors (see Definition 12 below) until a stable set of zones is reached. Stable zone are a multi-timed bisimulation relation if every pair of states of every zone in the set have the same signature with respect to every computed refinement. A detailed explication about building a stable zones follows:

• Initial phase: Let $\varPi _{0}$ = Q be the initial set of zones, where Q is given by Algorithm 1. After the initial phase, the set $\varPi$ contains zones consisting of states with unique signatures, $\textsf {ActionSigPred}_{q}(s_{\mathcal {A}}, \nu _{\mathcal {A}})$ $=$ $\textsf {ActionSigPred}_{q}(s_{\mathcal {B}}, \nu _{\mathcal {B}})$.

• Refinement phase: An existing set of zones are iteratively refined until all zones becomes stable simultaneously with respect to all their timed predecessors and discrete predecessors. For simplicity, we will write $(s, \mathcal {Z})$ to denote the pairs $((s_{\mathcal {A}},s_{\mathcal {B}}), \mathcal {Z})$.

Definition 11

Let $\varPi$ be a set of zones and q = $(s, \mathcal {Z})$, $q'$ = $(s', \mathcal {Z}')$ be two zones in $\varPi$. Then for the delay transitions, the refinement function is defined as follows:

$\textsf {TimeRefine}(\mathcal {Z}, \varPi )$ = $\{ \textsf {TimePred}_{\uparrow }(\mathcal {Z}, \mathcal {Z}') \ | \ \mathcal {Z}' \in \varPi , q \xrightarrow {\uparrow }_{\varPi } q' \}.$

Definition 12

Let $\varPi$ be a set of zones and q = $(s, \mathcal {Z})$, $q'$ = $(s', \mathcal {Z}')$ be two zones in $\varPi$. Let q = $(s, \mathcal {Z})$ be the currently examined zone and $\textsf {ActionSig}(q)$ be the signatures of the set of states into the zone q. Let $e_{\mathcal {A}}$ and $e_{\mathcal {B}}$ be the transitions of the icTAs $\mathcal {A}$ and $\mathcal {B}$. Then the refinement of a zone q is defined as follows:

$\textsf {DiscreteSigRefine}(\mathcal {Z}, \varPi ) = \bigcap _{a \in \textsf {ActionSig}(q)} \! ((\bigcap _{\{e_{\mathcal {A}} | \textsf {Action}(e_\mathcal {A}) = a\}} \bigcup _{\{e_{\mathcal {B}} | \textsf {Action}(e_\mathcal {B}) = a\}} \textsf {pred}(\mathcal {Z}', (e_{\mathcal {A}}, e_{\mathcal {B}}))) \cap (\bigcap _{\{e_{\mathcal {B}} \ | \ \textsf {Action}(e_\mathcal {B}) = a\}} \ \bigcup _{\{e_{\mathcal {A}} \ | \ \textsf {Action}(e_\mathcal {A}) = a\}} \textsf {pred}(\mathcal {Z}', (e_{\mathcal {A}}, e_{\mathcal {B}})))).$

Lemma 4

Let $(s, \mathcal {Z})$ be a class of $\varPi$ and let e be an edge of the $\textsf {ZG}(\mathcal {C})$, then each of $\textsf {TimeRefine}(\mathcal {Z}, \varPi )$ and $\textsf {DiscreteSigRefine}(\mathcal {Z}, \varPi )$ forms a partition of $\mathcal {Z}$ in zones.

The correctness of the Algorithm 2 follows from the algorithm in [6, 17]. The definition $\textsf {TimeRefine}(\mathcal {Z}, \varPi )$ above to generate a finer set of zones, which deals with delay transitions. The definition of $\textsf {DiscreteSigRefine}(\mathcal {Z}, \varPi )$, generate also a finer set of zones and distinguishes the states with discrete transitions. Termination is ensured by Lemma 4. Algorithm 2 describes the main steps of the decision procedure for multi-timed bisimulation checking. It is based on the function BuildSymbZoneGraph (i.e., Algorithm 1). The function PartitionZoneGraph returns stable set of zones $\varPi$. Given a set of zones $\varPi$, the Algorithm 2 computes the states $((s_{\mathcal {A}}, s_{\mathcal {B}}), \mathcal {Z})$ from $\varPi$ that are bisimilar up to the desired initial state $((s_{\mathcal {A}}^{0}, s_{\mathcal {B}}^{0}), \mathcal {Z}_0)$.

Proposition 1

Let q = $(s, \mathcal {Z})$ be a zone. Let $(s_{\mathcal {A}}, \nu _{\mathcal {A}})$ and $(s_{\mathcal {B}}, \nu _{\mathcal {B}})$ be two states in q, then $(s_{\mathcal {A}}, \nu _{\mathcal {A}})$ $\approx$ $(s_{\mathcal {B}}, \nu _{\mathcal {B}})$ iff $((s_{\mathcal {A}}, s_{\mathcal {B}}), \nu _{\mathcal {A}} \cup \nu _{\mathcal {B}})$ $\in$ $\mathcal {Z}$.

Theorem 1

Deciding multi-timed bisimulation between two icTA is EXPTIME-complete.

An example of the zone graph, partition and multi-timed bisimulation computed by our algorithms can be found in Fig. 4. The Fig. 4(a) shows two icTA $\mathcal {A}$ and $\mathcal {B}$ with the finite input alphabet $\varSigma = \{a,b\}$, the set of processes Proc = $\{p, q\}$, the set of clocks $\textit{X} = \{x^{p}, y^{q}\}$ and $\tau _{p}$ > $\tau _{q}$. The Fig. 4(b) shows the zone graph computed by Algorithm 1. The Fig. 4(c) shows the multi-timed bisimulation for $\mathcal {A}$ and $\mathcal {B}$.

Fig. 4.

(a) Composition of icTAs; (b) Zone graph; (c) bisimulation

5 Related Work

Because TA are a general-purpose formalism, several implementations and extensions have been considered. For example, Puri [18] studied the semantics of robustness timed automata where clocks can drift in a bounded way, i.e. clocks may grow at independent rates in the interval $1 \pm \epsilon$. Krishnan [11] considered asynchronous distributed timed automata, where clocks evolve independently in each component. Akshay et al. concentrate on the untimed language of DTA. In a previous work [16], we suggested a model that has the same expressive power as event clock automata [2], but without studied possible simulation algorithms.

The notion of bisimulation for TA is studied in various contributions [4, 8, 9, 19, 20]. Cerans [9] gives a proof of decidability for timed bisimulation. Several techniques are used in the literature for providing algorithms capable of checking (bi-)simulation: Weise and Lenzkes [20] rely on a zone-based algorithm for weak bisimulation over TA, but no implementation is provided; Bulychev et al. [8] study timed simulation for simulation-checking games, for which an implementation is available from [4]; region construction for timed bisimulation was also considered by Akshay et al. [1], but never implemented; and more closely to our work, Tripakis and Yovine proposed a time-abstract bisimulation over TA in [19]. Krishnan [11] and our previous work [16] manipulated clock drifts as well for manipulating DTA, but without considering bisimulation.

6 Conclusions

Bisimulation is a common technique to reduce the state space explosion issue encountered during model-checking of real-time systems. To enable the application of this technique for DTS modelled by icTA, we proposed an alternative semantics for capturing the execution of icTA, based on multi-timed words running over Multi-Timed Labelled Transition Systems. We extended the notion of bisimulation to such structures, and proposed an EXPTIME algorithm for checking decidability. We are now studying how to efficiently implement such structures and decidability algorithm, and plan to compare their performance against classical work as proposed in [4, 19].