Open Systems Laboratory at Illinois

Ltlc: linear temporal logic for control

By YoungMin Kwon and Gul Agha. In HSCC, volume 4981 of Lecture Notes in Computer Science, 316–329. Springer, 2008.

Full Text:
Download PDF
Publisher Link:


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, YoungMin and Agha, Gul",
    editor = "Egerstedt, Magnus and Mishra, Bud",
    title = "LTLC: Linear Temporal Logic for Control",
    booktitle = "HSCC",
    crossref = "conf/hybrid/2008",
    ee = "",
    keywords = "formal methods",
    pages = "316-329",
    year = "2008",

    editor = "Egerstedt, Magnus and Mishra, Bud",
    title = "Hybrid Systems: Computation and Control, 11th
             International Workshop, HSCC 2008, St. Louis, MO, USA, April
             22-24, 2008. Proceedings",
    isbn = "978-3-540-78928-4",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "4981",
    year = "2008",