# Equivalence Checking and Intersection of Deterministic Timed Finite State
Machines

Davide Bresolin  Dipartimento di Matematica, University of Padova, Italy.
<EMAIL_ADDRESS>Khaled El-Fakih  American University of Sharjah,
Sharjah, United Arab Emirates<EMAIL_ADDRESS>Tiziano Villa  Dipartimento di
Informatica, University of Verona, Italy<EMAIL_ADDRESS>Nina
Yevtushenko  Ivannikov Institute for System Programming of the Russian Academy
of Sciences & National Research University, Higher School of Economics,
Moscow, Russia<EMAIL_ADDRESS>
###### Abstract

There has been a growing interest in defining models of automata enriched with
time, such as finite automata extended with clocks (timed automata). In this
paper, we study deterministic timed finite state machines (TFSMs), i.e.,
finite state machines with a single clock, timed guards and timeouts which
transduce timed input words into timed output words. We solve the problem of
equivalence checking by defining a bisimulation from timed FSMs to untimed
ones and viceversa. Moreover, we apply these bisimulation relations to build
the intersection of two timed finite state machines by untiming them,
intersecting them and transforming back to the timed intersection.

##  1 Introduction

Finite automata (FA) and finite state machines (FSMs) are formal models widely
used in the practice of engineering and science, e.g., in application domains
ranging from sequential circuits, communication protocols, embedded and
reactive systems, to biological modelling.

Since the 90s, the standard classes of FA have been enriched with the
introduction of time constraints to represent more accurately the behaviour of
systems in discrete or continuous time. Timed automata (TA) are such an
example: they are finite automata augmented with a number of resettable real-
time clocks, whose transitions are triggered by predicates involving clock
values [3].

More recently, timed models of FSMs (TFSMs) have been proposed in the
literature by the introduction of time constraints such as timed guards or
timeouts. Timed guards restrict the input/output transitions to happen within
given time intervals. The meaning of timeouts is the following: if no input is
applied at a current state for some timeout period, the timed FSM moves from
the current state to another state using a timeout function; e.g., timeouts
are common in telecommunication protocols and systems.

For instance, the timed FSM proposed in [25, 18, 19] features: one clock
variable, time constraints to limit the time elapsed at a state, and a clock
reset when a transition is executed. Instead, the timed FSM proposed in [32,
27] features: one clock variable, time constraints to limit the time elapsed
when an output has to be produced after an input has been applied to the FSM,
a clock reset when an output is produced, and timeouts.

In [12] the following models of deterministic TFSMs with a single clock were
investigated: TFSMs with only timed guards, TFSMs with only timeouts, and
TFSMs with both timed guards and timeouts.

TFSM with timed guards and timeoutsTFSM with timeoutsTFSM with timed
guardsLoop-free TFSM with timeoutsTFSM with LCRO timed guardsUntimed FSM
Figure 1: Comparison of TFSM models.

The problem of equivalence checking was solved for all three models, their
expressive power compared, and subclasses of TFSMs with timeouts and with
timed guards equivalent to each other were characterized (see Fig. 1 from [12]
for a diagram showing the expressivity hierarchy of TFSMs with timed guards
and timeouts, TFSMs with only timed guards, TFSMs with only timeouts, loop-
free TFSMs with timeouts, TFSMs with LCRO - Left Closed Right Open - timed
guards, and finally untimed FSMs). Equivalence checking was obtained by
introducing relations of bisimulation that define untimed finite state
machines whose states include information on the clock regions, such that the
timed behaviours of two timed FSMs are equivalent if and only if the
behaviours of the companion untimed FSMs are equivalent. This operation is
reminiscent and stronger than the region graph construction for timed automata
[3].

Here we work directly with deterministic TFSMs with both timed guards and
timeouts, since they subsume the previous two models. For such TFSMs, we give
the detailed construction of the untimed FSM from a timed FSM (what we get is
the _FSM abstraction_ of the TFSM), and then we provide the complete proof
that we can describe the behavior of a TFSM using the corresponding untimed
FSM, i.e., that two deterministic TFSMs are equivalent if and only if their
timed-abstracted FSMs are equivalent.

Then we study the conditions under which the opposite transformation is
possible: we take an untimed deterministic FSM that accepts and produces words
from input and output alphabets (both including a special symbol that
simulates the passing of time), and we build an equivalent deterministic TFSM
with timeouts and timed guards, under the same notion of abstraction of timed
words. This is the key technical result of this paper.

Finally, we apply the previous transformations to perform the intersection of
two deterministic TFSMs, as an example of composition operator under which
TFSMs are closed. We prove how the transformation from TFSMs to untimed FSMs
of Section 2 and the transformation from untimed FSMs to TFSMs of Section 3
can be used to construct the intersection of two TFSMs.

We outline the structure of the paper. Sec. 2 introduces deterministic timed
finite state machines with timed guards and timeouts, describes the untiming
procedure to obtain a finite state machine and proves the bisimulation with
the original timed one, from which an equivalence checking procedure follows.
This is a revision of the material in [12], whereas the following sections are
completely new. Sec. 3 describes the backward transformation from untimed FSMs
to TFSMs and proves the backward bisimulation relation. The two results are
used in Sec. 4 to compute the TFSM that is the intersection of two given
deterministic TFSMs. Sec. 5 relates TFSMs to timed automata, and surveys
expressiveness and complexity results of various models of timed automata,
with final conclusions drawn in Sec. 6.

##  2 Models of Timed FSMs (TFSMs)

Let $A$ be a finite alphabet, and let $\mathbb{R}^{+}$ be the set of non-
negative reals. A _timed symbol_ is a pair $(a,t)$ where $t\in\mathbb{R}^{+}$
is called the _timestamp_ of the symbol $a\in A$. A timed word is then defined
as a finite sequence $(a_{1},t_{1})(a_{2},t_{2})(a_{3},t_{3})\dots$ of timed
symbols where the sequence of timestamps $t_{1}\leq t_{2}\leq t_{3}\leq\dots$
is increasing. Timestamps represent the _absolute times_ at which symbols are
received or produced. In the following we will sometime also reason in terms
of _relative times_ , or _delays_ , measured as the difference between the
timestamps of two successive symbols. More formally, the delay of a symbol
$a_{i}$ is defined as $t_{i}-t_{i-1}$ when $i>1$ and as $t_{1}$ when $i=1$.

The timed models considered in this paper are initialized input/output
machines that operate by reading a _timed input word_
$(i_{1},t_{1})(i_{2},t_{2})\dots(i_{k},t_{k})$ defined on some _input alphabet
$I$_, and producing a corresponding _timed output word_ $(o_{1},t_{1})$
$(o_{2},t_{2})\dots(o_{k},t_{k})$ on some _output alphabet $O$_. The
production of outputs is assumed to be instantaneous: the timestamp of the
$j$-th output $o_{j}$ is the same of the $j$-th input $i_{j}$. Models where
there is a delay between reading an input and producing the related output are
possible but not considered here. Given a timed word
$(a_{1},t_{1})(a_{2},t_{2})\dots(a_{k},t_{k})$,
$\operatorname{Untime}((a_{1},t_{1})(a_{2},t_{2})\dots(a_{k},t_{k}))=a_{1}a_{2}\dots
a_{k}$ denotes the word obtained when deleting the timestamps.

A timed possibly non-deterministic and partial FSM (TFSM) is an FSM augmented
with a clock. The clock is a real number that measures the time delay at a
state, and its value is reset to zero when a transition is executed. In this
section we introduce the TFSM model with both timed guards and timeouts
defined in [12]. Such a model subsumes the TFSM model with timed guards only
given in [18, 25] and the TFSM model with timeouts only given in [32, 43]. In
addition, we establish a very precise connection between timed and untimed
FSMs, showing that it is possible to describe the behavior of a TFSM using a
standard FSM that is called the _FSM abstraction_ of the TFSM.

A timed guard defines the time interval when a transition can be executed.
Intuitively, a TFSM in the present state $s$ accepts an input $i$ at a time
$t$ only if $t$ satisfies the timed guard of some transition labelled with
input symbol $i$. The transition defines the output $o$ to be produced and the
next state $s^{\prime}$. A timeout instead defines for how long the TFSM can
wait for an input in the present state before spontaneously moving to another
state. Each state of the machine has a timeout (possibly $\infty$) and all
outgoing transitions of the state have timed guards with upper bounds less
than the state timeout. The clock is reset to 0 every time the TFSM activates
a transition or a timeout expires.

######  Definition 1 (Timed FSM).

A timed FSM $M$ is a finite state machine augmented with timed guards and
timeouts. Formally, a timed FSM (TFSM) is a 6-tuple
$(S,I,O,\lambda_{S},s_{0},$ $\Delta_{S})$ where $S$, $I$, and $O$ are finite
disjoint non-empty sets of states, inputs and outputs, respectively, $s_{0}$
is the initial state, $\lambda_{S}\subseteq
S\times\left(I\times\Pi\right)\times O\times S$ is a transition relation where
$\Pi$ is the set of input timed guards, and $\Delta_{S}:S\rightarrow
S\times\left(N\cup\left\\{\infty\right\\}\right)$ is a timeout function. Each
guard in $\Pi$ is an interval $g=\langle t_{min},t_{max}\rangle$ where
$t_{min}$ is a nonnegative integer, while $t_{max}$ is either a nonnegative
integer or $\infty$, $t_{min}\leq t_{max}$, and
$\langle\in\big{\\{}(,[\big{\\}}$ while $\rangle\in\big{\\{}),]\big{\\}}$.

The _timed state_ of a TFSM is a pair $(s,x)$ such that $s\in S$ is a state of
$M$ and $x\in\mathbb{R}^{+}$ is the current value of the clock, with the
additional constraint that $x<\Delta_{S}(s)_{\downarrow\mathbb{N}}$ (the value
of the clock cannot exceed the timeout). If no input is applied at a current
state $s$ before the timeout $\Delta_{S}\left(s\right)_{\downarrow\mathbb{N}}$
expires, then the TFSM will move to anther state
$\Delta_{S}\left(s\right)_{\downarrow S}$ as prescribed by the timeout
function. If $\Delta_{S}\left(s\right)_{\downarrow\mathbb{N}}=\infty$, then
the TFSM can stay at state $s$ infinitely long waiting for an input. An
input/output transition can be triggered only if the value of the clock is
inside the guard $\langle t_{min},t_{max}\rangle$ labeling the transition.
_Transitions_ between timed states can be of two types:

  * •

_timed transitions_ of the form $(s,x)\xrightarrow{t}(s^{\prime},x^{\prime})$
where $t\in\mathbb{R}^{+}$, representing the fact that a delay of $t$ time
units has elapsed without receiving any input. The relation $\xrightarrow{t}$
is the smallest relation closed under the following properties:

    * –

for every timed state $(s,x)$ and delay $t\geq 0$, if
$x+t<\Delta_{S}(s)_{\downarrow\mathbb{N}}$, then
$(s,x)\xrightarrow{t}(s,x+t)$;

    * –

for every timed state $(s,x)$ and delay $t\geq 0$, if
$x+t=\Delta_{S}(s)_{\downarrow\mathbb{N}}$, then
$(s,x)\xrightarrow{t}(s^{\prime},0)$ with
$s^{\prime}=\Delta_{S}(s)_{\downarrow S}$;

    * –

if $(s,x)\xrightarrow{t_{1}}(s^{\prime},x^{\prime})$ and
$(s^{\prime},x^{\prime})\xrightarrow{t_{2}}(s^{\prime\prime},x^{\prime\prime})$
then $(s,x)\xrightarrow{t_{1}+t_{2}}(s^{\prime\prime},x^{\prime\prime})$.

  * •

