HyTech: A model checker for hybrid systems

From MaRDI portal
Publication:1856193


DOI10.1007/s100090050008zbMath1060.68603MaRDI QIDQ1856193

Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi

Publication date: 1997

Published in: International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s100090050008


68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)


Related Items

A Kleene-Schützenberger Theorem for Weighted Timed Automata, HYBRID SYSTEM VERIFICATION IS NOT A SINECURE — THE ELECTRONIC THROTTLE CONTROL CASE STUDY, Efficient Symbolic Representations for Arithmetic Constraints in Verification, HyTech, Some ways to reduce the space dimension in polyhedra computations, Specification and analysis of the AER/NCA active network protocol suite in real-time Maude, Hybridization methods for the analysis of nonlinear systems, Parametric probabilistic transition systems for system design and analysis, Semantics and pragmatics of real-time maude, An algebra of hybrid systems, What's decidable about hybrid automata?, Approximating labelled Markov processes, The power of reachability testing for timed automata, Specification of real-time and hybrid systems in rewriting logic, Process algebra for hybrid systems, Is your model checker on time? On the complexity of model checking for timed modal logics, Positive loop-closed automata: A decidable class of hybrid systems, Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice, Updatable timed automata, Discrete-time control for rectangular hybrid automata, Continuity controlled hybrid automata, CTL* model checking for time Petri nets, Algorithmic analysis of polygonal hybrid systems. I: Reachability, Optimal reachability for multi-priced timed automata, Algorithmic analysis of polygonal hybrid systems. II: Phase portrait and tools, Interval timed coloured Petri net: efficient construction of its state class space preserving linear properties, Hybrid abstractions of affine systems, Bisimulation for labelled Markov processes, Denotational semantics of hybrid automata, Reachability and optimal control for linear hybrid automata: a quantifier elimination approach, Approximating Continuous Systems by Timed Automata, Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space, Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph, Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints