TY - JOUR
T1 - Mirror, mirror in my hand
T2 - a duality between specifications and models of process behaviour
AU - Fiadeiro, José Luiz
AU - Costa, José Félix
PY - 1996/8
Y1 - 1996/8
N2 - Since Pnueli’s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, ‘sound and complete’ with respect to process specification and interconnection techniques.
AB - Since Pnueli’s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, ‘sound and complete’ with respect to process specification and interconnection techniques.
U2 - 10.1017/S0960129500001067
DO - 10.1017/S0960129500001067
M3 - Article
SN - 0960-1295
VL - 6
SP - 353
EP - 373
JO - Mathematical Structures in Computer Science
JF - Mathematical Structures in Computer Science
IS - 4
ER -