Temporal Logic Control of Discrete-Time Piecewise Affine Systems

YORDANOV, Boyan; Jana TŮMOVÁ; Ivana ČERNÁ; Jiří BARNAT a Calin BELTA. Temporal Logic Control of Discrete-Time Piecewise Affine Systems. IEEE Transactions on Automatic Control. PISCATAWAY, 2012, roč. 57, č. 6, s. 1491-1504. ISSN 0018-9286. Dostupné z: https://doi.org/10.1109/TAC.2011.2178328.

Základní údaje

Originální název

Temporal Logic Control of Discrete-Time Piecewise Affine Systems

Autoři

YORDANOV, Boyan; Jana TŮMOVÁ; Ivana ČERNÁ ORCID; Jiří BARNAT a Calin BELTA

Vydání

IEEE Transactions on Automatic Control, PISCATAWAY, 2012, 0018-9286

---

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Impakt faktor

Impact factor: 2.718

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/12:00057211

Organizační jednotka

Fakulta informatiky

DOI

https://doi.org/10.1109/TAC.2011.2178328

UT WoS

000304609300012

Klíčová slova anglicky

Control design; discrete time systems; formal specifications; piecewise linear approximation

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

We present a computational framework for automatic synthesis of a feedback control strategy for a discrete-time piece-wise affine (PWA) system from a specification given as a linear temporal logic (LTL) formula over an arbitrary set of linear predicates in the system's state variables. Our approach consists of two main steps. First, by defining appropriate partitions for its state and input spaces, we construct a finite abstraction of the PWA system in the form of a control transition system. Second, by leveraging ideas and techniques from LTL model checking and Rabin games, we develop an algorithm to generate a control strategy for the finite abstraction. While provably correct and robust to state measurements and small perturbations in the applied inputs, the overall procedure is conservative and expensive. The proposed algorithms have been implemented as a software package and made available for download. Illustrative examples are included.

---

Návaznosti

GAP202/11/0312, projekt VaV	Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems) Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
GD102/09/H042, projekt VaV	Název: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
LH11065, projekt VaV	Název: Řízení a ověřování vlastností komplexních hybridních systémů (Akronym: Řízení a ověřování vlastností komplexních hybridní) Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Řízení a ověřování vlastností komplexních hybridních systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
MUNI/A/0914/2009, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty