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

Abstract

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)
Volume37
Issue number18
DOIs
StatePublished - 2004
Event7th International Workshop on Discrete Event Systems, WODES 2004 - Reims, France
Duration: Sep 22 2004Sep 24 2004

Bibliographical note

Funding Information:
1 Email: holloway:1'i'engr.uky.edu. Supported in part by Rockwell International. "SF grant ECS-9S0il06 and ECS-0115694, the Office of \'aval Research under the grant :\'000140110621, and the Center for :\1anufacturing at the universitv of Kentuckv. 2 Email: ·jashley:1'igw~ail.kysu.edu.

Publisher Copyright:
© 2004 IFAC.

Keywords

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

ASJC Scopus subject areas

  • Control and Systems Engineering

Fingerprint

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