# The shrinktech Tool

## Example

Non-shrinkability of timed automata can be due either to the disappearance of
a finite behaviour, or that of an infinite behaviour.
We illustrate the first kind of non-shrinkability here; the user guide
contains an example to the second one.

Let us describe a simple system that is not shrinkable. We
consider the timed automaton A of the figure below.
The system has to give a feedback (fb) at least every 2 time
units, through the self-loop on ℓ_{0}. At any time, it can receive a
message m, which it can transfer to another system after a delay of at least 1 and at
most 2. In fact, let us assume that the target system only listens between
this time interval. If the message is sent too early or too late, it will be
lost. In addition, while the system is in the state ℓ_{1} preparing for transferring the
message, it can decide to send the message to a buffer by realizing
the btransfer action as long as *x*≤ 1.
The sytem may also receive a dupplicate (m′) of the message while 1≤ *x*≤ 2.

A good implementation must only

transfer the message when

*x* ∈ [1+δ, 2−
δ] for a safe δ>0, and should always give the feedback when

*y*≤
2− δ. Hence it makes sense to do shrinkability analysis on this system to
check whether any significant behaviour is lost under shrinking.

To simplify the discussion, we will only concentrate on a simple behaviour
of _{2}, and summarize it as the timed automaton in the figure
below.
This timed automaton consists of the unfolding of the above one for two
transitions from ℓ_{1}.
By investigating the state space of _{2}, one can see that it contains a
branching: at ℓ_{1}, both btransfer and
transfer actions are available. The state space is illustrated in
the figure below.
On the other hand,
under any shrinking, the branching btransfer and transfer is disabled
(the right of the figure).
This means that a controller that waits for the repetition of the message before making the
decision between btransfer and transfer is not robust.
Therefore, the timed automaton is not shrinkable w.r.t.
its own time-abstract behaviour.
Note however that the shrunk automaton does contain the behaviours
m·m′· transfer
and m·m′· btransfer
so if the branching is not important, one can eliminate the branching in the
time-abstract bisimulation quotient and prove shrinkability w.r.t. this smaller
finite automaton.

The figure on left illustrates the behaviour in the original timed
automaton, while on the right, the behaviour of the shrunk automaton is
given.
The red area is the guard of btransfer, while the blue area is the
guard of transfer. The thick black segment is a set of states
reachable after the action m′.
From this set, both actions transfer and btransfer are
available in the original timed automaton, while the latter is disabled in
the shrunk automaton. Hence, the branching disappears under any shrinking. |

Shrinktech main page