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

Jeff Ashley; L. E. Holloway

doi:10.1016/S1474-6670(17)30722-X

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

Jeff Ashley, L. E. Holloway

Institute for Sustainable Manufacturing (ISM)

Research output: Contribution to journal › Conference article › peer-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 language	English
Pages (from-to)	57-62
Number of pages	6
Journal	IFAC Proceedings Volumes (IFAC-PapersOnline)
Volume	37
Issue number	18
DOIs	https://doi.org/10.1016/S1474-6670(17)30722-X
State	Published - 2004
Event	7th International Workshop on Discrete Event Systems, WODES 2004 - Reims, France Duration: Sep 22 2004 → Sep 24 2004

Bibliographical note

Publisher Copyright:
© 2004 IFAC.

Keywords

Condition systems
Languages
Linear temporal logic
Petri nets

ASJC Scopus subject areas

Control and Systems Engineering

Access to Document

10.1016/S1474-6670(17)30722-X

Cite this

@article{2791dfb9e1cb4549a2ac6d3395537a98,

title = "An equivalent LTL/Kripke structure for the condition sequence/condition system model",

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.",

keywords = "Condition systems, Languages, Linear temporal logic, Petri nets",

author = "Jeff Ashley and Holloway, {L. E.}",

note = "Publisher Copyright: {\textcopyright} 2004 IFAC.; 7th International Workshop on Discrete Event Systems, WODES 2004 ; Conference date: 22-09-2004 Through 24-09-2004",

year = "2004",

doi = "10.1016/S1474-6670(17)30722-X",

language = "English",

volume = "37",

pages = "57--62",

number = "18",

}

TY - JOUR

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

AU - Ashley, Jeff

AU - Holloway, L. E.

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

KW - Condition systems

KW - Languages

KW - Linear temporal logic

KW - Petri nets

UR - http://www.scopus.com/inward/record.url?scp=26444478604&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=26444478604&partnerID=8YFLogxK

U2 - 10.1016/S1474-6670(17)30722-X

DO - 10.1016/S1474-6670(17)30722-X

M3 - Conference article

AN - SCOPUS:26444478604

SN - 1474-6670

VL - 37

SP - 57

EP - 62

JO - IFAC Proceedings Volumes (IFAC-PapersOnline)

JF - IFAC Proceedings Volumes (IFAC-PapersOnline)

IS - 18

T2 - 7th International Workshop on Discrete Event Systems, WODES 2004

Y2 - 22 September 2004 through 24 September 2004

ER -

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

Abstract

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this