_input/output transitions_ of the form $(s,x)\xrightarrow{i,o}(s^{\prime},0)$,
representing reception of the input symbol $i\in I$, production of the output
$o\in O$ and reset of the clock. An input/output transition can be activated
only if there exists $(s,i,\langle
t_{min},t_{max}\rangle,o,s^{\prime})\in\lambda_{S}$ such that $x\in\langle
t_{min},t_{max}\rangle$.

A _timed run_ of a TFSM $M$ interleaves timed transitions with input/output
transitions. Given a timed input word $v=(i_{1},t_{1})(i_{2},t_{2})\dots$
$(i_{k},t_{k})$, a timed run of $M$ over $v$ is a finite sequence
$\rho=(s_{0},0)\xrightarrow{t_{1}}(s_{0}^{\prime},x_{0})\xrightarrow{i_{1},o_{1}}(s_{1},0)\xrightarrow{t_{2}-t_{1}}(s_{1}^{\prime},x_{1})\xrightarrow{i_{2},o_{2}}(s_{2},0)\xrightarrow{t_{3}-t_{2}}\dots\xrightarrow{i_{k},o_{k}}(s_{k},0)$
such that $s_{0}$ is the initial state of $M$, and for every $j\geq 0$
$(s_{j},0)\xrightarrow{t_{j+1}-t_{j}}(s_{j}^{\prime},x_{j})\xrightarrow{i_{j+1},o_{j+1}}(s_{j+1},0)$
is a valid sequence of transitions of $M$. The timed run $\rho$ is said to
_accept_ the timed input word $v=(i_{1},t_{1})(i_{2},t_{2})\dots(i_{k},t_{k})$
and to _produce_ the timed output word
$u=(o_{1},t_{1})(o_{2},t_{2})\dots(o_{k},t_{k})$. The behavior of $M$ is
defined in terms of the input/output words accepted and produced by the
machine.

The usual definitions for FSMs of deterministic and non-deterministic,
submachine, etc., can be extended to the timed FSM model considered here. In
particular, a TFSM is complete if for each state $s$, input $i$ and value of
the clock $x$ there exists at least one transition
$(s,x)\xrightarrow{i,o}(s^{\prime},0)$, otherwise the machine is partial. A
TFSM is _deterministic_ if for each state $s$, input $i$ and value of the
clock $x$ there exists at most one input/output transition, otherwise is non-
deterministic.

For the sake of simplicity, from now on we consider only _deterministic_
machines (possibly partial), leaving the treatment of non-deterministic TFSMs
to future work.

######  Definition 2.

The behavior of a deterministic TFSM $M$ is a partial mapping
$B_{M}:(I\times\mathbb{R})^{*}\mapsto(O\times\mathbb{R})^{*}$ that associates
every input word $w=(i_{1},t_{1})(i_{2},t_{2})\dots(i_{k},t_{k})$ accepted by
$M$ with the unique output word
$B_{M}(w)=(o_{1},t_{1})(o_{2},t_{2})\dots(o_{k},t_{k})$ produced by $M$ under
input $w$, if it exists. When $M$ is an untimed FSM the behavior is defined as
a partial mapping $B_{M}:I^{*}\mapsto O^{*}$.

Two machines $M$ and $M^{\prime}$ with the same input and output alphabets are
_equivalent_ if and only if they have same behavior, i.e,
$B_{M}=B_{M^{\prime}}$.

So for a partial and deterministic TFSM $M$, we have that for every input word
$w$, $B_{M}(w)$ is either not defined or a singleton set. Moreover, we can
consider the transition relation of the machine as a partial function
$\lambda_{S}:S\times I\times\mathbb{R}^{+}\mapsto S\times O$ that takes as
input the current state $s$, the delay $t$ and the input symbol $i$ and
produces the (unique) next state and output symbol
$\lambda_{S}(s,t,i)=(s^{\prime},o)$ such that
$(s,0)\xrightarrow{t}(s^{\prime},t^{\prime})\xrightarrow{i,o}(s^{\prime\prime},0)$.
With a slight abuse of the notation, we can extend it to a partial function
$\lambda_{S}:S\times(I\times\mathbb{R}^{+})^{*}\mapsto S\times O^{*}$ that
takes as inputs the initial state $s$ and a timed word $w$, and returns the
state reached by the machine after reading $w$ and the generated output word.
We will use $s\xrightarrow{w,u}s^{\prime}$ as a shorthand for
$\lambda_{S}(s,w)=(s^{\prime},u)$.

#### Abstracting TFSMs with timeouts and timed guards.

In this section we show how to build an abstract untimed FSM that describes
the behaviour of a TFSM with guards. To do this we define an appropriate
notion of abstraction of a timed word into an untimed word and a notion of
bisimulation to compare a TFSM with guards with untimed FSM. From the
properties of the bisimulation relation, we conclude that the behaviour of the
abstract untimed FSM is the abstraction of the behaviour of the TFSM.

For every $N\geq 0$, we define $\mathbb{I}_{N}$ as the set of intervals
$\mathbb{I}_{N}=\\{[n,n]\mid n\leq N\\}\cup\\{(n,n+1)\mid 0\leq
n<N\\}\cup\\{(N,\infty)\\}.$ Given a TFSM $M$, we define $\max(M)$ as the
maximum between the greatest timeout value of the function $\Delta_{S}$
(different from $\infty$) and the greatest integer constant (different from
$\infty$) appearing in the guards of $\lambda_{S}$. The set $\mathbb{I}_{N}$
defines a discretization of the clock values of TFSMs. The following lemma
proves that such a discretization is correct, namely, that a TFSM cannot
distinguish between two timed states where the discrete state is the same and
the values of the clocks are in the same interval of $\mathbb{I}_{N}$.

######  Lemma 1.

Let $M=(S,I,O,\lambda_{S},s_{0},\Delta_{S})$ be a deterministic TFSM,
$N=\max(M)$, and let $(s,x)$ and $(s,x^{\prime})$ be two timed states of $M$
such that $x,x^{\prime}\in\langle n,n^{\prime}\rangle$ for some interval
$\langle n,n^{\prime}\rangle\in\mathbb{I}_{N}$. Then
$\lambda_{S}(s,x,i)=\lambda_{S}(s,x^{\prime},i)$ for every input symbol $i\in
I$.

###### Proof.

Suppose by contradiction that there exist two timed states $(s,x)$ and
$(s,x^{\prime})$ such that $x,x^{\prime}\in\langle n,n^{\prime}\rangle$ for
some $\langle n,n^{\prime}\rangle\in\mathbb{I}_{N}$ and
$\lambda_{S}(s,x,i)\neq\lambda_{S}(s,x^{\prime},i)$. Since $x\neq x^{\prime}$
we have that the interval $\langle n,n^{\prime}\rangle$ must be an open
interval of the form $(n,n+1)$ (it cannot be a point interval $[n,n]$) with
$n=\lfloor x\rfloor=\lfloor x^{\prime}\rfloor$ and $n+1=\lceil x\rceil=\lceil
x^{\prime}\rceil$. Suppose, without loss of generality, that
$\lambda_{S}(s,x,i)$ is defined and equal to $(s^{\prime},o)$. By the
definition of TFSM we have that there exists a transition $(s,i,\langle
t_{min},t_{max}\rangle,o,s^{\prime})\in\lambda_{S}$ such that $x\in\langle
t_{min},t_{max}\rangle$. Since $t_{min},t_{max}$ are nonnegative integers (or
$\infty$), it is easy to see that $(n,n+1)\subseteq\langle
t_{min},t_{max}\rangle$. Hence, $x^{\prime}\in\langle t_{min},t_{max}\rangle$
and thus $\lambda_{S}(s,x^{\prime},i)=(s^{\prime},o)=\lambda_{S}(s,x,i)$, in
contradiction with the hypothesis that
$\lambda_{S}(s,x,i)\neq\lambda_{S}(s,x^{\prime},i)$. ∎

We can exploit the discretization given by $\mathbb{I}_{N}$ to build the
abstract FSM as follows. States of the abstract FSM will be pairs $(s,\langle
n,n^{\prime}\rangle)$ where $s$ is a state of $M$ and $\langle
n,n^{\prime}\rangle$ is either a point-interval $[n,n]$ or an open interval
$(n,n+1)$ from the set $\mathbb{I}_{N}$ defined above, where $N=\max(M)$.
Transitions can be either standard input/output transitions labelled with
pairs from $I\times O$ or “time elapsing” transitions labelled with the
special pair $(\mathbbmss{t},\mathbbmss{t})$, which intuitively represents a
time delay $0<t^{*}<1$ without inputs.

######  Definition 3.

Given a TFSM with timeouts and timed guards
$M=(S,I,O,\lambda_{S},s_{0},\Delta_{S})$, let $N=\max(M)$. We define the
_$\mathbbmss{t}$ -abstract FSM_
$A_{M}=(S\times\mathbb{I}_{N},I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{A},(s_{0},[0,0]))$
as the untimed FSM such that:

  * •

$(s,[n,n])\xrightarrow{\mathbbmss{t},\mathbbmss{t}}(s,(n,n+1))$ if and only if
$n+1\leq\Delta_{S}(s)_{\downarrow\mathbb{N}}$;

  * •

$(s,(n,n+1))\xrightarrow{\mathbbmss{t},\mathbbmss{t}}(s,[n+1,n+1])$ if and
only if $n+1<\Delta_{S}(s)_{\downarrow\mathbb{N}}$;

  * •

$(s,(n,n+1))\xrightarrow{\mathbbmss{t},\mathbbmss{t}}(s^{\prime},[0,0])$ if
and only if $\Delta_{S}(s)=(s^{\prime},n+1)$;

  * •

$(s,[N,N])\xrightarrow{\mathbbmss{t},\mathbbmss{t}}(s,(N,\infty))$ and
$(s,(N,\infty))\xrightarrow{\mathbbmss{t},\mathbbmss{t}}(s,(N,\infty))$ if and
only if $\Delta_{S}(s)_{\downarrow\mathbb{N}}=\infty$;

  * •

$(s,\langle n,n^{\prime}\rangle)\xrightarrow{i,o}(s^{\prime},[0,0])$ if and
only if there exists $(s,i,\langle
t,t^{\prime}\rangle,o,s^{\prime})\in\lambda_{S}$ such that $\langle
n,n^{\prime}\rangle\subseteq\langle t,t^{\prime}\rangle$.

$s_{0}$$s_{1}$$[0,1):i/o_{1}$$t=1$$(1,\infty):i/o_{1}$$[0,1]:i/o_{2}$ (a) TFSM
with timeouts and timed guards $M$

$s_{0}$ $[0,0]$ $s_{0}$ $(0,1)$ $s_{1}$ $[0,0]$ $s_{1}$ $(0,1)$ $s_{1}$
$[1,1]$ $s_{1}$ $(1,\infty)$
$i/o_{1}$$\mathbbmss{t}/\mathbbmss{t}$$i/o_{1}$$\mathbbmss{t}/\mathbbmss{t}$$i/o_{2}$$\mathbbmss{t}/\mathbbmss{t}$$i/o_{2}$$\mathbbmss{t}/\mathbbmss{t}$$i/o_{2}$$\mathbbmss{t}/\mathbbmss{t}$$i/o_{1}$$\mathbbmss{t}/\mathbbmss{t}$
(b) $\mathbbmss{t}$-Abstract untimed FSM $A_{M}$

Figure 2: $\mathbbmss{t}$-abstraction of TFSM with timeout and timed guards.

Figure 2 shows an example of a TFSM with timeouts and its
$\mathbbmss{t}$-abstraction. In this case the untimed abstraction accepts
untimed input words on $I\cup\\{\mathbbmss{t}\\}$. The delay is implicitly
represented by sequences of the special input symbol $\mathbbmss{t}$
interleaving the occurrences of the real input symbols from $I$. The
representation of delays in the abstraction is quite involved:

  * •

