LTL Model Checking of Interval Markov Chains
From MaRDI portal
Publication:5326312
DOI10.1007/978-3-642-36742-7_3zbMath1381.68147OpenAlexW125973810MaRDI QIDQ5326312
Michael Benedikt, Rastislav Lenhardt, James Worrell
Publication date: 5 August 2013
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-36742-7_3
Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items
Incorporating monitors in reactive synthesis without paying the price ⋮ From LTL to unambiguous Büchi automata via disambiguation of alternating automata ⋮ Safraless LTL synthesis considering maximal realizability ⋮ Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems ⋮ Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination ⋮ Quantitative analysis of interval Markov chains ⋮ Markov chains and unambiguous automata ⋮ Unnamed Item ⋮ Opacity for linear constraint Markov chains ⋮ Approximate Verification of the Symbolic Dynamics of Markov Chains ⋮ On the metric-based approximate minimization of Markov chains ⋮ Reachability in parametric interval Markov chains using constraints ⋮ Smoothed model checking for uncertain continuous-time Markov chains
