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

José Luiz Fiadeiro, José Félix Costa

Research output: Contribution to journalArticle

20 Citations (Scopus)

Abstract

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.
Original languageEnglish
Pages (from-to)353-373
Number of pages21
JournalMathematical Structures in Computer Science
Volume6
Issue number4
DOIs
Publication statusPublished - Aug 1996

Fingerprint Dive into the research topics of 'Mirror, mirror in my hand: a duality between specifications and models of process behaviour'. Together they form a unique fingerprint.

  • Cite this