Information Technology Reference
In-Depth Information
Eleanor looked down at the worn wooden bench, where some young wit
had recorded his ignorance of biology. \But what about all that necessity of
necessity stu? It can't have any real eect, can it?" \Well, he was talk-
ing about the way the behaviour is modelled and how the way the model is
expressed changes the range of behaviours you would consider as being the
same. If you can show a rule for simplifying the description of behaviour
always holds, even if it is seemingly quite obscure, it may be the key to sim-
plifying the description and so proving it satisfies the objectives. If I know
that I can just replace necessarily necessary with necessary, then I've got a
tactic for rewriting the description in a simpler form, where it may be more
obvious that two terms are the same." Eleanor was still not satised. \But
isn't it obvious they mean the same?" \Unfortunately not. There are a num-
ber of formal descriptions of necessity and possibility, which can be arranged
as a family depending on the assumptions you make. Unfortunately, this very
point is one of the distinguishing features of subfamilies you get by including
or excluding particular axioms."
By now it was dark outside the high windows and only the group round
the whiteboard remained, and it was thinning out. They were now drawing
complex expressions consisting almost entirely of stars, arrows and brackets.
\OK," Claire said, \but what about the worlds with no future?" \One of
the ways of clarifying what possibility and necessity means is to talk in terms
of what is sometimes called a possible-worlds model. It is made up of nodes
representing possible states of the system as a whole, expressed as frames
giving a list of statements that say how the state is expressed and markings
saying which of these are true in a particular situation. These nodes are then
linked by arcs that indicate whether one description can evolve into another.
If we have such a model, we can define our terms in a simple way. Something
is possible in a given state if there is at least one way the system can evolve
that would make it true, and it is necessary if there is no way evolution can
make it false. This is a very powerful way of analysing properties of behaviour,
and is very important for toolbuilders. The tag he quoted is not very useful
in itself, but helps students remember the denitions. If a state can't evolve
at all because it has no outgoing arcs, it clearly has no successor where a
statement is false, so anything you want to consider is necessary."
A porter had come in at the lower door and was cleaning the boards.
\Come on, they want to turn the lights out, and I've talked for long enough.
Let's go and have a drink."
14.1
The Importance of Formal Models
So far, we have described the basic conceptual tools needed to describe a
system. Here, we look behind the scenes a little, to explain how some of the
