An equivalent CTL formulation for condition sequences

Jeffrey Ashley, Lawrence E. Holloway

Research output: Contribution to journalArticlepeer-review

1 Scopus citations


A condition system is a form of Petri net that interacts with other condition systems and the environment via state-based signals called conditions. The condition language framework has been used in previous papers to characterize the input/output behavior of such interacting systems, as well as to specify desired control behavior among other things. In this paper, we show that condition sequences (the specification) and condition systems (the model of the system) have an equivalent structure in the computation tree logic (CTL) framework. The primary goals of this work are to be able to utilize existing tools for program verification for our systems, and to make our work more accessible to the temporal logic community.

Original languageEnglish
Pages (from-to)333-348
Number of pages16
JournalDiscrete Event Dynamic Systems: Theory and Applications
Issue number4
StatePublished - Dec 2005

Bibliographical note

Funding Information:
This work has been supported in part by the National Science Foundation grant ECS-0115694, Office of Naval Research N000140110621, and the Center for Manufacturing at the University of Kentucky.


  • Computation tree logic (CTL)
  • Condition systems
  • Discrete event systems (DES)
  • Temporal logic

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Modeling and Simulation
  • Electrical and Electronic Engineering


Dive into the research topics of 'An equivalent CTL formulation for condition sequences'. Together they form a unique fingerprint.

Cite this