
HyTech
 Referenced in 321 articles
[sw04125]
 linear hybrid system satisfies a temporal requirement. Hybrid systems are specified as collections of automata...

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

LinAIG
 Referenced in 6 articles
[sw10316]
 Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces ... symbolic 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 ... minimization: redundancy elimination eliminates socalled redundant linear constraints from LinAIG representations by a suitable...

BACH
 Referenced in 4 articles
[sw11906]
 BACH: bounded reachability checker for linear hybrid automata. Hybrid automata are well studied formal models ... Even for the simple class of linear hybrid automata, the reachability problem is undecidable ... author’s previous work, for linear hybrid automata we proposed a linear programming based approach ... perform bounded reachability checking of linear hybrid automata. The experiment data shows that BACH...

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

COSMOS
 Referenced in 5 articles
[sw13329]
 Automata Stochastic Logic (HASL). HASL employs Linear Hybrid Automata (LHA), a gen eralization of Deterministic...

SPeeDI
 Referenced in 7 articles
[sw00896]
 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...

LySHA
 Referenced in 3 articles
[sw20150]
 algorithm for verifying inevitability of Linear Hybrid Automata (LHA). The algorithm combines (a) Lyapunov function...

FORTS
 Referenced in 1 article
[sw15029]
 FORTS is a model checker on Linear Hybrid Automata (LHA) that I write...

SReach
 Referenced in 4 articles
[sw20158]
 uncertainty. The second one is probabilistic hybrid automata with additional randomness for both transition probabilities ... Standard approaches to reachability problems for linear hybrid systems require numerical solutions for large optimization...

CAR30
 Referenced in 3 articles
[sw08370]
 Cellular Automata (CA) along with a Maximum Length Linear Hybrid CA. This design...

CalCS
 Referenced in 6 articles
[sw13098]
 satisfiability solving of Boolean combinations of nonlinear constraints that are convex. Our approach applies ... generated from bounded model checking of hybrid automata and static analysis of floatingpoint software...

REDLIB
 Referenced in 5 articles
[sw21175]
 full TCTL modelchecking of densetime automata with multiple fairness assumptions. REDLIB uses ... fixpoint calculation, parametric safety analysis of linear hybrid systems, speedup techniques for greatest fixpoint...

HyLAA
 Referenced in 2 articles
[sw20821]
 tool for computing simulationequivalent reachability for linear systems. Simulations are a practical method ... that can be reached using a particular hybrid automaton simulation algorithm, a property we call ... 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...

ATLAS
 Referenced in 195 articles
[sw00056]
 This paper describes the Automatically Tuned Linear Algebra...

CGAL
 Referenced in 344 articles
[sw00118]
 The goal of the CGAL Open Source Project...

Coq
 Referenced in 1758 articles
[sw00161]
 Coq is a formal proof management system. It...

GAP
 Referenced in 2735 articles
[sw00320]
 GAP is a system for computational discrete algebra...

gmp
 Referenced in 260 articles
[sw00363]
 GMP is a free library for arbitrary precision...

Isabelle
 Referenced in 601 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...