SPeeDI -- a verification tool for polygonal hybrid systems Hybrid systems combining discrete and continuous dynamics arise as mathematical models of various artificial and natural systems, and as an approximation to complex continuous systems. A very important problem in the anajysis of the behavior of hybrid systems is reachability. It is well-known that for most nontrivial subclasses of hybrid systems this and all interesting verification problems are undecidable. Most of the proved decidability results rely on stringent hypothesis that lead to the existence of a finite and computable partition of the state space into classes of states which are equivalent with respect to reachability. This is the case for classes of rectangular automata and hybrid automata with linear vector fields. Most implemented computational procedures resort to (forward or backward) propagation of constraints, typically (unions of convex) polyhedra or ellipsoids. In general, these techniques provide semi-decision procedures, that is, if the given final set of states is reachable, they will terminate, otherwise they may fail to. Maybe the major drawback of set-propagation, reach-set approximation procedures is that they pay little attention to the geometric properties of the specific (class of) systems under analysis. An interesting and still decidable class of hybrid system are the (two-dimensional) polygonal differential inclusions (or SPDI for short).
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Sandler, Andrei; Tveretina, Olga: ParaPlan: a tool for parallel reachability analysis of planar polygonal differential inclusion systems (2017)
- Hansen, Hallstein Asheim; Schneider, Gerardo: GSPeeDI -- a verification tool for generalized polygonal hybrid systems (2009) ioport
- Asarin, Eugene; Pace, Gordon; Schneider, Gerardo; Yovine, Sergio: Algorithmic analysis of polygonal hybrid systems. II: Phase portrait and tools (2008)
- Asarin, Eugene; Schneider, Gerardo; Yovine, Sergio: Algorithmic analysis of polygonal hybrid systems. I: Reachability (2007)
- Pace, Gordon; Schneider, Gerardo: Static analysis for state-space reduction of polygonal hybrid systems (2006)
- Pace, Gordon; Schneider, Gerardo: A compositional algorithm for parallel model checking of polygonal hybrid systems (2006)
- Pace, Gordon J.; Schneider, Gerardo: Model checking polygonal differential inclusions using invariance kernels. (2004)
- Asarin, Eugene; Pace, Gordon; Schneider, Gerardo; Yovine, Sergio: SPeeDI -- a verification tool for polygonal hybrid systems (2002)