an _even number_ $2n$ of $\mathbbmss{t}$ symbols represents a delay of
_exactly_ $n$ time units;

  * •

an _odd number_ $2n+1$ of $\mathbbmss{t}$ symbols represents a delay $t$
included in the open interval $(n,n+1)$.

The notion of abstraction of a timed word captures the above intuition.

######  Definition 4.

Let $\mathbbmss{t}(t)$ be a function mapping a delay $t\in\mathbb{R}$ to a
sequence of $\mathbbmss{t}$ as follows: $\mathbbmss{t}(t)=\mathbbmss{t}^{2t}$
if ${\lfloor{t}\rfloor}=t$,
$\mathbbmss{t}(t)=\mathbbmss{t}^{2{\lfloor{t}\rfloor}+1}$ otherwise. Given a
finite alphabet $A$ and a finite timed word $v=(a_{1},t_{1})$
$(a_{2},t_{2})(a_{3},t_{3})\dots(a_{m},t_{m})$, we define its _$\mathbbmss{t}$
-abstraction_ as the finite word
$\mathbbmss{t}(v)=\mathbbmss{t}(t_{1})a_{1}\mathbbmss{t}(t_{2}-t_{1})\dots\mathbbmss{t}(t_{j}-t_{j-1})a_{j}\mathbbmss{t}(t_{j+1}-t_{j})\dots\mathbbmss{t}(t_{m-1}-t_{m})a_{m}$.

$\mathbbmss{t}$-bisimulation connects _timed states $(s,x)$_ of a timed FSM
with states of an untimed FSM. Conditions 1. and 2. formalize the connection
between timed transitions and the special symbol $\mathbbmss{t}$. Conditions
3. and 4. formalize the connection between actual input/output transition in
the two machines.

######  Definition 5.

Given a TFSM with timed guards and timeouts
$T=(S,I,O,\lambda_{S},s_{0},\Delta_{S})$ and an untimed FSM
$U=(R,I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{R},r_{0})$, a
_$\mathbbmss{t}$ -bisimulation_ is a relation
$\sim\subseteq(S\times\mathbb{R}^{+})\times R$ that respects the following
conditions for every pair of states $(s,x)\in S\times\mathbb{R}^{+}$ and $r\in
R$ such that $(s,x)\sim r$:

  1. 1.

if $(s,x)\xrightarrow{t}(s^{\prime},x^{\prime})$ with $0<t<1$ and either
$x\in\mathbb{N}$ or $x+t\in\mathbb{N}$ then there exists $r^{\prime}\in R$
such that $r\xrightarrow{\mathbbmss{t},\mathbbmss{t}}r^{\prime}$ and
$(s^{\prime},x^{\prime})\sim r^{\prime}$;

  2. 2.

if $r\xrightarrow{\mathbbmss{t},\mathbbmss{t}}r^{\prime}$ then for every
$0<t<1$ such that either $x\in\mathbb{N}$ or $x+t\in\mathbb{N}$ there exists
$(s^{\prime},x^{\prime})\in S\times\mathbb{R}^{+}$ such that
$(s,x)\xrightarrow{t}(s^{\prime},x^{\prime})$ and $(s^{\prime},x^{\prime})\sim
r^{\prime}$;

  3. 3.

if $(s,x)\xrightarrow{i,o}(s^{\prime},0)$ then there exists $r^{\prime}\in R$
such that $r\xrightarrow{i,o}r^{\prime}$ and $(s^{\prime},0)\sim r^{\prime}$;

  4. 4.

if $r\xrightarrow{i,o}r^{\prime}$ then there exists $(s^{\prime},0)\in
S\times\mathbb{R}^{+}$ such that $(s,x)\xrightarrow{i,o}(s^{\prime},0)$ and
$(s^{\prime},0)\sim r^{\prime}$.

$T$ and $U$ are _$\mathbbmss{t}$ -bisimilar_ if there exists a
$\mathbbmss{t}$-bisimulation $\sim\subseteq S\times R$ such that
$(s_{0},0)\sim r_{0}$.

To prove that $\mathbbmss{t}$-bisimilar machines have the same behavior we
need to introduce the following technical result, connecting timed transitions
with the special symbol $\mathbbmss{t}$.

######  Lemma 2.

Given a TFSM with timed guards and timeouts
$T=(S,I,O,\lambda_{S},s_{0},\Delta_{S})$ and an untimed FSM
$U=(R,I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{R},r_{0})$,
every $\mathbbmss{t}$-bisimulation relation
$\sim\subset(S\times\mathbb{R}^{+})\times R$ respects the following properties
for every $(s,0)\sim r$ and $t>0$:

  1. (i)

if $(s,0)\xrightarrow{t}(s^{\prime},x^{\prime})$ then there exists
$r^{\prime}$ such that $(s^{\prime},x^{\prime})\sim r^{\prime}$ and
$r\xrightarrow{\mathbbmss{t}(t),\mathbbmss{t}(t)}r^{\prime}$;

  2. (ii)

if $r\xrightarrow{\mathbbmss{t}(t),\mathbbmss{t}(t)}r^{\prime}$ then there
exists $(s^{\prime},x^{\prime})\sim r^{\prime}$ such that
$(s,0)\xrightarrow{t}(s^{\prime},x^{\prime})$.

###### Proof.

The proof is by induction on the number of symbols $n$ in $\mathbbmss{t}(t)$.
For the basis of the induction, suppose $n=1$ and let $(s,0)\sim r$: by the
definition of $\mathbbmss{t}(t)$, we have that $0<t<1$. The two properties are
a direct consequence of the definition of $\mathbbmss{t}$-bisimulation. By
condition 1 of Definition 5, we have that for every $0<t<1$,
$(s,0)\xrightarrow{t}(s^{\prime},x^{\prime})$ implies that there exists
$r^{\prime}$ such that $(s^{\prime},x^{\prime})\sim r^{\prime}$ and
$r\xrightarrow{\mathbbmss{t},\mathbbmss{t}}r^{\prime}$. By condition 2 of
Definition 5, we have that for every $0<t<1$,
$r\xrightarrow{\mathbbmss{t},\mathbbmss{t}}r^{\prime}$ implies that there
exists $(s^{\prime},x^{\prime})\sim r^{\prime}$ such that
$(s,0)\xrightarrow{t}(s^{\prime},x^{\prime})$.

For the inductive case, suppose that $n\geq 1$ and that the Lemma holds for
$n-1$. Now, let $(s,0)\xrightarrow{t}(s^{\prime},x^{\prime})$. Two cases may
arise: either ${\lfloor{t}\rfloor}=t$ or ${\lfloor{t}\rfloor}>t$. In the
former case, consider the timed state $(s^{\prime\prime},x^{\prime\prime})$
such that
$(s,0)\xrightarrow{t-0.5}(s^{\prime\prime},x^{\prime\prime})\xrightarrow{0.5}(s^{\prime},x^{\prime})$.111Here
$0.5$ is an arbitrary value chosen for the sake of simplicity. Indeed, the
argument holds for every delay $0<t^{*}<1$. Since the number of symbols in
$\mathbbmss{t}(t-0.5)$ is exactly $n-1$, by inductive hypothesis we have that
there exists $r^{\prime\prime}$ such that
$(s^{\prime\prime},x^{\prime\prime})\sim r^{\prime\prime}$ and
$r\xrightarrow{\mathbbmss{t},\mathbbmss{t}^{n-1}}r^{\prime\prime}$. By
condition 1 of Definition 5, we have that there exists $r^{\prime}$ such that
$(s^{\prime},x^{\prime})\sim r^{\prime}$ and
$r^{\prime\prime}\xrightarrow{\mathbbmss{t},\mathbbmss{t}}r^{\prime}$ and thus
that $r\xrightarrow{\mathbbmss{t}(t),\mathbbmss{t}(t)}r^{\prime}$. To prove
property (ii), suppose
$r\xrightarrow{\mathbbmss{t}(t),\mathbbmss{t}(t)}r^{\prime}$ and consider the
state $r^{\prime\prime}$ such that
$r\xrightarrow{\mathbbmss{t},\mathbbmss{t}^{n-1}}r^{\prime\prime}\xrightarrow{\mathbbmss{t},\mathbbmss{t}}r^{\prime}$.
By inductive hypothesis we have that there exists
$(s^{\prime\prime},x^{\prime\prime})\sim r^{\prime\prime}$ such that
$(s,0)\xrightarrow{t-0.5}(s^{\prime\prime},x^{\prime\prime})$. By condition 2
of Definition 5 it is possible to find a state $(s^{\prime},x^{\prime})$ such
that $(s^{\prime},x^{\prime})\sim r^{\prime}$ and
$(s^{\prime\prime},x^{\prime\prime})\xrightarrow{0.5}(s^{\prime},x^{\prime})$.
This shows that $(s,0)\xrightarrow{t}(s^{\prime},x^{\prime})$. When
${\lfloor{t}\rfloor}>t$, we can consider the timed state
$(s^{\prime\prime},x^{\prime\prime})$ such that
$(s,0)\xrightarrow{{\lfloor{t}\rfloor}}(s^{\prime\prime},x^{\prime\prime})\xrightarrow{t-{\lfloor{t}\rfloor}}(s^{\prime},x^{\prime})$.
Since the number of symbols in $\mathbbmss{t}({\lfloor{t}\rfloor})$ is exactly
$n-1$, by an argument similar to the above we can prove that both properties
_(i)_ and _(ii)_ hold also in this case, concluding the proof. ∎

The following lemma proves that $\mathbbmss{t}$-bisimilar machines have the
same behavior.

######  Lemma 3.

Given a TFSM with timeouts $T=(S,I,O,\lambda_{S},s_{0},\Delta_{S})$ and an
untimed FSM
$U=(R,I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{R},r_{0})$,
if there exists a $\mathbbmss{t}$-bisimulation $\sim$ such that $(s_{0},0)\sim
r_{0}$ then for every timed input word $v=(i_{1},t_{1})\dots(i_{m},t_{m})$ we
have that $\mathbbmss{t}(B_{T}(v))=B_{U}(\mathbbmss{t}(v))$.

###### Proof.

We prove the lemma by showing that the following claim holds:

> for every pair of states $s\in S$ and $r\in R$ such that $(s,0)\sim r$ and
> timed word $v$, $\lambda_{S}(s,v)=(s^{\prime},w)$ if and only if
> $\lambda_{R}(r,\mathbbmss{t}(v))=(r^{\prime},\mathbbmss{t}(w))$ with
> $(s^{\prime},0)\sim r^{\prime}$.

We prove the claim by induction on the length $m$ of the input word. Suppose
$m=1$, $v=(i_{1},t_{1})$ and $w=(o_{1},t_{1})$. We have to show that
$\lambda_{S}(s,(i_{1},t_{1}))=(s^{\prime},(o_{1},t_{1}))$ if and only if
$\lambda_{R}(r,\mathbbmss{t}(i_{1},t_{1}))=(r^{\prime},\mathbbmss{t}(o_{1},t_{1}))$
for some $r^{\prime}$ such that $(s^{\prime},0)\sim r^{\prime}$.

To prove the direct implication, suppose $\lambda_{S}(s,v)=(s^{\prime},w)$. By
the definition of TFSM we have that
$\lambda_{S}(s,(i_{1},t_{1}))=(s_{1},(o_{1},t_{1}))$ if and only if there
exists a timed state $(s^{\prime},x^{\prime})$ such that
$(s,0)\xrightarrow{t_{1}}(s^{\prime},x^{\prime})\xrightarrow{i_{1},o_{1}}(s_{1},0)$.
We distinguish between two cases depending on the value of $t_{1}$.

  * •

