202310101410

Tags : Timed Automata

---

Zone Automata

Consider this Example. It shows that having a Reachability Axiom is Important for software verification purposes.

Region Automata is Too Inefficient!

Lets say we have a Network of 10 Timed Automata, and each of these have 10 states. All of them have a single clock and the maximum number present guards of all of the automata is 2.

A naïve way would be to first construct a Monolithic Automata which accepts the same language.

The above construction gives $10^{10}$ states, with 10 clock and guards having the maximum number $2$.

The time bound that for Region automata construction would give time around $10!\cdot 2^{10}\cdot 10^{10}$. Doing a reachability check in this automata is not feasible. A better approach is required $!!$

Much like Region Automata, Zone Automata also makes an Untimed Finite State Automaton given a Timed Automaton by combining states with a set of clock configurations to represent time.

Tldr: Zones

Zones are sets in the Clock Space, which represent the set of clock configurations, these are obtained by

• Starting with a set of points
• Taking away the points that do not satisfy guards when the transition is taken
• Then adding points that can be achieved by waiting. i.e the future operator.

Zones

A Zone is a set of clock valuations. We define $3$ operations of zones to help us model the configuration of clocks for a run in a timed automaton.

• Intersection of two zones $W$ and $W^{\prime }$
• Resets of a subset of clocks to $0$ in $W$
• Future of $W$: $\overrightarrow{W}=\{v+\delta |v\in W,\delta \in {\mathbb{R}}^{+}\}$

using these three operations, we will emulate the change in a zone caused by a transition. Given a transition $t=⟨q,g,Y,q^{\prime }⟩$ we define

$${\text{Post}}_t(W)=\overrightarrow{[Y](W\cap \text{textlbrackdbl}g\text{textrbrackdbl})}$$

where $[Y]$ denotes the resets and $\text{textlbrackdbl}g\text{textrbrackdbl}$ denotes the zone that is satisfied by $g$.

idea

$(q,Z)\stackrel{\text{guards}}{\to }(q,Z\cap \text{textlbrackdbl}g\text{textrbrackdbl})\stackrel{\text{resets}}{\to }(q,[Y](Z\cap \text{textlbrackdbl}g\text{textrbrackdbl}))\stackrel{\text{elapse}}{\to }(q,\overrightarrow{[Y](Z\cap \text{textlbrackdbl}g\text{textrbrackdbl})})$

Zone Automata

Let $(q,Z)$ be a symbolic state where $q$ is a state and $Z$ is a zone. Let $s_0=(q_0,\overrightarrow{\{\text{0}\}})$ be the initial state. Then the set of reachable symbolic states $\mathcal{S}$ is given by

$$\frac{}{s_0\in \mathcal{S}}\text{Init}$$ $$\frac{\begin{array}{ccccc}(q,Z)\in \mathcal{S}& & t=(q,g,Y,q^{\prime })& & Z^{\prime }={\text{Post}}_t(Z)\ne \varnothing \end{array}}{(q^{\prime },Z^{\prime })\in \mathcal{S}}\text{Trans}$$

Whenever we derive a symbolic state using the $\text{Trans}$ rule we also get a corresponding transition in the zone automata between the symbolic states.

Now we can start building our Reachability Algorithm for Zone Automata

But this method does not terminate. The two main approaches to that problem are extrapolation and simulation.

Zone Automata Example

---

References

Zone Automata Example Extrapolation for Zone Automata Simulation for Zone Automata Reachability Algorithm for Zone Automata