Affordable Access

Publisher Website

Specification in CTL+Past for Verification in CTL

Authors
Journal
Information and Computation
0890-5401
Publisher
Elsevier
Publication Date
Volume
156
Identifiers
DOI: 10.1006/inco.1999.2817
Disciplines
  • Linguistics
  • Mathematics

Abstract

Abstract We describe PCTL, a temporal logic extending CTL with connectives allowing to refer to the past of a current state. This incorporates the new N, “from now on,” combinator we recently introduced. PCTL has a branching future, but a determined, finite, and cumulative past. We argue this is the right choice for a semantical framework and show this through an extensive example. We investigate the feasibility of verification with PCTL and demonstrate how a translation-based approach allows model-checking specifications written in NCTL, a fragment of PCTL.

There are no comments yet on this publication. Be the first to share your thoughts.

Statistics

Seen <100 times
0 Comments

More articles like this

Specification in CTL+Past, Verification in CTL

on Electronic Notes in Theoretica... Jan 01, 1997

Local Module Checking for CTL Specifications

on Electronic Notes in Theoretica... Jan 01, 2007
More articles like this..