Advanced search
Start date
Betweenand
Related content
(Reference retrieved automatically from Web of Science through information on FAPESP grant and its corresponding number as mentioned in the publication by the authors.)

Generating invariants for non-linear hybrid systems

Full text
Author(s):
Rebiha, Rachid [1] ; Moura, Arnaldo V. [1] ; Matringe, Nadir [2]
Total Authors: 3
Affiliation:
[1] Univ Estadual Campinas, Inst Comp, Sao Paulo - Brazil
[2] Univ Poitiers, Lab Math & Applicat, Poitiers - France
Total Affiliations: 2
Document type: Journal article
Source: THEORETICAL COMPUTER SCIENCE; v. 594, p. 180-200, AUG 23 2015.
Web of Science Citations: 3
Abstract

We describe powerful computational techniques, relying on linear algebraic methods, for generating ideals of non-linear invariants of algebraic hybrid systems. We show that the preconditions for discrete transitions and the Lie-derivatives for continuous evolution can be viewed as morphisms, and so can be suitably represented by matrices. We reduce the non-trivial invariant generation problem to the computation of the associated eigenspaces or nullspaces by encoding the consecution requirements as specific morphisms represented by such matrices. Our methods are the first to establish very general sufficient conditions that show the existence and allow the computation of invariant ideals. Our approach also embodies a strategy to estimate certain degree bounds, leading to the discovery of rich classes of inductive invariants. By reducing the problem to related linear algebraic manipulations we are able to address various deficiencies of other state-of-the-art invariant generation methods, including the efficient treatment of non-linear hybrid systems. Our approach avoids first-order quantifier eliminations, Grobner basis computations or direct system resolutions, thereby circumventing difficulties met by other recent techniques. (C) 2015 Elsevier B.V. All rights reserved. (AU)

FAPESP's process: 11/08947-1 - Algebraic Formal Methods for Invariant Generation.
Grantee:Rachid Rebiha
Support Opportunities: Scholarships in Brazil - Post-Doctoral
FAPESP's process: 13/04734-9 - Algebraic formal methods for program verification
Grantee:Rachid Rebiha
Support Opportunities: Scholarships abroad - Research Internship - Post-doctor