Game Development Reference

In-Depth Information

the maximal equivalence relation

on
V
such that any two equivalent nodes

satisfy the same unary predicates
P
i
and have edges into the same equivalence

classes. To put it differently,

∼

∼

is the greatest fixed-point of the refinement

operator
F
:

P

(
V

×

V
)

→P

(
V

×

V
) with

(
u, v
)

V
:
i≤m
P
i
u

F
:
Z

→

∈

V

×

↔

P
i
v

∧∀u
(
Euu
→∃v
(
Evv
∧ Zu
v
))

Zu
v
))
.

v
(
Evv
→∃

u
(
Euu
∧

∧∀

For some applications (one of which will appear in Section 4.6.4) one is

interested in having not only the bisimulation relation

∼

but also a linear

order on the bisimulation quotient

K

/
∼
. That is, we want to define a pre-

order

u
. We can again do this via

a fixed-point construction, by defining a sequence

on

K

such that
u

∼

v
iff
u

v
and
v

α
of pre-orders (where
α

ranges over ordinals) such that

α
+1
refines

α
and

λ
, for limit ordinals
λ
,

is the intersection of the pre-orders

α
with
α<λ
. Let

P
i
v

P
i
v
)

u

1
v
:

⇐⇒

P
i
u

→

∨

(

¬

P
j
u

∧

i≤m

j<i

(i.e., if the truth values of the
P
i
at
u
are lexicographically smaller than or

equal to those at
v
), and for any
α
, let

u

∼
α
v
:

⇐⇒

u

α
v

∧

v

α
u.

To define the refinement, we say that the
∼
α
-class
C separates
two nodes
u

and
v
, if precisely one of the two nodes has an edge into
C
. Now, let
u
α
+1
v

if, and only if,
u
α
v
and there is an edge from
v
(and hence none from
u
)

into the smallest

α
) that separates
u
from
v
(if it exists).

Since the sequence of the pre-orders

∼
α
-class (w.r.t.

α
is decreasing, it must indeed reach a

fixed-point

, and it is not hard to show that the corresponding equivalence

relation is precisely the bisimilarity relation

∼

.

is a deflationary fixed-point

of a non-monotone induction. Indeed, the refinement operator on pre-orders

is not monotone and does not, in general, have a greatest fixed-point. We

remark that is not di
cult to give an analogous definition of this order by

an inflationary, rather than deflationary induction.

The point that we want to stress here is that

The lazy engineer: iterated relativisation.
Let
ϕ
(
x
) be a specification that

should be satisfied by all states
a
of a system, which we assume to be

described as a relational structure

. Now, suppose that the engineer notices

that the system he designed is faulty, i.e., that there exist elements
a

A

∈
A

Search Nedrilad ::

Custom Search