An equivalent LTL/Kripke structure for the condition sequence/condition system model

Jeff Ashley, L. E. Holloway

Research output: Contribution to journalConference articlepeer-review

1 Scopus citations


A condition system is a form of Petri net that interacts with other condition systems and the environment via input and output signals called conditions. The Condition Language framework has been used in previous papers to characterize t he input/output behavior of such interacting systems, as well as to specify desired control behavior. In this paper, we show that condition sequences (the specificat ion) and condition systems (the model of the system) have an equivalent structure in the temporal logic framework. In part icular, we show that there exists a linear-time temporal logic (LTL) specification and a Kripke structure that represents our specification and model.

Original languageEnglish
Pages (from-to)57-62
Number of pages6
JournalIFAC Proceedings Volumes (IFAC-PapersOnline)
Issue number18
StatePublished - 2004
Event7th International Workshop on Discrete Event Systems, WODES 2004 - Reims, France
Duration: Sep 22 2004Sep 24 2004

Bibliographical note

Publisher Copyright:
© 2004 IFAC.


  • Condition systems
  • Languages
  • Linear temporal logic
  • Petri nets

ASJC Scopus subject areas

  • Control and Systems Engineering


Dive into the research topics of 'An equivalent LTL/Kripke structure for the condition sequence/condition system model'. Together they form a unique fingerprint.

Cite this