Reachability in parametric interval Markov chains using constraints

DOI10.1016/j.tcs.2018.06.016zbMath1400.68118arXiv1706.00270OpenAlexW2809485720WikidataQ129624531 ScholiaQ129624531MaRDI QIDQ1786613

Didier Lime, Anicet Bart, Benoît Delahaye, Paulin Fournier, Charlotte Truchet, Eric Monfroy

Publication date: 24 September 2018

Published in: Theoretical Computer Science, Quantitative Evaluation of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1706.00270

zbMATH Keywords

Markov chainsreachabilityconstraint programmingparameter synthesisabstract models

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) 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 (4)

Parameter Synthesis Algorithms for Parametric Interval Markov Chains ⋮ Quantitative analysis of interval Markov chains ⋮ Parameter synthesis in Markov models: a gentle survey ⋮ Reachability in parametric interval Markov chains using constraints

Uses Software

• PRISM
• CPLEX
• z3
• PARAM
• TuLiP
• PROPhESY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model checking of open interval Markov chains
• Reachability in parametric interval Markov chains using constraints
• Probabilistic verification of Herman's self-stabilisation algorithm
• Parameter Synthesis for Parametric Interval Markov Chains
• Mixed Integer Linear Programming Formulation Techniques
• Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
• Parametric real-time reasoning
• LTL Model Checking of Interval Markov Chains
• Model-Checking ω-Regular Properties of Interval Markov Chains
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Reachability in parametric interval Markov chains using constraints