Verification and control for probabilistic hybrid automata with finite bisimulations
type: Item
instance of: scholarly article
title: Verification and control for probabilistic hybrid automata with finite bisimulations
zbMATH Open document ID: 1417.68105
author: Jeremy Sproston
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2019-03-27T00:00:00Z
full work available at URL: http://hdl.handle.net/2318/1681478
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 7043263
zbMATH Keywords: hybrid automata
zbMATH Keywords: probabilistic model checking
zbMATH Keywords: probabilistic games
describes a project that uses: PRISM
MaRDI profile type: Publication
OpenAlex ID: W2900091779
cites work: The algorithmic analysis of hybrid systems
cites work: Discrete-time control for rectangular hybrid automata
cites work: Q4270068
cites work: Q4953390
cites work: Q2766628
cites work: Hybrid Systems: Computation and Control
cites work: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
cites work: Measurability and safety verification for stochastic hybrid systems
cites work: Safety verification for probabilistic hybrid systems
cites work: Formal Verification and Synthesis for Discrete-Time Stochastic Systems
cites work: On Optimal Control of Stochastic Linear Hybrid Systems
cites work: Q4315289
cites work: Automatic verification of real-time systems with discrete probability distributions.
cites work: Bisimulation through probabilistic testing
cites work: Q4847023
cites work: STORMED Hybrid Systems
cites work: What's decidable about hybrid automata?
cites work: Algorithmic analysis of nonlinear hybrid systems
cites work: Formal Modeling and Analysis of Timed Systems
cites work: State explosion in almost-sure probabilistic reachability
cites work: Performance analysis of probabilistic timed automata using digital clocks
cites work: Expected reachability-time games
cites work: Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
cites work: A survey of stochastic \(\omega \)-regular games
cites work: Q5322945
cites work: Automata, Languages and Programming
cites work: On Probabilistic Alternating Simulations
cites work: Model Checking Linear-Time Properties of Probabilistic Systems
cites work: Model checking of probabilistic and nondeterministic systems
cites work: O-Minimal Hybrid Reachability Games
Wikidata QID: Q128966315
DOI: 10.1016/J.JLAMP.2018.11.001
description: scientific article; zbMATH DE number 7043263