LTLC: Linear temporal logic for control

Young Min Kwon; Gul Agha

doi:10.1007/978-3-540-78929-1_23

LTLC: Linear temporal logic for control

Young Min Kwon, Gul Agha

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Linear systems are one of the most commonly used models to represent physical systems. Yet, only few automated tools have been developed to check their behaviors over time. In this paper, we propose a linear temporal logic for specifying complex properties of discrete time linear systems. The proposed logic can also be used in a control system to generate control input in the process of model checking. Although, developing a full feedback control system is beyond the scope of this paper, authors believe that a feedback loop can be easily introduced by adopting the receding horizon scheme of predictive controllers. In this paper we explain the syntax, the semantics, a model checking algorithm, and an example application of our proposed logic.

Original language	English (US)
Title of host publication	Hybrid Systems
Subtitle of host publication	Computation and Control - 11th International Workshop, HSCC 2008, Proceedings
Publisher	Springer
Pages	316-329
Number of pages	14
ISBN (Print)	3540789286, 9783540789284
DOIs	https://doi.org/10.1007/978-3-540-78929-1_23
State	Published - 2008
Event	11th International Workshop on Hybrid Systems: Computation and Control, HSCC 2008 - St. Louis, MO, United States Duration: Apr 22 2008 → Apr 24 2008

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4981 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	11th International Workshop on Hybrid Systems: Computation and Control, HSCC 2008
Country/Territory	United States
City	St. Louis, MO
Period	4/22/08 → 4/24/08

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-540-78929-1_23

Library availability

Discover UIUC Full Text

Cite this

Kwon, Y. M., & Agha, G. (2008). LTLC: Linear temporal logic for control. In Hybrid Systems: Computation and Control - 11th International Workshop, HSCC 2008, Proceedings (pp. 316-329). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4981 LNCS). Springer. https://doi.org/10.1007/978-3-540-78929-1_23

LTLC: Linear temporal logic for control. / Kwon, Young Min; Agha, Gul.
Hybrid Systems: Computation and Control - 11th International Workshop, HSCC 2008, Proceedings. Springer, 2008. p. 316-329 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4981 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kwon, YM & Agha, G 2008, LTLC: Linear temporal logic for control. in Hybrid Systems: Computation and Control - 11th International Workshop, HSCC 2008, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4981 LNCS, Springer, pp. 316-329, 11th International Workshop on Hybrid Systems: Computation and Control, HSCC 2008, St. Louis, MO, United States, 4/22/08. https://doi.org/10.1007/978-3-540-78929-1_23

@inproceedings{719376ca207848a2a9d5409d610b1599,

title = "LTLC: Linear temporal logic for control",

abstract = "Linear systems are one of the most commonly used models to represent physical systems. Yet, only few automated tools have been developed to check their behaviors over time. In this paper, we propose a linear temporal logic for specifying complex properties of discrete time linear systems. The proposed logic can also be used in a control system to generate control input in the process of model checking. Although, developing a full feedback control system is beyond the scope of this paper, authors believe that a feedback loop can be easily introduced by adopting the receding horizon scheme of predictive controllers. In this paper we explain the syntax, the semantics, a model checking algorithm, and an example application of our proposed logic.",

author = "Kwon, {Young Min} and Gul Agha",

note = "Copyright: Copyright 2021 Elsevier B.V., All rights reserved.; 11th International Workshop on Hybrid Systems: Computation and Control, HSCC 2008 ; Conference date: 22-04-2008 Through 24-04-2008",

year = "2008",

doi = "10.1007/978-3-540-78929-1_23",

language = "English (US)",

isbn = "3540789286",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "316--329",

booktitle = "Hybrid Systems",

address = "Germany",

}

TY - GEN

T1 - LTLC

T2 - 11th International Workshop on Hybrid Systems: Computation and Control, HSCC 2008

AU - Kwon, Young Min

AU - Agha, Gul

PY - 2008

Y1 - 2008

N2 - Linear systems are one of the most commonly used models to represent physical systems. Yet, only few automated tools have been developed to check their behaviors over time. In this paper, we propose a linear temporal logic for specifying complex properties of discrete time linear systems. The proposed logic can also be used in a control system to generate control input in the process of model checking. Although, developing a full feedback control system is beyond the scope of this paper, authors believe that a feedback loop can be easily introduced by adopting the receding horizon scheme of predictive controllers. In this paper we explain the syntax, the semantics, a model checking algorithm, and an example application of our proposed logic.

AB - Linear systems are one of the most commonly used models to represent physical systems. Yet, only few automated tools have been developed to check their behaviors over time. In this paper, we propose a linear temporal logic for specifying complex properties of discrete time linear systems. The proposed logic can also be used in a control system to generate control input in the process of model checking. Although, developing a full feedback control system is beyond the scope of this paper, authors believe that a feedback loop can be easily introduced by adopting the receding horizon scheme of predictive controllers. In this paper we explain the syntax, the semantics, a model checking algorithm, and an example application of our proposed logic.

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

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

U2 - 10.1007/978-3-540-78929-1_23

DO - 10.1007/978-3-540-78929-1_23

M3 - Conference contribution

AN - SCOPUS:70350004055

SN - 3540789286

SN - 9783540789284

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 316

EP - 329

BT - Hybrid Systems

PB - Springer

Y2 - 22 April 2008 through 24 April 2008

ER -

LTLC: Linear temporal logic for control

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this