A compositional modelling and verification framework for stochastic hybrid systems

DOI10.1007/s00165-017-0421-7zbMath1370.68220OpenAlexW2590905045MaRDI QIDQ2403530

Naijun Zhan, Li-jun Zhang, Shu-Ling Wang

Publication date: 8 September 2017

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-017-0421-7

zbMATH Keywords

invariantsstochastic hybrid systemsdeductive verificationstochastic hybrid CSP

Mathematics Subject Classification ID

Control/observation systems involving computers (process control, etc.) (93C83) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces ⋮ A probabilistic calculus of cyber-physical systems

Uses Software

• PASS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Safety verification for probabilistic hybrid systems
• Stochastic differential equations. An introduction with applications
• Automatic verification of stability and safety for delay differential equations
• A compositional modelling and analysis framework for stochastic hybrid systems
• Bayesian statistical model checking with application to Stateflow/Simulink verification
• Validated simulation-based verification of delayed differential dynamics
• Refinement-oriented probability for CSP
• Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
• An Assume/Guarantee Based Compositional Calculus for Hybrid CSP
• Formal Modelling, Analysis and Verification of Hybrid Systems
• Automatic invariant generation for hybrid systems using ideal fixed points
• Measurability and safety verification for stochastic hybrid systems
• Transcendental inductive invariants generation for non-linear differential and hybrid systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• Computing Differential Invariants of Hybrid Systems as Fixedpoints
• Constraint-Based Approach for Analysis of Hybrid Systems
• GLOBAL ATTRACTIVITY IN A PREDATOR–PREY SYSTEM WITH PURE DELAYS
• Assume-Guarantee Verification for Probabilistic Systems
• On invariant polyhedra of continuous-time linear systems
• Asymptotic Optimization of a Nonlinear Hybrid System Governed by a Markov Decision Process
• Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs
• A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Extending Hybrid CSP with Probability and Stochasticity
• An axiomatic basis for computer programming
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control