Mirror, mirror in my hand: a duality between specifications and models of process behaviour

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 -