Generating invariants for non-linear hybrid systems

Autor(es)

Rebiha, Rachid ^[1] ; Moura, Arnaldo V. ^[1] ; Matringe, Nadir ^[2]

Afiliação do(s) autor(es)

^[1] Univ Estadual Campinas, Inst Comp, Sao Paulo - Brazil

^[2] Univ Poitiers, Lab Math & Applicat, Poitiers - France

• Tipo de documento: Artigo Científico
• Fonte: THEORETICAL COMPUTER SCIENCE; v. 594, p. 180-200, AUG 23 2015.
• Citações Web of Science: 3

Resumo

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)

• Processo FAPESP: 11/08947-1 - Métodos Formais Algébricos para Gerção de Invariantes.
• Beneficiário: Rachid Rebiha
• Modalidade de apoio: Bolsas no Brasil - Pós-Doutorado
• Processo FAPESP: 13/04734-9 - Métodos formais algébricos para verificação de programas
• Beneficiário: Rachid Rebiha
• Modalidade de apoio: Bolsas no Exterior - Estágio de Pesquisa - Pós-Doutorado