FMCAD 2004 START ConferenceManager    


An Operational Semantics for Weak PSL

Koen Claessen and Johan Mårtensson

Presented at Formal Methods in Computer-Aided Design (FMCAD 2004), Austin, Texas, November 14-17, 2004


Abstract

Extending linear temporal logic by adding regular expressions increases its expressiveness. However, as for example, problems in recent versions of Accellera's Property Specification Language (PSL) as well as in OpenVera's ForSpec and other property languages show, it is a non-trivial task to give a formal denotational semantics with desirable properties to the resulting logic. In this paper, we argue that specifying an {\em operational semantics} may be helpful in guiding this work, and as a bonus leads to an implementation of the logic for free. We give a concrete operational semantics for {\em Weak PSL}, which is the safety property subset of PSL. We also propose a denotational semantics which we show to be equivalent to the operational one. This semantics is inspired by a new denotational semantics proposed in recent related work.


  
START Conference Manager (V2.46.3)
Maintainer: sanders@cs.ubc.ca