The Expressive Power of Temporal Logic of Actions

2002 ◽  
Vol 12 (5) ◽  
pp. 839-859 ◽  
Author(s):  
A. Estrin
Keyword(s):  
Temporal Logic ◽  
Expressive Power ◽  
Temporal Logic Of Actions

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

1996 ◽  
Vol 6 (4) ◽  
pp. 353-373 ◽  
Author(s):  
J. L. Fiadeiro ◽  
J. F. Costa
Keyword(s):  
Temporal Logic ◽  
Structural Property ◽  
Reactive Systems ◽  
Expressive Power ◽  
Seminal Paper ◽  
Process Specification ◽  
Temporal Specifications ◽  
Mirror Mirror

SummarySince 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.

Sign in / Sign up

Export Citation Format

Share Document