A compositional modelling and analysis framework for stochastic hybrid systems

DOI10.1007/s10703-012-0167-zzbMath1291.68293OpenAlexW2087486424WikidataQ57800949 ScholiaQ57800949MaRDI QIDQ2248073

Arnd Hartmanns, Holger Hermanns, Ernst Moritz Hahn, Joost-Pieter Katoen

Publication date: 30 June 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-012-0167-z

zbMATH Keywords

modellingabstractionprocess calculusstochastic hybrid automata

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (17)

A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces ⋮ Tweaking the odds in probabilistic timed automata ⋮ Optimizing reachability probabilities for a restricted class of stochastic hybrid automata via flowpipe-construction ⋮ Estimating the volume of the solution space of SMT(LIA) constraints by a flat histogram method ⋮ A compositional modelling and verification framework for stochastic hybrid systems ⋮ Compositional abstraction-based synthesis for networks of stochastic switched systems ⋮ A Theory for the Semantics of Stochastic and Non-deterministic Continuous Systems ⋮ Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach ⋮ Revisiting sequential composition in process calculi ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ Multi-cost bounded tradeoff analysis in MDP ⋮ Preface to the special issue on probabilistic model checking ⋮ Adaptive step size numerical integration for stochastic differential equations with discontinuous drift and diffusion ⋮ Identity-Based Cryptosystems and Quadratic Residuosity ⋮ A probabilistic calculus of cyber-physical systems ⋮ Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations ⋮ Compositional construction of control barrier functions for continuous-time stochastic hybrid systems

Uses Software

• PRISM
• MoDeST
• HySAT
• PHAVer
• HyTech
• RSOLVER
• Benchmarks
• Uppaal
• mctau
• HSolver
• SpaceEx

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Approximate model checking of stochastic hybrid systems
• The algorithmic analysis of hybrid systems
• Modular and visual specification of hybrid systems: An introduction to HyCharts
• A theory of timed automata
• Hybrid I/O automata.
• Automatic verification of real-time systems with discrete probability distributions.
• Hybrid process algebra
• HyTech: A model checker for hybrid systems
• Syntax and consistent equation semantics of hybrid Chi
• Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
• Stochastic hybrid systems. Theory and safety critical applications.
• Bisimulation for labelled Markov processes
• Measurability and safety verification for stochastic hybrid systems
• Asymptotic Optimization of a Nonlinear Hybrid System Governed by a Markov Decision Process
• Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs
• Hybrid Systems: Computation and Control
• A Compositional Approach to Performance Modelling
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Formal Methods for the Design of Real-Time Systems
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Process algebra for performance evaluation

This page was built for publication: A compositional modelling and analysis framework for stochastic hybrid systems