Region (model checking) explained

In model checking, a field of computer science, a region is a convex polytope in

Rd

for some dimension

d

, and more precisely a zone, satisfying some minimality property. The regions partition

Rd

.

The set of zones depends on a set

K

of constraints of the form

x\lec

,

x\gec

,

x1\lex2+c

and

x1\gex2+c

, with

x1

and

x2

some variables, and

c

a constant. The regions are defined such that if two vectors

\vecx

and

\vecx'

belong to the same region, then they satisfy the same constraints of

K

. Furthermore, when those vectors are considered as a tuple of clocks, both vectors have the same set of possible futures. Intuitively, it means that any timed propositional temporal logic-formula, or timed automaton or signal automaton using only the constraints of

K

can not distinguish both vectors.

The set of region allows to create the region automaton, which is a directed graph in which each node is a region, and each edge

r\tor'

ensure that

r'

is a possible future of

r

. Taking a product of this region automaton and of a timed automaton

lA

which accepts a language

L

creates a finite automaton or a Büchi automaton which accepts untimed

L

. In particular, it allows to reduce the emptiness problem for

lA

to the emptiness problem for a finite or Büchi automaton. This technique is used for example by the software UPPAAL.[1]

Definition

Let

C=\{x1,...,xd\}

a set of clocks. For each

x\inN

let

cx\inN

. Intuitively, this number represents an upper bound on the values to which the clock

x

can be compared. The definition of a region over the clocks of

C

uses those numbers

cx

's. Three equivalent definitions are now given.

Given a clock assignment

\nu

,

[\nu]

denotes the region in which

\nu

belongs. The set of regions is denoted by

lR

.

Equivalence of clocks assignment

The first definition allow to easily test whether two assignments belong to the same region.

A region may be defined as an equivalence class for some equivalence relation. Two clocks assignments

\nu1

and

\nu2

are equivalent if they satisfy the following constraints:[2]

\nu1(x)\simc

iff

\nu2(x)\simc

, for each

x\inC

and

0\lec\lecx

an integer, and ~ being one of the following relation =, < or .

\{\nu1(x)\}\sim\{\nu1(y)\}

iff

\{\nu2(x)\}\sim\{\nu2(y)\}

, for each

x,y\inC

,

\nu1(x)\lecx

,

\nu1(y)\lecy

,

\{r\}

being the fractional part of the real

r

, and ~ being one of the following relation =, < or .

The first kind of constraints ensures that

\nu1

and

\nu2

satisfies the same constraints. Indeed, if

\nu1(x)=0.5

and

\nu2(x)=1

, then only the second assignment satisfies

x=1

. On the other hand, if

\nu1(x)=0.5

and

\nu2(x)=0.6

, both assignment satisfies exactly the same set of constraint, since the constraints use only integral constants.

The second kind of constraints ensures that the future of two assignments satisfy the same constraints. For example, let

\nu1=\{x\mapsto0.5,y\mapsto0.6\}

and

\nu2=\{x\mapsto0.5,y\mapsto0.4\}

. Then, the constraint

y=1\landx<1

is eventually satisfied by the future of

\nu1

without clock reset, but not by the future of

\nu2

without clock reset.

Explicit definition of a region

While the previous definition allow to test whether two assignments belong to the same region, it does not allow to easily represents a region as a data structure. The third definition given below allow to give a canonical encoding of a region.

A region can be explicitly defined as a zone, using a set

S

of equations and inequations satisfying the following constraints:

x\inC

,

S

contains either:

x=c

for some integer

0\lec\lecx

x\in(c,c+1)

for some integer

0\lec<cx

,

x>cx

,

x,y\inC

, where

S

contains constraints of the form

x\in(c,c+1)

and

y\in(c',c'+1)

, then

S

contains an (in) equality of the form

\{x\}\sim\{y\}

with

\sim

being either =, < or .

Since, when

c

and

c'

are fixed, the last constraint is equivalent to

x\simy+c-c'

.

This definition allow to encode a region as a data structure. It suffices, for each clock, to state to which interval it belongs and to recall the order of the fractional part of the clocks which belong in an open interval of length 1. It follows that the size of this structure is

O\left(\sumlog(ck)+|C|log(|C|)\right)

with

|C|

the number of clocks.

Timed bisimulation

Let us now give a third definition of regions. While this definition is more abstract, it is also the reason why regions are used in model checking. Intuitively, this definition states that two clock assignments belong to the same region if the differences between them are such that no timed automaton can notice them. Given any run

r

starting with a clock assignment

\nu

, for any other assignment

\nu'

in the same region, there is a run

r'

, going through the same locations, reading the same letters, where the only difference is that the time waited between two successive transition may be different, and thus the successive clock variations are different.

The formal definition is now given. Given a set of clock

C

, two assignments two clocks assignments

\nu1

and

\nu2

belongs to the same region if for each timed automaton

lA

in which the guards never compare a clock

x

to a number greater than

cx

, given any location

\ell

of

lA

, there is a timed bisimulation between the extended states

(\ell,\nu1)

and

(\ell,\nu2)

. More precisely, this bisimulation preserves letters and locations but not the exact clock assignments.

Operation on regions

Some operations are now defined over regions: Resetting some of its clock, and letting time pass.

Resetting clocks

Given a region

\alpha

defined by a set of (in)equations

S

, and a set of clocks

C'\subseteqC

, the region similar to

\alpha

in which the clocks of

C'

