The algorithmic analysis of hybrid systems
From MaRDI portal
Publication:673868
DOI10.1016/0304-3975(94)00202-TzbMath0874.68206OpenAlexW2004463571WikidataQ56338518 ScholiaQ56338518MaRDI QIDQ673868
Costas Courcoubetis, Rajeev Alur, Pei-Hsin Ho, Nicolas Halbwachs, Thomas A. Henzinger
Publication date: 28 February 1997
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(94)00202-t
Related Items (only showing first 100 items - show all)
Analysis of faults in cyber-physical systems by finite discrete-time Markov chains ⋮ Numerical bifurcation analysis of the bipedal spring-mass model ⋮ Optimizing reachability probabilities for a restricted class of stochastic hybrid automata via flowpipe-construction ⋮ Verisig 2.0: verification of neural network controllers using Taylor model preconditioning ⋮ Synthesizing invariant barrier certificates via difference-of-convex programming ⋮ \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability ⋮ Continuity controlled hybrid automata ⋮ Compositional modeling and refinement for hierarchical hybrid systems ⋮ Syntax and consistent equation semantics of hybrid Chi ⋮ Counterexample-guided predicate abstraction of hybrid systems ⋮ Schedulability analysis of fixed-priority systems using timed automata ⋮ Bisimulation for Feller-Dynkin processes ⋮ Discrete semantics for hybrid automata. Avoiding misleading assumptions in systems biology ⋮ Formal verification of real-time systems with preemptive scheduling ⋮ On the computational power of dynamical systems and hybrid systems ⋮ Mode discernibility and bounded-error state estimation for nonlinear hybrid systems ⋮ Event-B refinement for continuous behaviours approximation ⋮ On the decidability and complexity of problems for restricted hierarchical hybrid systems ⋮ Recent advances in program verification through computer algebra ⋮ Reachable set estimation and safety verification of nonlinear systems via iterative sums of squares programming ⋮ Hybridization methods for the analysis of nonlinear systems ⋮ Symbolic models for control systems ⋮ Decidable hybrid systems ⋮ An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems ⋮ Sum-of-squares methods for controlled invariant sets with applications to model-predictive control ⋮ A dynamic quantized state system execution framework for hybrid automata ⋮ Observer design for linear hybrid systems with unknown inputs and Petri-net discrete dynamics ⋮ Semantics and pragmatics of real-time maude ⋮ Reachability problems and abstract state spaces for time Petri nets with stopwatches ⋮ Observer synthesis for linear hybrid systems with constrained discrete dynamics ⋮ Safety verification for probabilistic hybrid systems ⋮ A game-theoretic approach to fault diagnosis and identification of hybrid systems ⋮ Hybrid automata-based CEGAR for rectangular hybrid systems ⋮ Reliable social sensing with physical constraints: analytic bounds and performance evaluation ⋮ Exact safety verification of hybrid systems using sums-of-squares representation ⋮ Low dimensional hybrid systems -- decidable, undecidable, don't know ⋮ A Kleene-Schützenberger theorem for weighted timed automata ⋮ Implementing biological hybrid systems: allowing composition and avoiding stiffness ⋮ Weighted o-minimal hybrid systems ⋮ Automata and logics over finitely varying functions ⋮ Applying abstract acceleration to (co-)reachability analysis of reactive programs ⋮ Non-standard semantics of hybrid systems modelers ⋮ Modeling of complex systems. II: A minimalist and unified semantics for heterogeneous integrated systems ⋮ Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets ⋮ Computing branching distances with quantitative games ⋮ Interrupt timed automata: verification and expressiveness ⋮ Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations ⋮ Discrete-time control for rectangular hybrid automata ⋮ Computational challenges in systems biology ⋮ Control: a perspective ⋮ Hybrid I/O automata. ⋮ Verification of duration systems using an approximation approach ⋮ A CSP versus a zonotope-based method for solving guard set intersection in nonlinear hybrid reachability ⋮ SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata ⋮ Verification and control for probabilistic hybrid automata with finite bisimulations ⋮ Timed discrete event control of parallel production lines with continuous outputs ⋮ Approximate simulation relations for hybrid systems ⋮ Barrier certificates revisited ⋮ On the distinguishability and observer design for single-input single-output continuous-time switched affine systems under bounded disturbances with application to chaos-based modulation ⋮ An approximation algorithm for box abstraction of transition systems on real state spaces ⋮ A compositional modelling and analysis framework for stochastic hybrid systems ⋮ Computing reachable states for nonlinear biological models ⋮ Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement ⋮ A decidable class of planar linear hybrid systems ⋮ Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques ⋮ A brief history of process algebra ⋮ Process algebra for hybrid systems ⋮ Computing reachable sets for uncertain nonlinear monotone systems ⋮ Languages and models for hybrid automata: a coalgebraic perspective ⋮ Safe \& robust reachability analysis of hybrid systems ⋮ Limit cycle analysis in a class of hybrid systems ⋮ Inclusion dynamics hybrid automata ⋮ Robustness of temporal logic specifications for continuous-time signals ⋮ An algebra of hybrid systems ⋮ First-order hybrid Petri nets. An application to distributed manufacturing systems ⋮ Approximate equivalence and synchronization of metric transition systems ⋮ A receding horizon event-driven control strategy for intelligent traffic management ⋮ Falsification of hybrid systems with symbolic reachability analysis and trajectory splicing ⋮ What's decidable about hybrid automata? ⋮ Achilles and the tortoise climbing up the hyper-arithmetical hierarchy ⋮ Post and pre-initialized stopwatch Petri nets: formal semantics and state space computation ⋮ On fluidization of discrete event models: Observation and control of continuous Petri nets ⋮ 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 ⋮ Coverage-guided test generation for continuous and hybrid systems ⋮ Object-oriented hybrid systems of coalgebras plus monoid actions ⋮ Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers ⋮ Approximate equivalence of the hybrid automata with Taylor theory ⋮ Refinement of time ⋮ Hybrid diagrams ⋮ Decidable integration graphs. ⋮ An algebraic framework for urgency ⋮ Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques ⋮ Positive loop-closed automata: A decidable class of hybrid systems ⋮ Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro} ⋮ Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming ⋮ Decisiveness of stochastic systems and its application to hybrid models ⋮ Timed network games ⋮ Specification of real-time and hybrid systems in rewriting logic ⋮ Generating invariants for non-linear hybrid systems
Cites Work
- Unnamed Item
- Model-checking in dense real-time
- ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
- A calculus of durations
- A theory of timed automata
- From ATP to timed graphs and hybrid systems
- Symbolic model checking for real-time systems
- Real-time system = discrete system + clock variables
This page was built for publication: The algorithmic analysis of hybrid systems