An equivalent CTL formulation for condition sequences

Jeffrey Ashley; Lawrence E. Holloway

doi:10.1007/s10626-005-4056-0

An equivalent CTL formulation for condition sequences

Jeffrey Ashley, Lawrence E. Holloway

Institute for Sustainable Manufacturing (ISM)

Research output: Contribution to journal › 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 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 language	English
Pages (from-to)	333-348
Number of pages	16
Journal	Discrete Event Dynamic Systems: Theory and Applications
Volume	15
Issue number	4
DOIs	https://doi.org/10.1007/s10626-005-4056-0
State	Published - 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.

Funding

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.

Funders	Funder number
Center for Manufacturing
U.S. Department of Energy Chinese Academy of Sciences Guangzhou Municipal Science and Technology Project Oak Ridge National Laboratory Extreme Science and Engineering Discovery Environment National Science Foundation National Energy Research Scientific Computing Center National Natural Science Foundation of China	ECS-0115694
Office of Naval Research Naval Academy	N000140110621

Keywords

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

Access to Document

10.1007/s10626-005-4056-0

Cite this

@article{fdc5773391184ac2bfa6b6a08568499d,

title = "An equivalent CTL formulation for condition sequences",

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

keywords = "Computation tree logic (CTL), Condition systems, Discrete event systems (DES), Temporal logic",

author = "Jeffrey Ashley and Holloway, \{Lawrence E.\}",

year = "2005",

month = dec,

doi = "10.1007/s10626-005-4056-0",

language = "English",

volume = "15",

pages = "333--348",

number = "4",

}

TY - JOUR

T1 - An equivalent CTL formulation for condition sequences

AU - Ashley, Jeffrey

AU - Holloway, Lawrence E.

PY - 2005/12

Y1 - 2005/12

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

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

KW - Computation tree logic (CTL)

KW - Condition systems

KW - Discrete event systems (DES)

KW - Temporal logic

UR - https://www.scopus.com/pages/publications/26444615378

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

U2 - 10.1007/s10626-005-4056-0

DO - 10.1007/s10626-005-4056-0

M3 - Article

AN - SCOPUS:26444615378

SN - 0924-6703

VL - 15

SP - 333

EP - 348

JO - Discrete Event Dynamic Systems: Theory and Applications

JF - Discrete Event Dynamic Systems: Theory and Applications

IS - 4

ER -

An equivalent CTL formulation for condition sequences

Abstract

Bibliographical note

Funding

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this