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)

Producción científica: Conference article › revisión exhaustiva

1 Cita (Scopus)

Resumen

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.

Idioma original	English
Páginas (desde-hasta)	57-62
Número de páginas	6
Publicación	IFAC Proceedings Volumes (IFAC-PapersOnline)
Volumen	37
N.º	18
DOI	https://doi.org/10.1016/S1474-6670(17)30722-X
Estado	Published - 2004
Evento	7th International Workshop on Discrete Event Systems, WODES 2004 - Reims, France Duración: sept 22 2004 → sept 24 2004

Nota bibliográfica

Publisher Copyright:
© 2004 IFAC.

Financiación

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.

Financiadores	Número del financiador
Rockwell International Corporation	ECS-0115694, :\'000140110621, ECS-9S0il06

ASJC Scopus subject areas

Control and Systems Engineering

Acceder al documento

10.1016/S1474-6670(17)30722-X

Otros archivos y enlaces

Citar esto

@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 - https://www.scopus.com/pages/publications/26444478604

UR - https://www.scopus.com/pages/publications/26444478604#tab=citedBy

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

Resumen

Nota bibliográfica

Financiación

ASJC Scopus subject areas

Acceder al documento

Otros archivos y enlaces

Huella

Citar esto