• HyTech

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

  • Referenced in 32 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 10 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 multi-affine vector fields and is expected...
  • HYSDEL

  • Referenced in 35 articles [sw05200]
  • class of hybrid systems described by interconnections of linear dynamic systems, automata, if-then-else...
  • SPeeDI

  • Referenced in 7 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 (two-dimensional) 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...
  • COSMOS

  • Referenced in 5 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...
  • SReach

  • Referenced in 3 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...
  • 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...
  • HARE

  • Referenced in 2 articles [sw10938]
  • Hybrid automata-based 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 semi-complete...
  • HYST

  • Referenced in 4 articles [sw20137]
  • several classes (including affine and nonlinear hybrid automata) to the input formats of several tools...
  • R-Charon

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

  • Referenced in 4 articles [sw13098]
  • generated from bounded model checking of hybrid automata and static analysis of floating-point software...
  • 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...
  • pyHybrid Analysis

  • Referenced in 2 articles [sw10940]
  • Semantics Analysis of Hybrid Systems. Hybrid automata naturally represent systems that exhibit a mixed discrete ... semantics, has been proposed to analyze hybrid automata. This paper presents a Python package, pyHybrid ... semantics framework and allows to analyze hybrid automata...
  • LySHA

  • Referenced in 2 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...
  • HyDI

  • Referenced in 3 articles [sw11912]
  • demands for advanced validation techniques. Hybrid automata are a clean and consolidated formal language ... propose a new language, HYDI, for modeling Hybrid systems with Discrete Interaction. The purpose...