Some Observations on Frames and Observation Frames
by
M.M. Bonsangue
Vrije Universiteit Amsterdam

Frames can be thought as lattices of properties of a process. The underlying logic is geometric-i.e. with finite conjunctions and infinite disjunctions. However, infinite conjunctions as well as infinite disjunctions is often necessary for reasoning about liveness and fairness properties of a process. Recently, observation frames have been introduced as an extension of ordinary frames in order to describe infinite conjunctions. A full subcategory of observation frames has been shown to be dual to the category of T₀ topological spaces.

In this lecture we show how to construct the free observation frame from a given frame in a such way that ``points'' are preserved. Also, we show that there is a monadic functor from the category of observation frames to the category whose objects are all onto functions from one set X to a second set Y with the evident arrows (commutative squares) between these objects.

These results can then be applied for extending Abramsky's finitary logic of domains to an infinitary one preserving soundness and completeness.

Date received: April 12, 1996

Copyright © 1996 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # caae-06.