INVESTIGADORES
FRIAS Marcelo Fabian
artículos
Título:
A Logic for RealTime Systems Specification, its Algebraic Semantics and Equational Calculus
Autor/es:
BAUM, GABRIEL; FRIAS, MARCELO FABIAN; MAIBAUM, THOMAS STEPHEN EDWARD
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer
Referencias:
Año: 1999 vol. 1548 p. 91 - 105
ISSN:
0302-9743
Resumen:
We present a logic for real time systems specification which
is an extension of first order dynamic logic by adding (a) arbitrary atomic
actions rather than only assignments, (b) variables over actions which
allow to specify systems partially, and (c) explicit time. The logic is
algebraized using closure fork algebras and a representation theorem for
this class is presented. This allows to define an equational (but infinitary)
proof system for the algebraization.