If $t_{1}=0$, by condition 3. of the definition of
$\mathbbmss{t}$-bisimulation (since
$(s^{\prime},x^{\prime})\xrightarrow{i_{1},o_{1}}(s_{1},0)$), there exists
$r_{1}\in R$ such that $r\xrightarrow{i_{1},o_{1}}r_{1}$. Hence,
$\lambda_{R}(r,\mathbbmss{t}(i_{1},t_{1}))=(r_{1},\mathbbmss{t}(o_{1},t_{1}))$.

  * •

If $t_{1}>0$, by Lemma 2 (i), there exists $r^{\prime}$ such that
$r\xrightarrow{\mathbbmss{t}(t_{1}),\mathbbmss{t}(t_{1})}r^{\prime}$ and
$(s^{\prime},x^{\prime})\sim r^{\prime}$. By condition 3. of the definition of
$\mathbbmss{t}$-bisimulation (since
$(s^{\prime},x^{\prime})\xrightarrow{i_{1},o_{1}}(s_{1},0)$), we have that it
is possible to find a state $r_{1}\in R$ such that
$r^{\prime}\xrightarrow{i_{1},o_{1}}r_{1}$. This implies that under input
$\mathbbmss{t}(t_{1})i_{1}=\mathbbmss{t}(i_{1},t_{1})$ the FSM $U$ produces
the output word $\mathbbmss{t}(t_{1})o_{1}=\mathbbmss{t}(o_{1},t_{1})$, and
thus we can conclude that
$\lambda_{R}(r,\mathbbmss{t}(i_{1},t_{1}))=(r_{1},\mathbbmss{t}(o_{1},t_{1}))$.

To prove the converse implication, suppose
$\lambda_{R}(r,\mathbbmss{t}(i_{1},t_{1}))=(r_{1},\mathbbmss{t}(o_{1},t_{1}))$.
We distinguish between two cases depending on the value of $t_{1}$.

  * •

If $t_{1}=0$, then by the assumption
$\lambda_{R}(r,\mathbbmss{t}(i_{1},t_{1}))=(r_{1},\mathbbmss{t}(o_{1},t_{1}))$
there exists $r^{\prime}\in R$ such that
$r^{\prime}\xrightarrow{i_{1},o_{1}}r_{1}$, and so by condition 4. of the
definition of $\mathbbmss{t}$-bisimulation, there exists $(s_{1},0)\in
S\times\mathbb{R}$ such that $(s,t_{1})\xrightarrow{i_{1},o_{1}}(s_{1},0)$.
Hence, $\lambda_{S}(s,(i_{1},t_{1}))=(s_{1},(o_{1},t_{1}))$.

  * •

If $t_{1}>0$, then by the assumption
$\lambda_{R}(r,\mathbbmss{t}(i_{1},t_{1}))=(r_{1},\mathbbmss{t}(o_{1},t_{1}))$
there exists $r^{\prime}\in R$ such that
$r\xrightarrow{\mathbbmss{t}(t_{1}),\mathbbmss{t}(t_{1})}r^{\prime}\xrightarrow{i_{1},o_{1}}r_{1}$.
By Lemma 2 (ii), there exists $(s^{\prime},x^{\prime})\in S\times\mathbb{R}$
such that $(s,0)\xrightarrow{t_{1}}(s^{\prime},x^{\prime})$ and
$(s^{\prime},x^{\prime})\sim r^{\prime}$. By condition 4. of the definition of
$\mathbbmss{t}$-bisimulation, we have that there exists a timed state
$(s_{1},0)$ such that
$(s^{\prime},x^{\prime})\xrightarrow{i_{1},o_{1}}(s_{1},0)$. This implies that
under input $(i_{1},t_{1})$ the TFSM $T$ produces the timed output word
$(o_{1},t_{1})$, and thus we can conclude that
$\lambda_{S}(s,(i_{1},t_{1}))=(s_{1},(o_{1},t_{1}))$.

Since our machines may be partial, we have that $\lambda_{S}(s,(i_{1},t_{1}))$
and $\lambda_{R}(r,\mathbbmss{t}(v))$ are not necessarily defined. However,
the above argument also shows that $\lambda_{S}(s,(i_{1},t_{1}))$ is defined
if and only if $\lambda_{R}(r,\mathbbmss{t}(v))$ is defined.

To prove the inductive case, suppose $m>1$,
$v=(i_{1},t_{1})\ldots(i_{m},t_{m})$ and $w=(i_{1},t_{1})\ldots$
$(i_{m},t_{m})$. Now, let $v^{\prime}=(i_{1},t_{1})\ldots(i_{m-1},t_{m-1})$
and $w^{\prime}=(o_{1},t_{1})\ldots(o_{m-1},t_{m-1})$. By inductive
hypothesis, we have that $\lambda_{S}(s,v^{\prime})=(s_{m-1},w^{\prime})$ if
and only if
$\lambda_{R}(r,\mathbbmss{t}(v^{\prime}))=(r_{m-1},\mathbbmss{t}(w^{\prime}))$
for some $(s_{m-1},0)\sim r_{m-1}$, and that
$\lambda_{S}(s_{m-1},(i_{m},t_{m}-t_{m-1}))=(s_{m},(o_{m},t_{m}-t_{m-1}))$ if
and only if
$\lambda_{R}(r_{m-1},\mathbbmss{t}(i_{m},t_{m}-t_{m-1}))=(r_{m},\mathbbmss{t}(o_{m},t_{m}-t_{m-1}))$
for some $(s_{m},0)\sim r_{m}$. This implies that
$\lambda_{S}(s,v^{\prime}(i_{m},t_{m}))=(s_{m},w^{\prime}(o_{m},t_{m}))$ if
and only if
$\lambda_{R}(r,\mathbbmss{t}(v))=\lambda_{R}(r,\mathbbmss{t}(v^{\prime}(i_{m},t_{m})))=(r_{m},\mathbbmss{t}(w^{\prime})\mathbbmss{t}(o_{m},t_{m}-t_{m-1}))=(r_{m},\mathbbmss{t}(w))$,
and thus that the claim holds also for $m$.

To conclude the proof of the Lemma it is sufficient to recall that from the
definition of behaviour we have that $B_{T}(v)=w$ if and only if
$\lambda_{S}(s_{0},v)=(s_{m},w)$ for some state $s_{m}\in S$. From
$(s_{0},0)\sim r_{0}$ (hypothesis of the lemma) we can conclude that
$\lambda_{R}(r_{0},\mathbbmss{t}(v))=(r_{m},\mathbbmss{t}(w))$ and thus that
$B_{U}(\mathbbmss{t}(v))=\mathbbmss{t}(w)=\mathbbmss{t}(B_{T}(v))$. ∎

######  Theorem 1.

A TFSM with timeouts and timed guards $M$ is $\mathbbmss{t}$-bisimilar to the
abstract FSM $A_{M}$.

###### Proof.

The relation $\sim=\\{((s,x),(s,\langle n,n^{\prime}\rangle))\mid x\in\langle
n,n^{\prime}\rangle\\}$ is a $\mathbbmss{t}$-bisimulation for $M$ and $A_{M}$.
∎

We can use the above theorem to solve the equivalence problem for TFSM with
timed guards.

######  Corollary 1.

Let $M$ and $M^{\prime}$ be two TFSM with timeouts and timed guards. Then $M$
and $M^{\prime}$ are equivalent if and only if the two abstract FSM $A_{M}$
and $A_{M^{\prime}}$ are equivalent.

###### Proof.

The claim is a direct consequence of Theorem 1 and Lemma 3. ∎

##  3 From untimed FSMs to TFSMs

In the previous section we have shown how to build an abstract untimed FSM
that represents the behaviour of a TFSM, by means of appropriate notions of
bisimulation and of abstraction of timed words. In this section we study the
conditions under which the opposite transformation is possible: we take an
untimed FSM that accepts and produces words from input and output alphabets
that include the special symbol $\mathbbmss{t}$, and we show how to build an
equivalent TFSM with timeouts and timed guards, under the same notion of
abstraction of timed words.

Now, let $I$ and $O$ be, respectively, the input and output alphabets of our
machines. We are interested in studying untimed FSMs that accept words in
$(I\cup\\{\mathbbmss{t}\\})^{*}$ and produce words in
$(O\cup\\{\mathbbmss{t}\\})^{*}$. Clearly, not all untimed FSMs represent
valid timed behaviours. In particular, since in our TFSMs model outputs are
instantaneously produced when an input is received, and since a TFSM cannot
stop the advancing of time, we have that a deterministic untimed FSM
$U=(R,I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{R},r_{0})$
can be transformed into a TFSM only if every state $r$ of $U$ respects the
following two conditions:

  1. 1.

$\lambda_{R}(r,\mathbbmss{t})$ is defined and such that
$\lambda_{R}(r,\mathbbmss{t})=(r^{\prime},\mathbbmss{t})$ for some
$r^{\prime}\in R$ (when the input $\mathbbmss{t}$ is received, the FSM should
produce the output $\mathbbmss{t}$);

  2. 2.

for every input $i\in I$, if $\lambda(r,i)$ is defined then
$\lambda(r,i)=(r^{\prime},o)$ for some output $o\in O$ and state
$r^{\prime}\in R$ (when an input from $I$ is received, the FSM produces an
output from $O$).

We call any untimed FSM that respects the above two conditions _time
progressive_.

In the following we prove that every _deterministic time progressive_ FSM can
be transformed into an equivalent TFSM with timeouts and timed guards. Since
we cannot directly compare the behavior of an untimed FSM with the behavior of
a timed FSM, we will use the notion of $\mathbbmss{t}$-abstraction of a timed
word (Definition 4) to compare timed and untimed machines.

######  Definition 6.

Given a deterministic and time progressive FSM
$U=(R,I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{R},$
$r_{0})$, and a TFSM with timed guards and timeouts
$T=(S,I,O,\lambda_{S},s_{0},\Delta_{S})$, we say that _$T$ refines $U$_ if and
only if for every timed input word $v=(i_{1},t_{1})\dots(i_{m},t_{m})$ we have
that $B_{U}(\mathbbmss{t}(v))=\mathbbmss{t}(B_{T}(v))$.

The intuition behind the construction is the following. Since we start from a
deterministic and time progressive FSM $U$, from every state of $U$ there
exists exactly one transition with input $\mathbbmss{t}$ (and output
$\mathbbmss{t}$). Hence, given a state $s$ we can build the (infinite) “delay
run”

$\rho_{\mathbbmss{t}}^{s}=s\xrightarrow{\mathbbmss{t},\mathbbmss{t}}s_{1}\xrightarrow{\mathbbmss{t},\mathbbmss{t}}s_{2}\xrightarrow{\mathbbmss{t},\mathbbmss{t}}\dots$

Since the number of states of $U$ is finite, we have that the delay run is
“lasso shaped”, namely, that it consists of a prefix
$s\xrightarrow{\mathbbmss{t},\mathbbmss{t}}\dots\xrightarrow{\mathbbmss{t},\mathbbmss{t}}s_{p}$
followed by the infinite repetition of a loop
$s_{p}\xrightarrow{\mathbbmss{t},\mathbbmss{t}}\dots\xrightarrow{\mathbbmss{t},\mathbbmss{t}}s_{p}$.

The refined TFSM $T$ will have the same set of states of $U$. Then, for every
state $s$ the delay run is computed, and the transitions and timeouts are
defined as follows:

  * •

every $I/O$ transition leaving a state in the prefix is replaced with a timed
transition from $s$ with an appropriate timed guard;

  * •

a timeout corresponding to the length of the prefix forces $T$ to switch from
$s$ to a state in the loop.

