Formal Analysis of Piecewise Affine Systems through Formula-Guided Refinement

YORDANOV, Boyan, Jana TŮMOVÁ, Calin BELTA, Ivana ČERNÁ and Jiří BARNAT. Formal Analysis of Piecewise Affine Systems through Formula-Guided Refinement. In Proceedings of of the 49th IEEE Conference on Decision and Control (CDC). Neuveden: Omnipress for IEEE Control Systems Society, 2010, p. 5899-5904. ISBN 978-1-4244-7744-9.

Basic information

Original name

Formal Analysis of Piecewise Affine Systems through Formula-Guided Refinement

Name in Czech

Formální analýza po částech afinních systémů s použitím formulí řízeného zjemnění

Authors

YORDANOV, Boyan (100 Bulgaria), Jana TŮMOVÁ (203 Czech Republic, guarantor, belonging to the institution), Calin BELTA (840 United States of America), Ivana ČERNÁ (203 Czech Republic, belonging to the institution) and Jiří BARNAT (203 Czech Republic, belonging to the institution)

Edition

Neuveden, Proceedings of of the 49th IEEE Conference on Decision and Control (CDC), p. 5899-5904, 6 pp. 2010

Publisher

Omnipress for IEEE Control Systems Society

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

RIV identification code

RIV/00216224:14330/10:00045258

Organization unit

Faculty of Informatics

ISBN

978-1-4244-7744-9

ISSN

UT WoS

000295049106108

Keywords in English

Automata; Genetic regulatory systems; Hybrid Systems;

Tags

International impact, Reviewed

---

Abstract

V originále

We present a computational framework for identifying a set of initial states from which all trajectories of a piecewise affine (PWA) system satisfy a Linear Temporal Logic (LTL) formula over a set of linear predicates in its state variables. Our approach is based on the construction and refinement of finite abstractions of infinite systems. We derive conditions guaranteeing the equivalence of an infinite system and its finite abstraction with respect to a specific temporal logic formula and propose methods aimed at the construction of such formula-equivalent abstractions. We show that the proposed procedure can be implemented using polyhedral operations and analysis of finite graphs. While provably correct, the overall method is conservative and expensive. The proposed algorithms have been implemented as a software tool that is available for download. An illustrative example for a PWA gene network model is included.

---

Links

GA201/09/1389, research and development project	Name: Verifikace a analýza velmi velkých počítačových systémů Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems
GP201/09/P497, research and development project	Name: Automatizovaná formální verifikace s využitím soudobého hardware Investor: Czech Science Foundation, Automated formal verification using modern hardware
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
MUNI/A/0914/2009, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV) Investor: Masaryk University, Category A