The algorithmic analysis of hybrid systems

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

zbMATH Keywords

hybrid systems finite automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items

Differential Game Logic, Diagnosability of delay-deadline failures in fair real time discrete event models, Reachability and optimal control for linear hybrid automata: a quantifier elimination approach, Hybrid diagrams: A deductive-algorithmic approach to hybrid system verification, Efficient scaling-invariant checking of timed bisimulation, Algorithmic analysis of polygonal hybrid systems. I: Reachability, Statistical Model Checking for Networks of Priced Timed Automata, Craig Interpolation in the Presence of Non-linear Constraints, Model measuring for discrete and hybrid systems, Automata-based analysis of stage suspended boom systems, Modeling for Verification, Hybrid Automata as Coalgebras, On the expressiveness and decidability of o-minimal hybrid systems, Task automata: Schedulability, decidability and undecidability, Denotational semantics of hybrid automata, Modeling and analysis using hybrid Petri nets, Switched discrete-time systems with time-varying delays: A generalized \(\mathcal H_2\)-approach, Polynomial interrupt timed automata: verification and expressiveness, Formal controller synthesis from specifications given by discrete-time hybrid automata, Verification and Control of Probabilistic Rectangular Hybrid Automata, Deciding Concurrent Planar Monotonic Linear Hybrid Systems, The refinement calculus of reactive systems, Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems, Formal Modelling, Analysis and Verification of Hybrid Systems, Automated Reasoning for Hybrid Systems — Two Case Studies —, Modularity for timed and hybrid systems, Geometric control of hybrid systems, Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans, Approximating Continuous Systems by Timed Automata, Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space, Unnamed Item, STORMED Hybrid Systems, Reachability of Uncertain Nonlinear Systems Using a Nonlinear Hybridization, Modular Development of Hybrid Systems for Verification in Coq, Fault-tolerant continuous flow systems modelling, Unnamed Item, Compositional Verification for Component-Based Systems and Application, Compositionality issues in discrete, continuous, and hybrid systems, Zeno hybrid systems, Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets, Hybrid systems: Modelling and analysis using emergent dynamics, Taylor approximation for hybrid systems, Rigorous Simulation-Based Analysis of Linear Hybrid Systems, Hybrid Automata in Systems Biology: How Far Can We Go?, 2010 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '10, Hybrid automata with finite bisimulations, Programming with Infinitesimals: A While-Language for Hybrid System Modeling, Model Checking the Quantitative μ-Calculus on Linear Hybrid Systems, Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp>, Abstractions for hybrid systems, A survey of computational complexity results in systems and control, Constructive Collisions, The Unmet Challenge of Timed Systems, On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems, Monotonic hybrid systems, Achilles and the tortoise climbing up the arithmetical hierarchy, Deciding stability and mortality of piecewise affine dynamical systems, The stability of saturated linear dynamical systems is undecidable, Symbolic reachability computation for families of linear vector fields, Hybrid port--Hamiltonian systems: from parameterized incidence matrices to hybrid automata, Optimal persistent disturbance attenuation control for linear hybrid systems, Unnamed Item, Topologies, Continuity and Bisimulations, A first order logic for specification of timed algorithms: Basic properties and a decidable class, A polynomial-time algorithm for checking equivalence under certain semiring congruences motivated by the state-space isomorphism problem for hybrid systems, Modelling of Complex Software Systems: A Reasoned Overview, Computing efficient operation schemes for chemical plants in multi-batch mode, Symbolic verification of hybrid systems: an algebraic approach, The complementarity class of hybrid dynamical systems, Abstract Interpretation of the Physical Inputs of Embedded Programs, Analysis of Linear Hybrid Systems in CLP, Interrupt Timed Automata, Falsification of LTL Safety Properties in Hybrid Systems, Reachability analysis of rational eigenvalue linear systems, A Hybrid Denotational Semantics for Hybrid Systems, The Cayley-Hamilton Theorem for Noncommutative Semirings, A formal framework for Hybrid Event B, Monitoring bounded LTL properties using interval analysis, Applications of MetiTarski in the Verification of Control and Hybrid Systems, Epsilon-Tubes and Generalized Skorokhod Metrics for Hybrid Paths Spaces, Finite Automata as Time-Inv Linear Systems Observability, Reachability and More, Periodically Controlled Hybrid Systems, Supervisory target control for hybrid systems, Wireless ventilation control for large‐scale systems: The mining industrial case, A game approach to the parametric control of real-time systems, Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata, Parking Can Get You There Faster, Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants, A modular formal semantics for Ptolemy, Rigorous implementation of real-time systems – from theory to application, AutomationML as a Shared Model for Offline- and Realtime-Simulation of Production Plants and for Anomaly Detection, Discrete-time control for rectangular hybrid automata, On time optimal control of integrator switched systems with state constraints, Bifurcation in a system of imnteracting fronts, Bounded Model Checking with Parametric Data Structures, Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming, Relating Hybrid Chi to Other Formalisms, Stochastic Concurrent Constraint Programming and Differential Equations, Some decidable results on reachability of solvable systems, 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, Reachability analysis of pushdown automata: Application to model-checking, Stability in measure and asymptotic stability of uncertain nonlinear switched systems with a practical application, Rewriting logic as a semantic framework for concurrency: a progress report, Symbolic analysis of linear hybrid automata -- 25 years later, A Simpler Alternative: Minimizing Transition Systems Modulo Alternating Simulation Equivalence, Verification of machine learning based cyber-physical systems: a comparative study, Time distance-based computation of the \textit{DBM} over-approximation of preemptive real-time systems, State equivalences for rectangular hybrid automata, Hybrid zonotopes: A new set representation for reachability analysis of mixed logical dynamical systems, Switching controller synthesis for delay hybrid systems under perturbations, From post-conditions to post-region invariants

Cites Work