Statistical Model Checking for Stochastic Hybrid Systems

Abstract

This paper presents novel extensions and applications of the UPPAAL-SMC model checker. The extensions allow for statistical model checking of stochastic hybrid systems. We show how our race-based stochastic semantics extends to networks of hybrid systems, and indicate the integration technique applied for implementing this semantics in the UPPAAL-SMC simulation engine. We report on two applications of the resulting tool-set coming from systems biology and energy aware buildings.

In Proceedings HSB 2012, arXiv:1208.3151

References in corpus (3)

• Mechanisms of noise-resistance in genetic oscillators
• Statistical Model Checking : An Overview
• Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach

Cited by in corpus (12)

• PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
• Shielded Reinforcement Learning for Hybrid Systems
• Monitoring Temporal Properties using Interval Analysis
• SReach: A Bounded Model Checker for Stochastic Hybrid Systems
• HySIA: Tool for Simulating and Monitoring Hybrid Automata Based on Interval Analysis
• Stochastic HYPE: Flow-based modelling of stochastic hybrid systems
• Probabilistic Analysis of Weakly-Hard Real-Time Systems
• Decisiveness of Stochastic Systems and its Application to Hybrid Models
• Approximate probabilistic verification of hybrid systems
• Formal Verification of Dynamic and Stochastic Behaviors for Automotive Systems
• Decisiveness of Stochastic Systems and its Application to Hybrid Models (Full Version)
• Monitoring Bounded LTL Properties Using Interval Analysis