What's decidable about hybrid automata?
From MaRDI portal
Publication:1273866
DOI10.1006/jcss.1998.1581zbMath0920.68091OpenAlexW2085838366MaRDI QIDQ1273866
Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, Pravin P. Varaiya
Publication date: 6 January 1999
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://hdl.handle.net/1813/7198
Related Items (only showing first 100 items - show all)
Multi-agent Safety Verification Using Symmetry Transformations ⋮ Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities ⋮ Unnamed Item ⋮ Bounded Verification of Reachability of Probabilistic Hybrid Systems ⋮ Symbolic analysis of linear hybrid automata -- 25 years later ⋮ Simulation relations and applications in formal methods ⋮ Multi-Requirement Testing Using Focused Falsification ⋮ Linear Time Monitoring for One Variable TPTL ⋮ Mortality and Edge-to-Edge Reachability are Decidable on Surfaces ⋮ Parametric updates in parametric timed automata ⋮ Stability analysis of planar probabilistic piecewise constant derivative systems ⋮ Unnamed Item ⋮ Optimal mixed discrete-continuous planning for linear hybrid systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Symbolic models for nonlinear control systems affected by disturbances ⋮ Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp> ⋮ A survey of computational complexity results in systems and control ⋮ Boundedness of the Domain of Definition is Undecidable for Polynomial ODEs ⋮ A menagerie of timed automata ⋮ Unnamed Item ⋮ The stability of saturated linear dynamical systems is undecidable ⋮ Formal language properties of hybrid systems with strong resets ⋮ Topologies, Continuity and Bisimulations ⋮ Unnamed Item ⋮ What’s Decidable About Parametric Timed Automata? ⋮ Language-Based Abstraction Refinement for Hybrid System Verification ⋮ Property Driven Three-Valued Model Checking on Hybrid Automata ⋮ Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata ⋮ Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction* ⋮ A Survey on Analog Models of Computation ⋮ Timed recursive state machines: expressiveness and complexity ⋮ Reachability analysis of linear systems with stepwise constant inputs ⋮ Spotlight abstraction in model checking real-time task schedulability ⋮ Optimizing reachability probabilities for a restricted class of stochastic hybrid automata via flowpipe-construction ⋮ On The Complexity of Bounded Time Reachability for Piecewise Affine Systems ⋮ Deadness and how to disprove liveness in hybrid dynamical systems ⋮ Finite abstraction of mixed monotone systems with discrete and continuous inputs ⋮ Automata-based analysis of stage suspended boom systems ⋮ Model Checking Real-Time Systems ⋮ Verification of Hybrid Systems ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ On the complexity of bounded time and precision reachability for piecewise affine systems ⋮ Event-B refinement for continuous behaviours approximation ⋮ On the expressiveness and decidability of o-minimal hybrid systems ⋮ Symbolic models for time-varying time-delay systems via alternating approximate bisimulation ⋮ Task automata: Schedulability, decidability and undecidability ⋮ Computation with perturbed dynamical systems ⋮ Hybridization methods for the analysis of nonlinear systems ⋮ Symbolic models for control systems ⋮ Polynomial interrupt timed automata: verification and expressiveness ⋮ A dynamic quantized state system execution framework for hybrid automata ⋮ Semantics and pragmatics of real-time maude ⋮ Monitoring of dynamic processes by rectangular hybrid automata ⋮ Verification and Control of Probabilistic Rectangular Hybrid Automata ⋮ Nested Timed Automata with Frozen Clocks ⋮ Safety verification for probabilistic hybrid systems ⋮ Automatic synthesis of switching controllers for linear hybrid systems: safety control ⋮ On the greatest solutions to weakly linear systems of fuzzy relation inequalities and equations ⋮ A study on shuffle, stopwatches and independently evolving clocks ⋮ Approximating Continuous Systems by Timed Automata ⋮ Modular discrete time approximations of distributed hybrid automata ⋮ Bisimulations for fuzzy automata ⋮ Nondeterministic automata: equivalence, bisimulations, and uniform relations ⋮ PTIME parametric verification of safety properties for reasonable linear hybrid automata ⋮ Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets ⋮ Unnamed Item ⋮ Symbolic checking of fuzzy CTL on fuzzy program graph ⋮ Interrupt timed automata: verification and expressiveness ⋮ Succinct discrete time approximations of distributed hybrid automata ⋮ Accurate hybridization of nonlinear systems ⋮ Compositional analysis for linear control systems ⋮ On integration of event-based estimation and robust MPC in a feedback loop ⋮ From synchronous programs to symbolic representations of hybrid systems ⋮ A descent algorithm for the optimal control of constrained nonlinear switched dynamical systems ⋮ Timed automata with observers under energy constraints ⋮ Real-time scheduling of mixture-of-experts systems with limited resources ⋮ On a control algorithm for time-varying processor availability ⋮ Timed I/O automata ⋮ Receding horizon control for temporal logic specifications ⋮ Synthesis using approximately bisimilar abstractions ⋮ Oscillation analysis of linearly coupled piecewise affine systems ⋮ On infinity norms as Lyapunov functions for piecewise affine systems ⋮ Identifiability of discrete-time linear switched systems ⋮ Rank properties of poincare maps for hybrid systems with applications to bipedal walking ⋮ Stealthy deception attacks on water SCADA systems ⋮ Comparison of overapproximation methods for stability analysis of networked control systems ⋮ Distributed Kalman Filter algorithms for self-localization of mobile devices ⋮ Convergence results for ant routing algorithms viastochastic approximation ⋮ Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems ⋮ Automatic invariant generation for hybrid systems using ideal fixed points ⋮ Safe compositional network sketches ⋮ Bayesian statistical model checking with application to Simulink/Stateflow verification ⋮ On the connections between PCTL and dynamic programming ⋮ Modeling and verification of stochastic hybrid systems using HIOA ⋮ A generating function approach to the stability of discrete-time switched linear systems ⋮ Stabilization of planar switched linear systems using polar coordinates ⋮ Amir Pnueli and the dawn of hybrid systems ⋮ Finite-state automata in information technologies ⋮ Verification of duration systems using an approximation approach
Uses Software
Cites Work
- The algorithmic analysis of hybrid systems
- Formal methods for industrial applications. Specification and programming the Steam Boiler Control
- A theory of timed automata
- Symbolic model checking for real-time systems
- HyTech: A model checker for hybrid systems
- Forward and backward simulations. II: Timing-based systems
- Algorithmic analysis of nonlinear hybrid systems
- What good are digital clocks?
- Parametric real-time reasoning
This page was built for publication: What's decidable about hybrid automata?
