Dynamical systems model the time evolution of both natural and engineered processes. The automatic analysis of such models relies on different techniques ranging from reachability analysis, model checking, theorem proving, and abstractions. In this context, invariants are subsets of the state space containing all the states reachable from themself. The verification and synthesis of invariants is still a challenging problem over many classes of dynamical systems, since it involves the analysis of an infinite time horizon. In this paper we propose a method for computing invariants through sets of trajectories propagation. The method has been implemented and tested in the tool Sapo which provides reachability methods over discrete time polynomial dynamical systems.
Set-Based Invariants over Polynomial Systems
Alessandro Cimatti;Luca Dorigo;Stefano Tonetta
2023-01-01
Abstract
Dynamical systems model the time evolution of both natural and engineered processes. The automatic analysis of such models relies on different techniques ranging from reachability analysis, model checking, theorem proving, and abstractions. In this context, invariants are subsets of the state space containing all the states reachable from themself. The verification and synthesis of invariants is still a challenging problem over many classes of dynamical systems, since it involves the analysis of an infinite time horizon. In this paper we propose a method for computing invariants through sets of trajectories propagation. The method has been implemented and tested in the tool Sapo which provides reachability methods over discrete time polynomial dynamical systems.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.