Algorithm 1 Transform a FSM into a TFSM with timeouts and timed guards

1:A time progressive and deterministic FSM
$U=(S,I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{U},s_{0})$

2:A TFSM $T=(S,I,O,\lambda_{T},s_{0},\Delta_{T})$ that refines $U$

3:function Refine($U$)

4: $\lambda_{T}\leftarrow\emptyset$

5: $\Delta_{T}\leftarrow\emptyset$

6: $T\leftarrow(S,I,O,\lambda_{T},s_{0},\Delta_{T})$

7: for all $s\in S$ do

8: $\textsc{AddTimedTrans}(s,U,T)$

9: return T

Algorithms 1 and 2 describe the above procedure in detail. To simplify the
code, we will unfold the final loop once, and put the timeout in
correspondence to the second occurrence of $s_{p}$ in the delay run. Moreover,
since $U$ is assumed to be deterministic, we consider the transition relation
as a partial function $\lambda_{U}:S\times I\cup\\{\mathbbmss{t}\\}\mapsto
S\times O\cup\\{\mathbbmss{t}\\}$ returning the next state and the output.

Algorithm 2 Add timed transitions to a state $s$

1:function AddTimedTrans($s,U,T$)

2: for all $r\in S$ do $\textsc{Marked}(r)\leftarrow False$

3: $r\leftarrow s$

4: $g\leftarrow[0,0]$

5: while not Marked($r$) do

6: $\textsc{Marked}(r)\leftarrow True$

7: for all $i\in I$ such that $i\neq\mathbbmss{t}$ and $\lambda_{U}(r,i)$ is
defined do

8: $(r^{\prime},o)\leftarrow\lambda_{U}(r,i)$

9: add $(s,i,g,o,r^{\prime})$ to $\lambda_{T}$

10: $r\leftarrow\lambda_{U}(r,\mathbbmss{t})\downarrow_{S}$

11: if $g=[n,n]$ then $g\leftarrow(n,n+1)$

12: else if $g=(n,n+1)$ then $g\leftarrow[n+1,n+1]$

13: if $g=[n,n]$ then $\Delta_{T}(s)=(r,n)$ $\triangleright$ prefix of even
length: set the timeout and return

14: else if $g=(n,n+1)$ then $\triangleright$ prefix of odd length: unfold it
one more step

15: for all $i\in I$ such that $i\neq\mathbbmss{t}$ do

16: $(r^{\prime},o)\leftarrow\lambda_{U}(r,i)$

17: add $(s,i,g,o,r^{\prime})$ to $\lambda_{T}$

18: $r\leftarrow\lambda_{U}(r,\mathbbmss{t})\downarrow_{S}$

19: $\Delta_{T}(s)=(r,n+1)$

We prove the correctness of our construction by showing that the TFSM $T$
obtained from Algorithm 1 is $\mathbbmss{t}$-bisimilar to $U$. Hence, by Lemma
3, we can immediately conclude that $T$ is a refinement of $U$.

######  Theorem 2.

Given a time progressive and deterministic FSM
$U=(S,I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{U},$
$s_{0})$, Algorithm 1 builds a TFSM with timeouts and timed guards
$T=(S,I,O,\lambda_{T},$ $s_{0},\Delta_{T})$ for which there exists a
$\mathbbmss{t}$-bisimulation $\sim$ such that $(s_{0},0)\sim s_{0}$.

###### Proof.

Let
$U=(S,I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{U},s_{0})$ be
a time progressive and deterministic FSM, and let
$T=(S,I,O,\lambda_{T},s_{0},\Delta_{T})$ be the TFSM built by Algorithm 1. We
define the following relation between states of $T$ and states of $U$:

$\sim=\\{((s,x),r)\mid
r=\hat{\lambda}_{U}(s,\mathbbmss{t}(x))\downarrow_{S}\\}$ (1)

where $\hat{\lambda}_{U}:S\times(I\cup\\{\mathbbmss{t}\\})^{*}\mapsto
S\times(O\cup\\{\mathbbmss{t}\\})^{*}$ is the usual extension of the
transition function $\lambda_{U}$ to input words.

We show that $\sim$ is indeed a $\mathbbmss{t}$-bisimulation between $T$ and
$U$ by proving that the function AddTimedTransition (Algorithm 2) respects the
following invariant:

  * INV

$(s,x)\sim r$ for all $x\in g$, and all conditions of Definition 5 are
respected by the transitions in $\lambda_{T}$

Before entering into the while loop, AddTimedTransition sets $r=s$ and
$g=[0,0]$. Since $\mathbbmss{t}(0)=\varepsilon$, we have that $(s,0)\sim s$,
and since $\lambda_{T}$ is empty, Definition 5 is trivially respected.

Consider now a generic iteration of the while loop (lines 5–12). By the
invariant, we have that $(s,x)\sim r$ for all $x\in g$. The for loop (lines
7–9) iterates through all transitions of $U$ activated by an actual input
$i\in I$, adding a transition $(s,i,o,g,r^{\prime})$ to $\lambda_{T}$ for
every transition $(r,i,o,r^{\prime})\in\lambda_{U}$. Hence, for every $x\in g$
we have that $(s,x)\xrightarrow{i,o}(r^{\prime},0)$ and
$r\xrightarrow{i,o}r^{\prime}$. Since $(s,x)\sim r$ and $(r^{\prime},0)\sim
r^{\prime}$, we have that conditions 3 and 4 of Definition 5 are respected.
After updating $\lambda_{T}$, lines 10–12 update the value of $r$ and $g$. Let
us call $r_{old}$ and $g_{old}$ the values of $r$ and $g$ before the update.
Then, $r$ is set to the $\mathbbmss{t}$-successor of $r_{old}$ and $g$ is
updated to the “next interval” as follows:

  * •

if $g_{old}=[n,n]$ then $g=(n,n+1)$;

  * •

if $g_{old}=(n,n+1)$ then $g=[n+1,n+1]$.

We consider the two cases separately. If $g=[n,n]$ then the only possible
state $(s,x)$ such that $x\in[n,n]$ is $(s,n)$. Moreover, by the definition of
$\sim$, since $(s,n)\sim r_{old}$ we have that
$r_{old}=\hat{\lambda}_{U}(s,\mathbbmss{t}(n))\downarrow_{S}$, with
$\mathbbmss{t}(n)=\mathbbmss{t}^{2n}$. Since line 10 updates $r$ to
$\lambda_{U}(r_{old},\mathbbmss{t})$, and since
$\mathbbmss{t}(x+t)=\mathbbmss{t}^{2n+1}$ for every $0<t<1$, we have that
$r=\hat{\lambda}_{U}(s,\mathbbmss{t}(x+t))\downarrow_{S}$. Hence, since
$(s,n)\xrightarrow{t}(s,n+t)$, $(s,n+t)\sim r$ and
$r_{old}\xrightarrow{\mathbbmss{t},\mathbbmss{t}}r$ we have that conditions 1
and 2 of Definition 5 are respected. By a similar argument, if $g=(n,n+1)$ we
can show that $(s,x)\xrightarrow{t}(s,x+t)$, $(s,x+t)\sim r$ and
$r_{old}\xrightarrow{\mathbbmss{t},\mathbbmss{t}}r$ for every $x$ and $t$ such
that $0<t<1$ and $x+t=n+1$, respecting conditions 1 and 2 of Definition 5 also
in this case. Hence, every iteration of the while loop respects the invariant.

The loop terminates when $r$ is a Marked state, that is, when it reaches the
first repetition of a state in the delay run from $s$. Lines 13–19 take care
of setting appropriately the timeout at state $s$. Two different situations
may arise: either $g=[n,n]$ or $g=(n,n+1)$ for some $n\in\mathbb{N}$. In the
former case, the state $r$ is repeated after an even number of transitions,
which corresponds to an integer time delay. Hence, the timeout at $s$ is set
to $\Delta_{S}(s)=(r,n)$. Consider now the predecessor $r_{pred}$ of $r$ in
the delay run. By the invariant, we have that $(s,x)\sim r_{pred}$ for every
$x\in(n-1,n)$. Hence, we have that $(s,x)\xrightarrow{n-x}(r,0)$ for every
$n-1<x<n$, $r_{pred}\xrightarrow{\mathbbmss{t},\mathbbmss{t}}r$, $(s,x)\sim
r_{pred}$ and $(r,0)\sim r$, respecting conditions 1 and 2 of Definition 5. In
the latter case ($g=(n,n+1)$), $r$ is repeated after an odd number of
transitions. Since the timeout at $s$ must be an integer value, lines 14–19
repeat the construction of the while loop one more time and then update $r$ to
a state that corresponds to precisely $n+1$ time units before setting the
timeout. As in the previous case, we can prove that the invariant is
respected.

To conclude the proof we observe that Algoritm 1 executes AddTimedTransition
on every state $s\in S$. Hence, the final TFSM $T$ is in relation $\sim$ with
$U$. Since $\sim$ respects all conditions of Definition 5, we have that it is
a $\mathbbmss{t}$-bisimulation between $T$ and $U$ such that $(s_{0},0)\sim
s_{0}$. ∎

######  Corollary 2.

Given a time progressive and deterministic FSM
$U=(S,I\cup\\{\mathbbmss{t}\\},O\cup\\{\mathbbmss{t}\\},\lambda_{U},$
$s_{0})$, Algorithm 1 builds a TFSM with timeouts and timed guards
$T=(S,I,O,\lambda_{T},s_{0},\Delta_{T})$ that refines $U$.

$q_{0}$$q_{2}$$q_{5}$$[0,1):i/o_{1}$$(2,3):i/o_{1}$$[1,2]:i/o_{2}$$t=3$$[0,1]:i/o_{2}$$(1,2):i/o_{1}$$t=2$$t=1$$[0,1):i/o_{1}$
Figure 3: Example of application of Algorithm 1.

Figure 3 shows the TFSM with timeouts and timed guards that can be obtained by
applying Algorithm 1 to the untimed FSM of Figure 2(b), where the states have
been renamed as follows:

$\displaystyle(s_{0},[0,0])$ $\displaystyle=q_{0}$
$\displaystyle(s_{0},(0,1))$ $\displaystyle=q_{1}$
$\displaystyle(s_{1},[0,0])$ $\displaystyle=q_{2}$
$\displaystyle(s_{1},(0,1))$ $\displaystyle=q_{3}$
$\displaystyle(s_{1},[1,1])$ $\displaystyle=q_{4}$
$\displaystyle(s_{1},(1,\infty))$ $\displaystyle=q_{5}$

In the picture, transitions with adjacent guards have been merged: for
instance, the application of the algorithm creates the transitions
$(q_{0},i,o_{1},[0,0],q_{0})$ and the transition $(q_{0},i,o_{1},(0,1),q_{0})$
that are merged into the unique transition $(q_{0},i,o_{1},[0,1),q_{0})$ in
the picture. The picture includes only the states that are reachable from the
initial state $q_{0}$. This shows that in the final result only the three
states $q_{0}$, $q_{2}$ and $q_{5}$ are relevant: the other states have been
replaced by either timed guards or timeouts.

