HyTech: A model checker for hybrid systems
From MaRDI portal
Publication:1856193
DOI10.1007/s100090050008zbMath1060.68603OpenAlexW2060095702MaRDI QIDQ1856193
Howard Wong-Toi, Thomas A. Henzinger, Pei-Hsin Ho
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
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Approximate optimal hybrid control synthesis by classification-based derivative-free optimization, Modelling and analysing neural networks using a hybrid process algebra, Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey, Hybrid automata as a modelling approach in the behavioural sciences, \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability, Continuity controlled hybrid automata, CTL* model checking for time Petri nets, Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice, Reachability and optimal control for linear hybrid automata: a quantifier elimination approach, Updatable timed automata, Algorithmic analysis of polygonal hybrid systems. I: Reachability, Rigorous Discretization of Hybrid Systems Using Process Calculi, Verification of Hybrid Systems, Formal verification of real-time systems with preemptive scheduling, Action language verifier: An infinite-state model checker for reactive software specifications, Generalization strategies for the verification of infinite state systems, HYPE: A Process Algebra for Compositional Flows and Emergent Behaviour, Some ways to reduce the space dimension in polyhedra computations, Denotational semantics of hybrid automata, 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, Automatic synthesis of switching controllers for linear hybrid systems: safety control, A survey of timed automata for the development of real-time systems, Hybrid automata-based CEGAR for rectangular hybrid systems, Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration, Approximating labelled Markov processes, The power of reachability testing for timed automata, Symbolic analysis of linear hybrid automata -- 25 years later, Approximating Continuous Systems by Timed Automata, Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space, A Kleene-Schützenberger theorem for weighted timed automata, Bisimulation conversion and verification procedure for goal-based control systems, Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces, Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets, Computing branching distances with quantitative games, Discrete-time control for rectangular hybrid automata, Linear temporal logic symbolic model checking, Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph, Efficient Symbolic Representations for Arithmetic Constraints in Verification, Parameter synthesis for hierarchical concurrent real-time systems, Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation, Rigorous Simulation-Based Analysis of Linear Hybrid Systems, Hybrid Automata in Systems Biology: How Far Can We Go?, On Reachability for Hybrid Automata over Bounded Time, Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp>, Optimal reachability for multi-priced timed automata, Algorithmic analysis of polygonal hybrid systems. II: Phase portrait and tools, A compositional modelling and analysis framework for stochastic hybrid systems, Unnamed Item, Reachability computation for polynomial dynamical systems, Interval timed coloured Petri net: efficient construction of its state class space preserving linear properties, Sampling-based Algorithm for Testing and Validating Robot Controllers, Hybrid automata, reachability, and systems biology, Hybrid dynamics of stochastic programs, Modeling and simulation of cardiac tissue using hybrid I/O automata, Hybrid abstractions of affine systems, Smaller Abstractions for ∀CTL* without Next, Process algebra for hybrid systems, A hybrid automata model of social networking addiction, Bisimulation for labelled Markov processes, Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration, On checking equivalence of simulation scripts, Discrete-time hybrid modeling and verification of the batch evaporator process benchmark, An algebra of hybrid systems, Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints, A Kleene-Schützenberger Theorem for Weighted Timed Automata, Applications of MetiTarski in the Verification of Control and Hybrid Systems, Parameter Synthesis for Hybrid Systems with an Application to Simulink Models, HyTech, A receding horizon event-driven control strategy for intelligent traffic management, Event-driven optimization-based control of hybrid systems with integral continuous-time dynamics, What's decidable about hybrid automata?, Bio-PEPA with Events, Model-checking Timed Temporal Logics, Formalized Timed Automata, Don't care words with an application to the automata-based approach for real addition, A game approach to the parametric control of real-time systems, HYBRID SYSTEM VERIFICATION IS NOT A SINECURE — THE ELECTRONIC THROTTLE CONTROL CASE STUDY, Logahedra: A New Weakly Relational Domain, Applications of polyhedral computations to the analysis and verification of hardware and software systems, Hybrid systems: From verification to falsification by combining motion planning and discrete search, Computing differential invariants of hybrid systems as fixed points, PARAMETRIC VERIFICATION AND TEST COVERAGE FOR HYBRID AUTOMATA USING THE INVERSE METHOD, Contraction of the ITCPN state space, On Improving Backwards Verification of Timed Automata (Extended Abstract), Parking Can Get You There Faster, Modeling, analyzing and controlling hybrid systems by guarded flexible nets, Hierarchical hybrid modelling and control of an unmanned helicopter, Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques, Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming, Recent Advances in Real-Time Maude, 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, Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems, Spatial Networks of Hybrid I/O Automata for Modeling Excitable Tissue, Abstraction and Completeness for Real-Time Maude, Specification of real-time and hybrid systems in rewriting logic
