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