To better understand how Algorihm 1 works, let us review the application of
function AddTimedTrans (Algorithm 2) to the initial state $q_{0}$ (state
$(s_{0},[0,0])$ in the picture) of the untimed FSM $A_{M}$ of Figure 2(b). The
procedure starts by unmarking all states of $A_{M}$ and by initialising the
current state $r$ to $q_{0}$ and the current guard $g$ to $[0,0]$. Then the
while loop of lines 5–12 follows the sequence of $\mathbbmss{t}/\mathbbmss{t}$
transitions in $A_{M}$, marking the states it reaches, until a previously
marked state is found. At lines 7-9, for every I/O transition exiting the
current state, a corresponding timed transition labelled with the current
value of $g$ is added to the TFSM. Then the current state $r$ is updated to
the next state in the sequence of $\mathbbmss{t}/\mathbbmss{t}$ transitions
and $g$ is increased following the sequence $[0,0],(0,1),[1,1],(1,2),\dots$.
In this example, the first iteration of the while loop considers all I/O
transitions exiting from the state $q_{0}$ of $A_{M}$, namely the transition
$q_{0}\xrightarrow{i/o_{1}}q_{0}$, and adds the transition
$q_{0}\xrightarrow{[0,0]:i/o_{1}}q_{0}$ to the TFSM (the initial value of $g$
is indeed $[0,0]$). Then $r$ is updated to $q_{1}$, $g$ to $(0,1)$ and the
second iteration is started. The transition $q_{1}\xrightarrow{i/o_{1}}q_{0}$
corresponds to the transition $q_{0}\xrightarrow{(0,1):i/o_{1}}q_{0}$ in the
TFSM. Notice that the starting state of the timed transition is still $q_{0}$.
The $\mathbbmss{t}/\mathbbmss{t}$ transition between $q_{0}$ and $q_{1}$ of
$A_{M}$ models the fact that the machine waits for a time included in the
interval $(0,1)$ before accepting an input. This situation is modelled in the
TFSM by adding the guard $(0,1)$ to the transition while keeping $q_{0}$ as
starting state. Then the loop continues by adding the following transitions to
the TFSM:

$\displaystyle q_{0}\xrightarrow{[1,1]:i/o_{2}}q_{2}$ $\displaystyle
q_{0}\xrightarrow{(1,2):i/o_{2}}q_{2}$ $\displaystyle
q_{0}\xrightarrow{[2,2]:i/o_{2}}q_{2}$ $\displaystyle
q_{0}\xrightarrow{(2,3):i/o_{1}}q_{0}$

At this point, the current state $r$ of $A_{M}$ is $q_{5}$ (i.e.,
$(s_{1},(1,\infty))$) and the guard $g$ is $(2,3)$. Because of the self loop
on $\mathbbmss{t}/\mathbbmss{t}$ of $A_{M}$ in state $q_{5}$, at the end of
the loop $r$ does not change and $g$ is updated to $[3,3]$: a previously
marked state is reached and the loop terminates. Lines 13–19 of AddTimedTrans
set the timeout at state $q_{0}$ to $(q_{5},3)$, terminating the function
call. The value of the timeout is set to $3$ because the first marked state is
reached after $6$ $\mathbbmss{t}/\mathbbmss{t}$ transitions, which corresponds
to $3$ time units. A subsequent call to AddTimedTrans on state $q_{5}$ will
set the timeout at state $q_{5}$ to $(q_{5},1)$ (i.e., the self-loop on $t=1$
depicted in the figure), to model the fact that in the untimed FSM $A_{M}$
there is a self-loop on $\mathbbmss{t}/\mathbbmss{t}$ at state $q_{5}$. In
this way, the sequence of $\mathbbmss{t}/\mathbbmss{t}$ transitions
$q_{0}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}q_{1}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}q_{2}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}q_{3}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}q_{4}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}q_{5}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}q_{5}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}q_{5}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}q_{5}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}q_{5}\xrightarrow{\mathbbmss{t}/\mathbbmss{t}}\dots$
of $A_{M}$ is replaced by the sequence of timeout transitions
$q_{0}\xrightarrow{3}q_{5}\xrightarrow{1}q_{5}\xrightarrow{1}\dots$. In both
cases the machines can wait in $q_{5}$ forever, if no input is received in the
first $3$ time units. The application of AddTimedTrans to the other states of
$A_{M}$ builds the rest of the TFSM.

$q_{0}$ $[0,0]$ $q_{0}$ $(0,1)$ $q_{0}$ $[1,1]$ $q_{0}$ $(1,2)$ $q_{0}$
$[2,2]$ $q_{0}$ $(2,3)$ $q_{2}$ $[0,0]$ $q_{2}$ $(0,1)$ $q_{2}$ $[1,1]$
$q_{2}$ $(1,2)$ $q_{5}$ $[0,0]$ $q_{5}$ $(0,1)$
$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$i/o_{1}$$i/o_{1}$$i/o_{2}$$i/o_{2}$$i/o_{2}$$i/o_{1}$$i/o_{2}$$i/o_{2}$$i/o_{2}$$i/o_{1}$$i/o_{1}$$i/o_{1}$
Figure 4: $\mathbbmss{t}$-abstraction of the TFSM in Figure 3.

By applying the equivalence checking methodology presented in Section 2, we
can prove that the TFSM of Figure 3 is indeed equivalent to the TFSM of Figure
2(a). Figure 4 shows the $\mathbbmss{t}$-abstraction of the TFSM of Figure 3,
which is equivalent to the FSM of Figure 2(b) (by standard FSM state-
minimization of the FSM in Figure 4, we get a reduced FSM isomorphic to the
one in Figure 2(b)). This is consistent with the fact that the FSM of Figure
2(b) is the $\mathbbmss{t}$-abstraction of the TFSM of Figure 2(a).

##  4 Intersection of TFSMs

In this section we apply the previous transformations to perform the
intersection of TFSMs. In general, TFSMs can be composed to build complex
systems out of simpler components. Several composition operators exist for
untimed FSMs, the most relevant ones being the intersection operator, the
serial composition, and synchronous and asynchronous parallel composition (see
[40]). Parallel composition of TA was discussed in [35]. Preliminary work on
parallel composition of TFSMs with timed guards and output delays can be found
in [29], and on parallel composition of TFSMs with timeouts and output delays
in [26]. When extending compositions to Timed FSMs, one must verify that TFSMs
are closed under the type of composition of interest. In our setting, this
means that the behaviour of the composed system should be represented by a
machine with only a single clock. Here we focus on the intersection operator
for which we show that closure holds.

In the following we show how the transformation from TFSMs to untimed FSMs of
Section 2 and the transformation from untimed FSMs to TFSMs of Section 3 can
be used to implement the intersection of TFSMs. Suppose that we have two TFSMs
$M_{1}$ and $M_{2}$ and that we want to compute the intersection $M_{1}\cap
M_{2}$ whose behaviour is the intersection of the behaviours of $M_{1}$ and
$M_{2}$. We can proceed as follows:

  1. 1.

compute the $\mathbbmss{t}$-abstract FSMs $A_{M_{1}}$ and $A_{M_{2}}$ as in
Definition 3 for, respectively, $M_{1}$ and $M_{2}$;

  2. 2.

intersect $A_{M_{1}}$ and $A_{M_{2}}$ using the standard algorithm for untimed
FSMs, obtaining the untimed FSM $C=A_{M_{1}}\cap A_{M_{2}}$;

  3. 3.

compute the TFSM $T$ that is $\mathbbmss{t}$-bisimilar with $C$ using
Algorithm 1.

The following theorem shows that $T$ is equivalent to the intersection of
$M_{1}$ and $M_{2}$.

######  Theorem 3.

Let $M_{1}$ and $M_{2}$ be two deterministic TFSMs, and let
$T=\textsc{Refine}(A_{M_{1}}\cap A_{M_{2}})$. Then, for every timed input word
$v=(i_{1},t_{1})\dots(i_{k},t_{k})$ we have that
$B_{T}(v)=w=(o_{1},t_{1})\dots(o_{k},t_{k})$ if and only if $B_{M_{1}}(v)$ and
$B_{M_{2}}(v)$ are defined and such that $B_{M_{1}}(v)=B_{M_{2}}(v)=w$.

###### Proof.

Let $M_{1}$ and $M_{2}$ be two deterministic TFSMs, and let $A_{M_{1}}$ and
$A_{M_{2}}$ be their respective $\mathbbmss{t}$-abstractions. By Definition 3
we have that $A_{M_{1}}$ and $A_{M_{2}}$ are deterministic and time
progressive. Hence, the intersection $A_{M_{1}}\cap A_{M_{2}}$ is also
deterministic and time progressive and Algorithm 1 can be applied to obtain
the TFSM $T$.

To prove the direct implication, let $v=(i_{1},t_{1})\dots(i_{k},t_{k})$ be an
input timed word and suppose that $B_{T}(v)=w$ for some timed output word
$w=(o_{1},t_{1})\dots(o_{k},t_{k})$. Since $T=\textsc{Refine}(A_{M_{1}}\cap
A_{M_{2}})$, by Corollary 2 we have that $T$ refines $A_{M_{1}}\cap
A_{M_{2}}$. Hence, by Definition 6 we have that $B_{A_{M_{1}}\cap
A_{M_{2}}}(\mathbbmss{t}(v))=\mathbbmss{t}(B_{T}(v))=\mathbbmss{t}(w)$. Since
$A_{M_{1}}\cap A_{M_{2}}$ is the intersection of $A_{M_{1}}$ and $A_{M_{2}}$,
we have that
$B_{A_{M_{1}}}(\mathbbmss{t}(v))=B_{A_{M_{2}}}(\mathbbmss{t}(v))=\mathbbmss{t}(w)$.
Since $A_{M_{1}}$ and $A_{M_{2}}$ are the $\mathbbmss{t}$-abstraction of
$M_{1}$ and $M_{2}$, by Theorem 1 and Lemma 3 we have that
$\mathbbmss{t}(w)=B_{A_{M_{1}}}(\mathbbmss{t}(v)))=\mathbbmss{t}(B_{M_{1}}(v))$
and
$\mathbbmss{t}(w)=B_{A_{M_{2}}}(\mathbbmss{t}(v)))=\mathbbmss{t}(B_{M_{2}}(v))$.
This proves that $B_{M_{1}}(v)$ and $B_{M_{2}}(v)$ are defined and such that
$B_{M_{1}}(v)=B_{M_{2}}(v)=w$.

To prove the opposite implication, let $v=(i_{1},t_{1})\dots(i_{k},t_{k})$ be
an input timed word and suppose that $B_{M_{1}}(v)$ and $B_{M_{2}}(v)$ are
defined and such that $B_{M_{1}}(v)=B_{M_{2}}(v)=w$ for some timed output word
$w=(o_{1},t_{1})\dots(o_{k},t_{k})$. Since $A_{M_{1}}$ and $A_{M_{2}}$ are the
$\mathbbmss{t}$-abstraction of $M_{1}$ and $M_{2}$, by Theorem 1 and Lemma 3
we have that
$B_{A_{M_{1}}}(\mathbbmss{t}(v)))=\mathbbmss{t}(B_{M_{1}}(v))=\mathbbmss{t}(w)$
and
$B_{A_{M_{2}}}(\mathbbmss{t}(v)))=\mathbbmss{t}(B_{M_{2}}(v))=\mathbbmss{t}(w)$.
Hence, the intersection $A_{M_{1}}\cap A_{M_{2}}$ is such that
$B_{A_{M_{1}}\cap
A_{M_{2}}}(\mathbbmss{t}(v))=B_{A_{M_{1}}}(\mathbbmss{t}(v))=B_{A_{M_{2}}}(\mathbbmss{t}(v))=\mathbbmss{t}(w)$.
Since $T=\textsc{Refine}(A_{M_{1}}\cap A_{M_{2}})$, by Corollary 2 and
Definition 6 we have that $\mathbbmss{t}(B_{T}(v))=B_{A_{M_{1}}\cap
A_{M_{2}}}(\mathbbmss{t}(v))=\mathbbmss{t}(w)$. Hence, we have proved that
$B_{T}(v)=w$. ∎