are restarted is now defined. This region is denoted by

\alpha[C'\mapsto0]

, it is defined by the following constraints:

S

not containing the clock

x

,

x=0

for

x\inC'

.

The set of assignments defined by

\alpha[C'\mapsto0]

is exactly the set of assignments

\nu[C'\mapsto0]

for

\nu\in\alpha

.

Time-successor

Given a region

\alpha

, the regions which can be attained without resetting a clock are called the time-successors of

\alpha

. Two equivalent definitions are now given.

Definition

A clock region

\alpha'

is a time-successor of another clock region

\alpha

if for each assignment

\nu\in\alpha

, there exists some positive real

t\nu,\alpha'>0

such that

\nu+t\nu,\alpha'\in\alpha'

.

Note that it does not mean that

\alpha+t\nu,\alpha'=\alpha'

. For example, the region

\alpha

defined by the set of constraint

\{0<x<1,0<y<1,x<y\}

has the time-successor

\alpha'

defined by the set of constraint

\{0<x<1,y=1\}

. Indeed, for each

\nu\in\alpha

, it suffices to take

t\nu,\alpha'=1-\nu(y)

. However, there exists no real

t

such that

\alpha+t=\alpha'

or even such that

\alpha+t\subseteq\alpha'

; indeed,

\alpha

defines a triangle while

\alpha'

defines a segment.

Computable definition

The second definition now given allow to explicitly compute the set of time-successor of a region, given by its set of constraints.

Given a region

\alpha

defined as a set of constraints

S

, let us define its set of time-successors. In order to do so, the following variables are required. Let

T\subseteqS

the set of constraints of

S

of the form

xi=ci

. Let

Y\subseteqC

the set of clocks

y

such that

S

contains the constraint

y>cy

. Let

Z\subseteqC\setminusY

the set of clocks

\{z\}

such that there are no constraints of the form

\{x\}<\{z\}

in

S

.

If

T

is empty,

\alpha

is its own time successor. If

Y=C

, then

\alpha

is the only time-successor of

\alpha

. Otherwise, there is a least time-successor of

\alpha

not equal to

\alpha

. The least time-successor, if

T

is non-empty, contains:

S\setminusT

xi>ci

,

\{xi\}=\{xj\}

, and

y

such that

y>cy

does not belong to

S

, the constraint

xi<y

.If

T

is empty, the least time-successor is defined by the following constraints:

S

not using the clocks of

Z

,

z=c+1

, for each constraint

c<z<c+1

in

S

, with

z\inZ

.

Properties

There are at most

|C|!2|C|\prodx\in(2cx+2)

regions, where

|C|

is the number of clocks.

Region automaton

Given a timed automaton

lA

, its region automaton is a finite automaton or a Büchi automaton which accepts untimed

L

. This automaton is similar to

lA

, where clocks are replaced by region. Intuitively, the region automaton is contructude as a product of

lA

and of the region graph. This region graph is defined first.

Region graph

The region graph is a rooted directed graph which models the set of possible clock valuations during a run of a timed-autoamton. It is defined as follows:

\alpha0

, defined by the set of constraints

\{x=0\midx\inC\}

,

(\alpha,\alpha'[C'\mapsto0])

, for

\alpha'

a time-successor of

\alpha

.

Region automaton

Let

lA=\langle\Sigma,L,L0,C,F,E\rangle

a timed automaton. For each clock

x\inC

, let

cx

the greatest number

c

such that there exists a guard of the form

x\simc

in

lA

. The region automaton of

lA

, denoted by

R(lA)

is a finite or Büchi automaton which is essentially a product of

lA

and of the region graph defined above. That is, each state of the region automaton is a pair containing a location of

lA

and a region. Since two clocks assignment belonging to the same region satisfies the same guard, each region contains enough information to decide which transitions can be taken.

Formally, the region automaton is defined as follows:

\Sigma

,

L x lR

,

L0 x \{\alpha0\}

with

\alpha0

the initial region,

F x lR

,

\delta

contains

((\ell,\alpha),a,(\ell',\alpha'[C'\mapsto0]))

, for

(\ell,a,g,C',\ell')\inE

, such that

\gamma\models\alpha'

and

\alpha'

is a time-successor of

\alpha

.

Given any run

r=(\ell0,\nu0)\xrightarrow[t1]{\sigma1}(\ell1,\nu1)...

of

lA

, the sequence

(\ell0,[\nu0])\xrightarrow{\sigma1}(\ell1,[\nu1])...

is denoted

[r]

, it is a run of

R(lA)

and is accepting if and only if

r

is accepting. It follows that

L(R(lA))=\operatorname{Untime}(L(lA))

. In particular,

lA

accepts a timed-word if and only if

R(lA)

accepts a word. Furthermore, an accepting run of

lA

can be computed from an accepting run of

R(lA)

.

References

  1. Book: Bengtsson . Johan . Yi . Wang L . Lectures on Concurrency and Petri Nets . Timed Automata: Semantics, Algorithms and Tools . Lecture Notes in Computer Science . 2004 . 3098 . 87–124 . 10.1007/978-3-540-27755-2_3 . 978-3-540-22261-3 . http://www.it.uu.se/research/group/darts/papers/texts/by-lncs04.ps.
  2. Alur . Rajeev . Dill . David L . A theory of timed automata . Theoretical Computer Science . April 25, 1994 . 126 . 2 . 183–235 . 10.1016/0304-3975(94)90010-8 . free .