Mirror, mirror in my hand: a duality between specifications and models of process behaviour
- 1 August 1996
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 6 (4) , 353-373
- https://doi.org/10.1017/s0960129500001067
Abstract
Summary: 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.Keywords
This publication has 11 references indexed in Scilit:
- Institutions for behaviour specificationPublished by Springer Nature ,1995
- A classification of models for concurrencyLecture Notes in Computer Science, 1993
- Process semantics of temporal logic specificationPublished by Springer Nature ,1993
- Composing specificationsACM Transactions on Programming Languages and Systems, 1993
- Temporal theories as modularisation units for concurrent system specificationFormal Aspects of Computing, 1992
- Object interactionPublished by Springer Nature ,1992
- A categorial theory of objects as observed processesPublished by Springer Nature ,1991
- On the relation of programs and computations to models of temporal logicPublished by Springer Nature ,1989
- Introducing institutionsPublished by Springer Nature ,1984
- Categories for the Working MathematicianPublished by Springer Nature ,1971