As an example, consider the TFSMs $M_{1}$ and $M_{2}$ of Figure 5, and suppose
we want to compute the _intersection_ $M_{1}\cap M_{2}$. Following the above
procedure, the first step is to obtain the $\mathbbmss{t}$-abstract FSMs
$A_{M_{1}}$ and $A_{M_{2}}$ in Figure 6. Then, by applying the standard
constructions for intersection and minimization of untimed FSMs, we obtain the
machine $C$ depicted in Figure 7 and finally, using Algorithm 1, the TFSM
$T=\textsc{Refine}(A_{M_{1}}\cap A_{M_{2}})$ of Figure 8. It is worth pointing
out that the intersection of two complete and deterministic TFSMs is still a
deterministic machine, but it may be partial. This is indeed the case of our
example: for instance, when the TFSM in Figure 8 is in state $0$ it can react
to the input $i$ only when the clock is in the intervals $[0,0]$ or $(1,2)$.
No behaviour is specified when the clock is inside the interval $(0,1]$ and
$[2,3)$. In state $1$ and $13$ no behaviour is specified when the clock has an
integer value smaller than the timeout ($0,1,2$ and $3$ for state $1$, $0$ for
state $13$).

$M_{1}$$A$$B$$C$$[1,2):i/o_{2}$$t=2$$[0,1):i/o_{1}$$[0,\infty):i/o_{2}$$(0,1):i/o_{1}$$[0,0]:i/o_{2}$t=1

$M_{2}$$a$$[0,0]:i/o_{1}$$(0,1):i/o_{2}$$t=1$

Figure 5: TFSMs $M_{1}$ and $M_{2}$ to be intersected.

$A_{M_{1}}$$A$$[0,0]$$A$$(0,1)$$A$$[1,1]$$A$$(1,2)$$C$$[0,0]$$C$$(0,1)$$B$$[0,0]$$B$$(0,1)$$B$$[1,1]$$B$$(1,2)$$B$$[2,2]$$B$$(2,\infty)$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$i/o_{1}$$i/o_{1}$$i/o_{2}$$i/o_{2}$$i/o_{2}$$i/o_{1}$$i/o_{2}$$i/o_{2}\\!\\!\\!\\!$$i/o_{2}$$i/o_{2}$$i/o_{2}$$i/o_{2}$

$A_{M_{2}}$$a$$[0,0]$$a$$(0,1)$$i/o_{1}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$
$i/o_{2}$

Figure 6: Untimed abstractions of $M_{1}$ and $M_{2}$.
$C$$0$$1$$3$$5$$7$$9$$11$$13$$2$$4$$6$$8$$10$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$\mathbbmss{t}/\mathbbmss{t}$$i/o_{1}$$i/o_{2}$$i/o_{2}$$i/o_{2}$$i/o_{2}$
Figure 7: The intersection of $A_{M_{1}}$ and $A_{M_{2}}$. $M_{1}\cap
M_{2}$$0$$1$$13$$[0,0]:i/o_{1}$$(1,2):i/o_{2}$$t=3$$(0,1):i/o_{2}$
$(1,2):i/o_{2}$ $(2,3):i/o_{2}$ $(3,4):i/o_{2}$$t=4$$(0,1):i/o_{2}$$t=1$
Figure 8: The TFSM for ${M_{1}}\cap{M_{2}}$.

##  5 Timed FSMs and Timed Automata

In this section, we compare TFSMs with Timed Automata (TA), and survey the
known results on the expressivity and computability of various classes of TA,
according to their computational resources. The landscape of finite automata
augmented with time is much more complex than in the case of untimed ones,
where both language recognizers (FA) and producers (FSMs) share the fact that
there is an underlying common model with corresponds to regular languages
(FSMs transform regular input languages into regular output languages). TA are
the most common formalism obtained by adding timing constraints (as clocks) to
finite-state automata [3], defining timed regular recognizers. TA are a more
expressive model than TFSMs because they allow multiple clocks, invariants as
conditions on clocks associated to a location, guards as conditions on clocks
associated to a transition, resets by which a clock may be reset to $0$ or may
be kept unchanged, and states which are products of a location and clock
valuations. Excellent surveys about the classes of TA proposed in the
literature can be found in [24, 42].

TFSMs can be transformed into TA with $\varepsilon$-transitions (called also
in the literature silent transitions or internal transitions or non-observable
transitions) by the following transformation:

  * •

there is one location of the TA for every state of the TFSM;

  * •

given the input and output alphabets $I$ and $O$ of the TFSM, the alphabet of
the TA is given by $I\times O$

  * •

as in the TFSM, the TA has a single clock, reset to zero at every transition;

  * •

intervals on transitions are replaced with guards;

  * •

timeouts of the TFSM are replaced by invariants and $\varepsilon$\-
transitions.

An example of such transformation is shown in Fig. 9, where on the left there
is a TFSM and on the right the corresponding TA.

$s_{0}$$s_{1}$$[0,1):i/o_{1}$$t=1$$(1,\infty):i/o_{1}$$[0,1]:i/o_{2}$

$l_{0}$$x\leq 1$$l_{1}$ $x\leq\infty$$(i,o_{1}),\ x<1,\ x:=0$$\epsilon,\ x=1,\
x:=0$$(i,o_{1}),\ x>1,\ x:=0$$(i,o_{2}),\ x\leq 1,\ x:=0$

Figure 9: Transformation from TFSM (on the left) to $\epsilon$-timed automaton
(on the right).

This reduction is not necessarily practical, since decision problems are in
general undecidable for timed automata, even for restricted versions of them.
In the following we mention some of these relevant results. For a classic
survey on decision problems for timed automata, see [5], where the following
results can be found:

  1. 1.

TA are closed under union, intersection, projection, but not under
complementation.

  2. 2.

The language emptiness problems is PSPACE-complete (a by-product of
reachability analysis obtained by means of the region construction).

  3. 3.

The universality. inclusion and equivalence problems for TA are undecidable.

  4. 4.

Deterministic TA are closed under union. intersection and complementation, but
not under projection. The language emptiness, universality, inclusion and
equivalence problems for deterministic TA are PSPACE-complete.

Further results are proved in [22] and [23], e.g., that one cannot decide
whether a given timed automaton is determinizable or whether the complement of
a timed regular language is timed regular.

One may wonder whether the complexity goes down, if we reduce the resources of
the timed automaton. The answer is sometimes yes, but only in very restricted
cases. In [34, 1] it is shown that the problem of checking language inclusion
$L(A)\subseteq L(B)$ of TA $A$ and $B$ is decidable if $B$ has no
$\epsilon$-transitions. and either $B$ has only one clock, or the guards of
$B$ use only the constant 0. These two cases are essentially the only
decidable instances of language inclusion, in terms of restricting the various
resources of timed automata. Similar conclusions for the universality problem
(does a given TA accept all timed words) are drawn in [2]: the one-clock
universality problem is undecidable for TA over infinite words, and decidable
for TA over finite words, but undecidable for both if $\epsilon$-transitions
are allowed. Model checking and reachability of timed automata with one or two
clocks are discussed in [30, 21].

It is a fact that reducing resources, like the number of clocks, may simplify
some problems, but allowing $\epsilon$-transitions, even with few resources,
makes the problems as hard as in the general case. A score of papers [7, 8,
15, 9] investigated the expressiveness of timed automata augmented with
$\epsilon$-transitions, and proved the following results:

  1. 1.

The class of timed languages recognized by timed automata with
$\epsilon$-transitions is more robust and expressive than those without them.

  2. 2.

A timed automaton with $\epsilon$-transitions that do not reset clocks can be
transformed into an equivalent one without $\epsilon$-transitions (equivalent
means with the same timed language).

  3. 3.

A (non-Zenonian) timed automaton such that no $\epsilon$-transitions that
reset clocks lie on a direct cycle can be transformed into an equivalent one
without $\epsilon$-transitions.

  4. 4.

There is a timed automaton, with an $\epsilon$-transition which resets clocks
on a cycle, which is not equivalent to any timed automaton without
$\epsilon$-transitions.

More undecidability questions for timed automata with $\epsilon$-transitions
were answered in [11], e.g.: given a timed automaton with
$\epsilon$-transitions, it is undecidable to determine if there exists an
equivalent timed automaton without $\epsilon$-transitions.

The problem of removing $\epsilon$-transitions got a new twist in [17], where
it was shown that if one allows periodic clock constraints and periodic resets
(updates), then we can remove $\epsilon$-transitions from a timed automaton;
moreover, the authors proved that periodic updates are necessary, defining a
language that cannot be accepted by any timed automaton with periodic
constraints and transitions which reset clocks to 0 and no
$\epsilon$-transitions.

In conclusion, timed automata are a rich model with and without
$\epsilon$-transitions, therefore in general their decision problems are
undecidable or very difficult also for restricted versions, even more so if
$\epsilon$-transitions are admitted.

An interesting restricted model are Real-Time Automata (RTA) introduced by C.
Dima [16] in 2001: they are finite automata with a labeling function (from
states to an alphabet) and a time labeling function (from states to rational
intervals) which together define the label of a state. RTA work over signals
that are functions with finitely many discontinuities from non-negative
rational intervals $[0,e)$ (with $e>0$) to an alphabet, so that the domain of
a signal is partitioned into finitely many intervals where the signal is
constant. A run is associated with a signal iff there is a sequence of
partitioning points consistent with the state labels (stuttering, i.e.,
repetition of signal values is allowed); signals associated with an accepting
run are the timed language associated to an RTA. The author states in [16]
that RTA can be viewed as a class of state-labeled timed automata over timed
words (instead than signals) with a single clock which is reset at every
transition (stuttering being reduced to $\epsilon$-transitions). Moreover, it
is claimed that RTA are the largest timed extension of finite automata whose
emptiness and universality problems are decidable, $\epsilon$-transitions can
be removed, there is a determinization construction, are closed under
complementation, and a version of Kleene theorem holds.

More complex classes of timed automata have been studied, in which the
interplay between variants of the basic constituents defining them yields
interesting combinations of expressivity and computability.

Event-Clock Automata [4] (ECTA) are a determinizable robust subclass of timed
automata. Event-clock automata are characterized with respect to timed
automata by the fact that explicit resets of clocks are replaced by a
predefined association with the input symbols such that for each input
$x\in\Sigma$: a global recorder clock records the time elapsed since the last
occurrence of $x$ and a global predictor clock measures the time required for
the next occurrence of $x$ (clock valuations are determined only by the input
timed words). They are closed under Boolean operations (TA are not closed
under complement) and language inclusion is PSPACE-complete for them (it is
undecidable for TA). It is mentioned in [16] that RTA are incomparable with
ECTA, which are the largest known determinizable subclass of timed automata.
since RTA may accept languages that ECTA cannot.

Timed Automata with Non-Instantaneous Actions [6] are such that an action can
take some time to be completed; they are more expressive that timed automata
and less expressive than timed automata with $\epsilon$-transitions. Updatable
Timed Automata were introduced in [10] as an extension to update the clocks in
a more elaborate way than simply resetting them to 0; their emptiness problem
is undecidable, but there are interesting decidable subclasses. Any updatable
automaton belonging to some decidable subclass can be effectively transformed
into an equivalent timed automaton without updates, but with
$\epsilon$-transitions.

A complete taxonomy of timed automata is presented in [24], and issues of
undecidability are discussed in depth in [33]. Properties of timed automata
are contrasted in [13] with those of a special class of hybrid automata with
severe restrictions on the discrete transitions: hybrid systems with strong
resets, which have the property that all the continuous variables are non-
deterministically reset after each discrete transition, (differently from
timed automata, where flow rates are constant, and it is not compulsory to
reset variables on each discrete transition). Connections between timed
automata and timed discrete-event models are explored in [37].

