Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems

DOI10.1145/2461328.2461372zbMath1362.68187OpenAlexW1975255760MaRDI QIDQ2986933

Alessandro Abate, Ilya Tkachev

Publication date: 16 May 2017

Published in: Proceedings of the 16th international conference on Hybrid systems: computation and control (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2461328.2461372

zbMATH Keywords

Markov processesformal verificationprobabilistic model-checkingstochastic hybrid systemsfinite abstractionsapproximate bisimulationslinear temporal specifications

Mathematics Subject Classification ID

Discrete-time Markov processes on general state spaces (60J05) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (8)

Time window temporal logic ⋮ Mixed Integer Linear Programming Approach for Control Synthesis with Weighted Signal Temporal Logic ⋮ On the Relationship Between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context ⋮ On the effect of perturbation of conditional probabilities in total variation ⋮ Quantitative model-checking of controlled discrete-time Markov processes ⋮ Dynamic Bayesian networks for formal verification of structured stochastic processes ⋮ Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations ⋮ Robustly complete finite-state abstractions for verification of stochastic systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A note on two problems in connexion with graphs
• Enhancing model checking in verification by AI techniques
• Receding horizon control for temporal logic specifications
• Model Repair for Probabilistic Systems
• Markov decision processes and regular events
• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• Controlling a Class of Nonlinear Systems on Rectangles
• Diagnostic Information for Realizability

This page was built for publication: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems