Semi-algebraic abstraction is an approach to the safety verification problem for polynomial dynamical systems where the state space is partitioned according to the sign of a set of polynomials. Similarly to predicate abstraction for discrete systems, the number of abstract states is exponential in the number of polynomials. Hence, semi-algebraic abstraction is expensive to explicitly compute and then analyze (e.g., to prove a safety property or extract invariants). In this paper, we propose an implicit encoding of the semi-algebraic abstraction, which avoids the explicit enumeration of the abstract states: the safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, allowing us to reuse existing model-checking tools based on Satisfiability Modulo Theory (SMT). The main challenge we solve is to express the semi-algebraic abstraction as a first-order logic formula that is linear in the number of predicates, instead of exponential, thus letting the model checker lazily explore the exponential number of abstract states with symbolic techniques. We implemented the approach and validated experimentally its potential to prove safety for polynomial dynamical systems.

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems / Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano. - 12759:(2021), pp. 529-551. (Intervento presentato al convegno International Conference on Computer Aided Verification, CAV 2021 tenutosi a Virtual nel July 20-23, 2021) [10.1007/978-3-030-81685-8_25].

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems

Alessandro Cimatti;Alberto Griggio;Stefano Tonetta
2021-01-01

Abstract

Semi-algebraic abstraction is an approach to the safety verification problem for polynomial dynamical systems where the state space is partitioned according to the sign of a set of polynomials. Similarly to predicate abstraction for discrete systems, the number of abstract states is exponential in the number of polynomials. Hence, semi-algebraic abstraction is expensive to explicitly compute and then analyze (e.g., to prove a safety property or extract invariants). In this paper, we propose an implicit encoding of the semi-algebraic abstraction, which avoids the explicit enumeration of the abstract states: the safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, allowing us to reuse existing model-checking tools based on Satisfiability Modulo Theory (SMT). The main challenge we solve is to express the semi-algebraic abstraction as a first-order logic formula that is linear in the number of predicates, instead of exponential, thus letting the model checker lazily explore the exponential number of abstract states with symbolic techniques. We implemented the approach and validated experimentally its potential to prove safety for polynomial dynamical systems.
2021
Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, Proceedings, Part I
Cham, Switzerland
Springer
Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems / Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano. - 12759:(2021), pp. 529-551. (Intervento presentato al convegno International Conference on Computer Aided Verification, CAV 2021 tenutosi a Virtual nel July 20-23, 2021) [10.1007/978-3-030-81685-8_25].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/342959
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact