Comportamento e estado

Abstract

Neste trabalho é apresentada uma nova forma de especificar o comportamento de sistemas computacionais usando, para isso, uma lógica com características especiais. A unidade básica de especificação do comportamento é o agente, que formalmente é um sistema lógico. A linguagem lógica dos agentes permite exprimir o relacionamento entre a ocorrência de eventos e as propriedades exibidas pelo agente. Os eventos são entendidos como conectivas lógicas e as asserções lógicas reflectem a noção de causalidade entre eventos e propriedades — a causa essencial de uma propriedade face a um evento. Devido a estarmos interessados em saber que encadeamento de eventos “justifica” uma dada propriedade, temos traços que evoluem do passado para o presente. A nossa pres pectiva é a de saber que comportamento poderá justificar as características de um agente num dado instante. Como é óbvio, essas características condicionam o comportamento futuro do agente e essa dependência é expressa num sistema de dedução que refiecte a noção de causa. No intuíto de caracterizar semanticamente os agentes, é feita a ligação entre o sistema lógico e os seus modelos topológicos. A dualidade de Stone assegura a sintonia entre o sistema lógico e a sua semântica, e faculta-nos duas perspectivas: a perspectiva algébrica da lógica e a perspectiva topológica. São apresentados dois tipos de modelos para os agentes: os modelos de traços, perten centes à classe das semãnticas denotacionais, intirnamente ligados à noção de evento e traço; e os modelos de estados, pertencentes à classe das sernânticas operacionais, baseados na noção de estado e transição de estado. Estabelece-se uma relação entre estes dois tipos de modelos: irenios ver como podem ruos obter um modelo de estados, partindo de um modelo de traços. Os estados surgem aqui como classes de equivalência de comportamentos passados. São também estudadas as propriedades dos modelos assim gerados. Nomeadamente, é feita uma análise de como propriedades topológicas — tais como: condições de separação, sobriedade ou coerência — caracterizam o espaço de estados de tais modelos, e de como a partir do comportamento se consegue gerar o espaço de estados mínimo.

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.