next up previous
Next: ``Branching time'' and ``linear Up: Extensions of the formalism Previous: Concurrency

Events whose occurrence depends on the past

 

Suppose we want George to unblock both vents when the room becomes stuffy. When he has unblocked one vent, the room becomes unstuffy, so the physical situation is as it was when he blocked the first vent, so he needs to remember that the room was previously stuffy. We can make occurrences depend on past situations by adding for each event e an additional effect axiom

  equation437

Notice that Past(Past,s)) is the situation two events back.

We can have George unblock Vent1 after he has unblocked Vent2 and the room has become unstuffy by introducing the occurrence axiom

  equation441

The history as just described does not say what events occurred. This information is provided by having for each event e the axiom

  equation445

Notice that this formalization is noncommittal as to whether the information is in an actor's memory.

This seems neat, and maybe it will be useful.



John McCarthy
Fri Feb 8 17:29:20 PST 2002