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.)

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).

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).

**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.

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

- 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.

## No comments:

## Post a Comment