The trade-off in preferring TA vs.TFSMs depends also on the specific problem
at hand. For instance, TA and TFSMs are used when deriving tests for discrete
event systems. However, methods for direct derivation of complete test suites
over TA return infinite test suites [38]. Therefore, to derive complete finite
test suites with a guaranteed fault coverage, a TA is usually converted to an
FSM and FSM-based test derivation is then used (see [36, 20]). Therefore,
TFSMs may be preferred over TA and other models when the derivation of
complete tests is required (as done in [19] for TFSMs with timed guards), even
though the test suites so obtained are rather long. We mention also that the
FSM abstraction introduced in this paper was used in [39], to derive complete
finite test suites for TFSMs with both timeouts and timed guards. Since FSMs
are used for testing, state distinguishability, and state identification
problems of hardware and software designs (see [31, 14, 28]), TFSMs may be
applied to the timed versions of these problems, instead than using TA.

##  6 Conclusions

We investigated deterministic TFSMs with a single clock, with both timed
guards and timeouts. We showed that the behaviours of the timed FSMs are
equivalent if and only if the behaviours of the companion untimed FSMs
obtained by time-abstracting bisimulations are equivalent, so that they
exhibit a good trade-off between expressive power and ease of analysis.

Then we defined and proved the correctness of the backward construction from
Untimed FSMs to TFSMs. The construction starts from any deterministic FSM
recognizing a subset of the language
$\left(\left(\nicefrac{{\mathbbmss{t}}}{{\mathbbmss{t}}}\right)^{*}\nicefrac{{I}}{{O}}\right)^{*}\left(\nicefrac{{\mathbbmss{t}}}{{\mathbbmss{t}}}\right)^{*}$
and builds a deterministic TFSM that recognizes the corresponding timed
language. Using the two constructions we showed how to intersect two
deterministic TFSMs, first by transforming them into untimed FSMs, then
applying the standard intersection algorithm for untimed FSMs, and then
transforming back into a deterministic TFSM.

Future work includes studying more general composition operators to define and
solve equations over deterministic TFSMs [41], and addressing the previous
problems for TFSMs with output delays [32] and nondeterministic TFSMs.

### Acknowledgements

Davide Bresolin and Tiziano Villa acknowledge partial support from the project
INdAM, GNCS 2020 (Strategic Reasoning and Automated Synthesis of Multi-Agent
Systems) funded by MIUR (Italian Ministry of Education, University and
Research). Tiziano Villa was partially supported by MIUR, “Project Italian
Outstanding Departments, 2018-2022”. Nina Yevtushenko was partly supported by
the Ministry of Science and Higher Education of the Russian Federation (grant
number 075-15-2020-788).

## References

  * [1] P. Abdulla, J. Deneux, J. Ouaknine, and J. Worrell.  Decidability and complexity results for timed automata via channel machines.  In L. Caires, G. Italiano, L. Monteiro, C. Palamidessi, and M. Yung, editors, Automata, Languages and Programming, volume 3580 of Lecture Notes in Computer Science, pages 1089–1101. Springer Berlin Heidelberg, 2005.
  * [2] P. A. Abdulla, J. Deneux, J. Ouaknine, K. Quaas, and J. Worrell.  Universality analysis for one-clock timed automata.  Fundam. Inform., 89(4):419–450, 2008.
  * [3] R. Alur and D. L. Dill.  A theory of timed automata.  Theoretical Computer Science, 126(2):183 – 235, 1994.
  * [4] R. Alur, L. Fix, and T. A. Henzinger.  Event-clock automata: A determinizable class of timed automata.  Theoretical Computer Science, 211(1-2):253–273, 1999.
  * [5] R. Alur and M. Parthasarathy.  Decision Problems for Timed Automata : A Survey, volume 3185 of Lecture Notes in Computer Science, pages 1–24.  Springer Verlag, 2004.
  * [6] R. Barbuti, N. De Francesco, and L. Tesei.  Timed automata with non-instantaneous actions.  Fundam. Inf., 47(3-4):189–200, Oct. 2001.
  * [7] B. Bérard, P. Gastin, and A. Petit.  On the power of non-observable actions in timed automata.  In Proceedings of the 13th Annual Symposium on Theoretical Aspects of Computer Science, STACS ’96, pages 257–268, London, UK, UK, 1996\. Springer-Verlag.
  * [8] B. Bérard, P. Gastin, and A. Petit.  Timed automata with non observable actions : expressive power and refinement.  Technical Report LIAFA 97/23, Université Denis Diderot (Paris), Paris, 1997.
  * [9] B. Bérard, A. Petit, V. Diekert, and P. Gastin.  Characterization of the expressive power of silent transitions in timed automata.  Fundam. Inf., 36(2,3):145–182, Aug. 1998.
  * [10] P. Bouyer, C. Dufourd, E. Fleury, and A. Petit.  Updatable timed automata.  Theoretical Computer Science, 321(2-3):291–345, 2004.
  * [11] P. Bouyer, S. Haddad, and P.-A. Reynier.  Undecidability results for timed automata with silent transitions.  Fundam. Inf., 92(1-2):1–25, Jan. 2009.
  * [12] D. Bresolin, K. El-Fakih, T. Villa, and N. Yevtushenko.  Deterministic timed finite state machines: Equivalence checking and expressive power.  In Proc. of the 5th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, September 10-12, 2014., volume 161 of EPTCS, pages 203–216, 2014.
  * [13] T. Brihaye, V. Bruyère, and E. Render.  Formal language properties of hybrid systems with strong resets.  RAIRO - Theor. Inf. and Applic., 44(1):79–111, 2010.
  * [14] T. S. Chow.  Testing software design modeled by finite-state machines.  IEEE Trans. Softw. Eng., SE-4(3):178–187, May 1978.
  * [15] V. Diekert, P. Gastin, and A. Petit.  Removing epsilon-transitions in timed automata.  In Proceedings of the 14th Annual Symposium on Theoretical Aspects of Computer Science, STACS ’97, pages 583–594, London, UK, UK, 1997\. Springer-Verlag.
  * [16] C. Dima.  Real-time automata.  Journal of Automata, Languages and Combinatorics, 6(1):3–24, 2001\.
  * [17] C. Dima and R. Lanotte.  Removing all silent transitions from timed automata.  In J. Ouaknine and F. W. Vaandrager, editors, FORMATS, volume 5813 of Lecture Notes in Computer Science, pages 118–132. Springer, 2009\.
  * [18] K. El-Fakih, M. Gromov, N. Shabaldina, and N. Yevtushenko.  Distinguishing experiments for timed nondeterministic finite state machines.  Acta Cybernetica, 212(2):205–222, 2013.
  * [19] K. El-Fakih, N. Yevtushenko, and A. Simao.  A practical approach for testing timed deterministic finite state machines with single clock.  Science of Computer Programming, 80, Part B(0):343 – 355, 2014\.
  * [20] A. En-Nouaary, R. Dssouli, and F. Khendek.  Timed Wp-Method: Testing Real-Time Systems.  IEEE Trans. Softw. Eng., 28(11):1023–1038, Nov. 2002.
  * [21] J. Fearnley and M. Jurdziński.  Reachability in two-clock timed automata is pspace-complete.  Information and Computation, 243(C):26–36, Aug. 2015.
  * [22] O. Finkel.  On decision problems for timed automata.  Bulletin of the EATCS, 87:185–190, 2005.
  * [23] O. Finkel.  Undecidable problems about timed automata.  In Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, September 25-27, 2006, Proceedings, pages 187–199, 2006.
  * [24] P. Fontana and R. Cleaveland.  A menagerie of timed automata.  ACM Comput. Surv., 46(3):40:1–40:56, Jan. 2014.
  * [25] M. Gromov, K. El-Fakih, N. Shabaldina, and N. Yevtushenko.  Distinguishing non-deterministic timed finite state machines.  In Formal Techniques for Distributed Systems, volume 5522 of Lecture Notes in Computer Science, pages 137–151. Springer Berlin Heidelberg, 2009.
  * [26] M. Gromov, A. Tvardovskii, and N. Yevtushenko.  Testing components of interacting timed finite state machines.  In 2016 IEEE East-West Design & Test Symposium (EWDTS), volume 00, pages 1–4, Oct. 2016.
  * [27] R. M. Hierons, M. G. Merayo, and M. Núñez.  Testing from a stochastic timed system with a fault model.  The Journal of Logic and Algebraic Programming, 78(2):98 – 115, 2009.
  * [28] Z. Kohavi and N. K. Jha.  Switching and Finite Automata Theory.  Cambridge University Press, 2009.
  * [29] O. Kondratyeva, N. Kushik, A. R. Cavalli, and N. Yevtushenko.  Evaluating web service quality using finite state models.  In 2013 13th International Conference on Quality Software, Najing, China, July 29-30, 2013, pages 95–102, 2013.
  * [30] F. Laroussinie, N. Markey, and P. Schnoebelen.  Model checking timed automata with one or two clocks.  In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR’04), volume 3170 of Lecture Notes in Computer Science, pages 387–401, Berlin, Heidelberg, 2004. Springer-Verlag.
  * [31] D. Lee and M. Yannakakis.  Principles and methods of testing finite state machines-a survey.  Proceedings of the IEEE, 84(8):1090–1123, 1996.
  * [32] M. G. Merayo, M. Núñez, and I. Rodríguez.  Formal testing from timed finite state machines.  Computer Networks, 52(2):432–460, 2008.
  * [33] J. S. Miller.  Decidability and complexity results for timed automata and semi-linear hybrid automata.  In Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control, HSCC ’00, pages 296–309, London, UK, UK, 2000\. Springer-Verlag.
  * [34] J. Ouaknine and J. Worrell.  On the language inclusion problem for timed automata: Closing a decidability gap.  In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS ’04, pages 54–63, Washington, DC, USA, 2004. IEEE Computer Society.
  * [35] J. Sifakis and S. Yovine.  Compositional specification of timed systems.  In C. Puech and R. Reischuk, editors, STACS 96, pages 345–359, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg.
  * [36] J. Springintveld, F. Vaandrager, and P. R. D’Argenio.  Testing timed automata.  Theoretical Computer Science, 254(1–2):225 – 257, 2001.
  * [37] C. Stergiou, S. Tripakis, E. Matsikoudis, and E. Lee.  On the verification of timed discrete-event models.  In V. Braberman and L. Fribourg, editors, Formal Modeling and Analysis of Timed Systems, volume 8053 of Lecture Notes in Computer Science, pages 213–227. Springer Berlin Heidelberg, 2013.
  * [38] J. Tretmans.  A formal approach to conformance testing.  PhD thesis, University of Twente, Tne Netherlands, 19922.
  * [39] A. Tvardovskii, K. El-Fakih, and N. Yevtushenko.  Deriving tests with guaranteed fault coverage for finite state machines with timeouts.  In I. Medina-Bulo, M. G. Merayo, and R. Hierons, editors, Testing Software and Systems, pages 149–154, Cham, 2018. Springer International Publishing.
  * [40] T. Villa, A. Petrenko, N. Yevtushenko, A. Mishchenko, and R. Brayton.  Component-based design by solving language equations.  Proceedings of the IEEE, 103(11):2152–2167, 2015.
  * [41] T. Villa, N. Yevtushenko, R. Brayton, A. Mishchenko, A. Petrenko, and A. Sangiovanni-Vincentelli.  The Unknown Component Problem: Theory and Applications.  Springer Verlag, 2012.
  * [42] M. T. B. Waez, J. Dingel, and K. Rudie.  A survey of timed automata for the development of real-time systems.  Computer Science Review, 9:1 – 26, 2013.
  * [43] M. Zhigulin, N. Yevtushenko, S. Maag, and A. Cavalli.  FSM-based test derivation strategies for systems with time-outs.  In Proc. of the 11th Int. Conf. on Quality Software (QSIC 2011), pages 141–149, 2011.