
HyTech
 Referenced in 333 articles
[sw04125]
 temporal requirement. Hybrid systems are specified as collections of automata with discrete and continuous components...

KeYmaera
 Referenced in 48 articles
[sw03709]
 hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements ... automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity...

Ariadne
 Referenced in 14 articles
[sw06670]
 library for computation with hybrid automata under development by a joint team including University ... synthesis of systems described with hybrid automata. The ARIADNE computational kernel is written using generic...

RAMAS
 Referenced in 12 articles
[sw10958]
 easily extendable to rectangular hybrid automata with multiaffine vector fields and is expected...

HYSDEL
 Referenced in 39 articles
[sw05200]
 class of hybrid systems described by interconnections of linear dynamic systems, automata, ifthenelse...

COSMOS
 Referenced in 6 articles
[sw13329]
 statistical model checker for the hybrid automata stochastic logic. This tool paper introduces Cosmos ... statistical model checker for the Hybrid Automata Stochastic Logic (HASL). HASL employs Linear Hybrid Automata...

SPeeDI
 Referenced in 8 articles
[sw00896]
 known that for most nontrivial subclasses of hybrid systems this and all interesting verification problems ... classes of rectangular automata and hybrid automata with linear vector fields. Most implemented computational procedures ... interesting and still decidable class of hybrid system are the (twodimensional) polygonal differential inclusions...

LinAIG
 Referenced in 6 articles
[sw10316]
 fully symbolic verification of linear hybrid automata with large discrete state spaces. We propose ... algorithm for the verification of linear hybrid automata with large discrete state spaces (where ... part and the continuous part of the hybrid state space are represented by one symbolic...

BACH
 Referenced in 4 articles
[sw11906]
 BACH: bounded reachability checker for linear hybrid automata. Hybrid automata are well studied formal models ... state changes. However, the analysis of hybrid automata is quite difficult. Even for the simple ... class of linear hybrid automata, the reachability problem is undecidable. In the author’s previous ... work, for linear hybrid automata we proposed a linear programming based approach to check...

HASL
 Referenced in 6 articles
[sw13330]
 stochastic models. We introduce the Hybrid Automata Stochastic Logic (HASL), a new temporal logic formalism ... stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) as machineries to select prefixes...

HYST
 Referenced in 8 articles
[sw20137]
 several classes (including affine and nonlinear hybrid automata) to the input formats of several tools...

CalCS
 Referenced in 8 articles
[sw13098]
 generated from bounded model checking of hybrid automata and static analysis of floatingpoint software...

HARE
 Referenced in 4 articles
[sw10938]
 Hybrid automatabased CEGAR for rectangular hybrid systems. In this paper we present a framework ... CEGAR) for systems modelled as rectangular hybrid automata. The main difference, between our approach ... previous proposals for CEGAR for hybrid automata, is that we consider the abstractions ... hybrid automata as well. We show that the CEGAR scheme is semicomplete...

SReach
 Referenced in 5 articles
[sw20158]
 systems. The first one is (nonlinear) hybrid automata with parametric uncertainty. The second ... probabilistic hybrid automata with additional randomness for both transition probabilities and variable resets. Standard approaches ... reachability problems for linear hybrid systems require numerical solutions for large optimization problems, and become...

LySHA
 Referenced in 4 articles
[sw20150]
 algorithm for verifying inevitability of Linear Hybrid Automata (LHA). The algorithm combines (a) Lyapunov function ... loops of the hybrid automaton. The algorithm is complete for automata that are symmetric with ... integrated with a Simulink/Stateflow frontend for modeling hybrid systems. The experimental results demonstrate the effectiveness ... methodology in verifying inevitability of hybrid automata with up to five continuous dimensions and forty...

Pyhybridanalysis
 Referenced in 3 articles
[sw14549]
 package to both represent and analyze hybrid automata. It exploit the semantics framework developed ... reduce the reachability problem over hybrid automata to the satiability problem of a formula...

HyLAA
 Referenced in 4 articles
[sw20821]
 tool for simulationequivalent reachability for hybrid automata with affine dynamics. HyLAA’s analysis ... unsafe state if and only if the hybrid automaton simulation engine could produce such...

RCharon
 Referenced in 4 articles
[sw19756]
 Charon is the first formal, hybrid automata based modeling language which also addresses dynamic reconfiguration...

HyComp
 Referenced in 4 articles
[sw20163]
 HyComp takes as input networks of hybrid automata specified using the HyDI symbolic language. HyComp...

HyCreate
 Referenced in 2 articles
[sw20138]
 Tool for Overapproximating Reachability of Hybrid Automata. HyCreate is a software tool for defining hybrid ... automata and computing overapproximations of reachable sets for systems with nonlinear, nondeterministic dynamics with ... user of HyCreate specifies a hybrid automata through the interface, using the standard hybrid automaton...