Region Automata and Zone Automata

As a sequel of a previous article on timed automaton (link), here we introduce its computational models.

1. Region

Why region automata? Timed automata have infinite state space (time be divided into infinite pieces), region automata give a finite partition of timed automata such that the computation becomes possible.

Intuition A region is a set of equivalent states. The partition divides the state space into different equivalent classes (regions).

Temporal constraint given by this grammar $\phi := x > c | x < c | x = c | \phi \wedge \phi$, $c$ must be an integer constant (to ensure non-zenoness)

Equivalent class The set of states which satisfies the same set of temporal constraints.

Region equivalence states are equivalent due to being in the same region, they are either within the integer grid, on the $x=c$ or $y=c$ axes, or above/below the diagonal of the integer grid. (see Figure 1.)

Fig 1. Regions as equivalent classes

Remind that largest constant relevant $c$ is actually the ceiling of $x_i$, i.e. $c = \lceil x_i \rceil$. Figure 2 is an example of partitions (regions) of the state space of a timed automaton. Not only are those shadowed areas regions, but also segments of lines (they usually are a result of clock resetting).

Fig 2. Regions on a 2-clock timed automaton

A further example Figure 3 shows the region representation of a simple timed automaton. Location $F$ is shadowed since it may loop forever, a bad design (livelock).

Fig 3. Timed automaton represented in regions

Time-abstract bisimulation If $w \simeq v$, $w,v \in l$, 1) after action $a$, $w'$ is in the region of location $l'$, so is $v'$; 2) $\forall d \exists d' . w+d \simeq v+d'$. They are respectively the transition on action and the transition on delay.

Region equivalence relation is a time-abstract bisimulation ($\simeq$).

Region reset The clock for all equivalent states is reset, hence the operation projects the whole region onto the clock axis (i.e. a line of shadow).

2. Zone

Why zone automata? Regions are still too many, we can force them collapse into unions of regions, where the unions are convex, i.e. no angles are larger than 180 degrees.

Zone Zones are so-called symbolic state (conjunction of regions). Formally, $Z = (s, \varphi)$, that is to start from a location (state) $s$ in a timed automaton, we make a conjunction of regions specified by temporal constraint $\varphi$.

Zone automaton A transition system for zones. Formally, $Z = (Q, Q^0, \Sigma, R)$, set of zones, initial zone, set of transition labels, transition relation.

Symbolic transition It may involve operations such as intersection (conjuncts), delay (stretches diagonally as x,y propagate in time simultaneously), reset (projects a shadow on the time axis). For a zone $Z = (s, \varphi)$, the transition is denoted as $\mathsf{succ}(\varphi, e)$, where $e$ is the label of switch. When $e$ is executed, $Z$ propagates by time till the time constraint $\varphi$ is met. The action is thus invoked. Proceed with a reset if it is needed.

Fig 4. Transitions on Zone Automaton

Figure 4 showed a symbolic transition from location n to m, i.e. $(n, 1 \leqslant x \leqslant 4, 1 \leqslant y \leqslant 3) \rightarrow (m, x>3,y=0)$

References

1. R. Sebastiani, Timed and Hybrid Systems: Formal Modeling and Verification, slides of Formal Methods course, 2012, link

Appendix

The most of this post is heavily extracted from the RS's teaching slides, hence I don't claim the copyright. The character of this post is intended to be a note, with marginal and personal remarks. For those who need to respect the source, please refer the link in the references.