Maria João Frade

Citation:

Frade MJ.  1995.  Comportamento e Estado.

Thesis Type:

Abstract:

In this work we introduce a formalism for specifying the behaviour of computational systems, based on logic.
Our basic unit of software specification is called agent and is nothing more than a particular logical system. The agent logical language allow us to express the relationship between the occurrence of events and the properties an agent exhibits. The events are seen as logical connectives and the logical assertions reflect the causality between events and properties - the essential cause of a property in face of an event.
Because we are interested in knowing which sequence of events “justify” a property, we have traces coming from the past to the present. Our perspective is that of knowing which behaviour could justify the characteristics of au agent in some instant. Obviously, these characteristics will condition the future behaviour of the agent. This dependency is expressed in a deduction system that reflects the notion of causality.
For the purpose of characterizing the agents semantically a connection is made between the logical system and its topological models. The Stone duality provides a junction between the logical system and its semantics and it provides two alternative perspectives:
the algebraic or logical perspective and the topological perspective.
We present two types of models for the agents: the trace model, a denotational model intimately connected to the notion of event and trace, and the state model, au operational model based on the notions of state and state transitions.
We establish a relation between these two types of models: we see how a state model may be obtained from a trace model. The states arise as equivalence classes of past behaviours. We also study the properties of the state models which result from the conversion of trace models. We see how topological properties — such as separation conditions, soberty and coherence — characterize the state space of these modeis, and how from behaviour we can generate a minimal state space.

Citation Key: