An Action Logic for Real-Time Reasoning

Fernando Naufel do Amaral & Edward Hermann Haeusler

In [3], Segerberg introduced the notion of a “bringing-it-about” δ operator, which, when applied to a given proposition q, denotes the set of actions that bring about the truth of q. In this paper, we discuss the use of a similar operator in a logical framework having computational transition systems as its semantics.

Segerberg’s δ operator has led to an extension of dynamic logic containing elements from logics of action, where δp denotes actions that lead to states where q holds. In [1, 2], the operator was extended in two different ways: the first extension was introduced to reason about preconditions as well as postconditions, with the dyadic form pδq. The second extension, concerned with real-time applications, added a minimal and a maximal delay for the occurrence of each action: here, the action term p_{l}δ^{u}q denotes the actions that achieve q in less than u units of time, provided they were enabled in states satisfying p for at least l units of time.

In [1, 2], this last extension was dubbed RETOOL (Real-Time Object-Oriented Logic, in reference to the ultimate goal of achieving a formalization of object-oriented software). The exact denotation of an action term pδq, however, has not been agreed upon. Two different semantics have been proposed for RETOOL. This paper presents yet a third one with soundness and completeness proofs regarding timed transition systems. It is also shown how this action logic can be combined with a temporal logic to derive temporal properties of actions from the logical description of a real-time computational system.

[1] Carvalho, S., Fiadeiro, J. and Haeusler, E.H., “A Formal Approach to Real-Time Object-Oriented Software”, in Proc. 22nd IFAC/IFIP Workshop on Real-Time Programming WRTP’97, Elsevier 1997.

[2] Fiadeiro, J. and Haeusler, E.H., “Bringing It About On Time (Extended Abstract)”, in Proc. I IMLLAI, Fortaleza, CE, Brazil, 1998.

[3] Segerberg, K., “Bringing It About”, in Journal of Philosophical Logic 18, 1989.

Addresses Fernando Naufel do Amaral: Department of Informatics, Catholic University of Rio de Janeiro, Rio de Janeiro, BRAZIL

E-mail: fnaufel@inf.puc-rio.br

Edward Hermann Haeusler: Department of Informatics, Catholic University of Rio de Janeiro, Rio de Janeiro, BRAZIL

E-mail: hermann@inf.puc-rio.br