Hierarchical synthesis of hybrid controllers from temporal logic specifications

Georgios Fainekos, Antoine Girard, George J. Pappas

Research output: Chapter in Book/Report/Conference proceedingConference contribution

24 Citations (Scopus)

Abstract

In this paper, the problem of synthesizing a hybrid controller for a specification expressed as a temporal logic formula ø is considered. We propose a hierarchical approach which consists of three steps. First, the plant to be controlled is abstracted to a fully actuated system. Using the notion of approximate simulation relation, we design a continuous interface allowing the plant to track the trajectories of its abstraction with a guaranteed precision δ. The second step, which is also the main contribution of this paper, consists in deriving a more robust specification ø from the temporal logic formula ø such that given a trajectory satisfying ø′ any other trajectory remaining within distance S satisfies ø. Third, we design a hybrid controller for the abstraction such that all its trajectories satisfy the robust specification ø′. Then, the trajectories of the plant satisfy the original specification. An application to the control of a second order model of a planar robot in a polygonal environment is considered.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages203-216
Number of pages14
Volume4416 LNCS
StatePublished - 2007
Externally publishedYes
Event10th International Conference on Hybrid Systems: Computation and Control, HSCC 2007 - Pisa, Italy
Duration: Apr 3 2007Apr 5 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4416 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other10th International Conference on Hybrid Systems: Computation and Control, HSCC 2007
CountryItaly
CityPisa
Period4/3/074/5/07

Fingerprint

Temporal logic
Temporal Logic
Trajectories
Trajectory
Synthesis
Specification
Specifications
Controller
Controllers
Second-order Model
Robot
Robots
Simulation

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Fainekos, G., Girard, A., & Pappas, G. J. (2007). Hierarchical synthesis of hybrid controllers from temporal logic specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4416 LNCS, pp. 203-216). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4416 LNCS).

Hierarchical synthesis of hybrid controllers from temporal logic specifications. / Fainekos, Georgios; Girard, Antoine; Pappas, George J.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4416 LNCS 2007. p. 203-216 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4416 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Fainekos, G, Girard, A & Pappas, GJ 2007, Hierarchical synthesis of hybrid controllers from temporal logic specifications. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 4416 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4416 LNCS, pp. 203-216, 10th International Conference on Hybrid Systems: Computation and Control, HSCC 2007, Pisa, Italy, 4/3/07.
Fainekos G, Girard A, Pappas GJ. Hierarchical synthesis of hybrid controllers from temporal logic specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4416 LNCS. 2007. p. 203-216. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Fainekos, Georgios ; Girard, Antoine ; Pappas, George J. / Hierarchical synthesis of hybrid controllers from temporal logic specifications. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4416 LNCS 2007. pp. 203-216 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{8724b018442949399d05b9da484aa6aa,
title = "Hierarchical synthesis of hybrid controllers from temporal logic specifications",
abstract = "In this paper, the problem of synthesizing a hybrid controller for a specification expressed as a temporal logic formula {\o} is considered. We propose a hierarchical approach which consists of three steps. First, the plant to be controlled is abstracted to a fully actuated system. Using the notion of approximate simulation relation, we design a continuous interface allowing the plant to track the trajectories of its abstraction with a guaranteed precision δ. The second step, which is also the main contribution of this paper, consists in deriving a more robust specification {\o} from the temporal logic formula {\o} such that given a trajectory satisfying {\o}′ any other trajectory remaining within distance S satisfies {\o}. Third, we design a hybrid controller for the abstraction such that all its trajectories satisfy the robust specification {\o}′. Then, the trajectories of the plant satisfy the original specification. An application to the control of a second order model of a planar robot in a polygonal environment is considered.",
author = "Georgios Fainekos and Antoine Girard and Pappas, {George J.}",
year = "2007",
language = "English (US)",
isbn = "9783540714927",
volume = "4416 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "203--216",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Hierarchical synthesis of hybrid controllers from temporal logic specifications

AU - Fainekos, Georgios

AU - Girard, Antoine

AU - Pappas, George J.

PY - 2007

Y1 - 2007

N2 - In this paper, the problem of synthesizing a hybrid controller for a specification expressed as a temporal logic formula ø is considered. We propose a hierarchical approach which consists of three steps. First, the plant to be controlled is abstracted to a fully actuated system. Using the notion of approximate simulation relation, we design a continuous interface allowing the plant to track the trajectories of its abstraction with a guaranteed precision δ. The second step, which is also the main contribution of this paper, consists in deriving a more robust specification ø from the temporal logic formula ø such that given a trajectory satisfying ø′ any other trajectory remaining within distance S satisfies ø. Third, we design a hybrid controller for the abstraction such that all its trajectories satisfy the robust specification ø′. Then, the trajectories of the plant satisfy the original specification. An application to the control of a second order model of a planar robot in a polygonal environment is considered.

AB - In this paper, the problem of synthesizing a hybrid controller for a specification expressed as a temporal logic formula ø is considered. We propose a hierarchical approach which consists of three steps. First, the plant to be controlled is abstracted to a fully actuated system. Using the notion of approximate simulation relation, we design a continuous interface allowing the plant to track the trajectories of its abstraction with a guaranteed precision δ. The second step, which is also the main contribution of this paper, consists in deriving a more robust specification ø from the temporal logic formula ø such that given a trajectory satisfying ø′ any other trajectory remaining within distance S satisfies ø. Third, we design a hybrid controller for the abstraction such that all its trajectories satisfy the robust specification ø′. Then, the trajectories of the plant satisfy the original specification. An application to the control of a second order model of a planar robot in a polygonal environment is considered.

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

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

M3 - Conference contribution

AN - SCOPUS:38049104000

SN - 9783540714927

VL - 4416 LNCS

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

SP - 203

EP - 216

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

ER -