On-the-fly verification and optimization of DTA-properties for large Markov chains

DOI10.1007/s10703-012-0165-1zbMath1291.68295OpenAlexW2075743205MaRDI QIDQ2248080

David Spieler, Martin R. Neuhäußer, Verena Wolf, Linar Mikeev

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-0165-1

zbMATH Keywords

parameter estimationmodel checkingcontinuous-time Markov chainsdeterministic timed automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Continuous-time Markov processes on discrete state spaces (60J27) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items

Abstraction-guided truncations for stationary distributions of Markov population models ⋮ Modeling and analysis of the obstacle-avoidance strategies for a mobile robot in a dynamic environment ⋮ Analyzing Oscillatory Behavior with Formal Methods ⋮ Preface to the special issue on probabilistic model checking ⋮ Analysis of Markov jump processes under terminal constraints

Uses Software

• PRISM

Cites Work

• Unnamed Item
• Unnamed Item
• Continuous-time Markov chains. An applications-oriented approach
• A theory of timed automata
• Efficient CTMC Model Checking of Linear Real-Time Objectives
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Bounding the equilibrium distribution of Markov population models
• Analysing Biochemical Oscillation through Probabilistic Model Checking

This page was built for publication: On-the-fly verification and optimization of DTA-properties for large Markov chains