Complexity of model checking MDPs against LTL specifications

DOI10.4230/LIPICS.FSTTCS.2017.35MaRDI QIDQ5136327zbMATH OpenOpenAlexFDO

Authors Dileep Kini, Mahesh Viswanathan

Publication date 25 November 2020

Full work available at URL https://doi.org/10.4230/lipics.fsttcs.2017.35

zbMATH Keywords

complexitymodel checkingMarkov decision processeslinear temporal logic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Parametric LTL on Markov chains
• Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
• The complexity of probabilistic verification
• Model checking probabilistic systems
• Qualitative Logics and Equivalences for Probabilistic Systems

Cites work

• scientific article; zbMATH DE number 1948167 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Deterministic generators and games for LTL fragments
• Limit-deterministic Büchi automata for linear temporal logic
• Playing games with boxes and diamonds.
• Probabilistic Automata for Safety LTL Specifications
• The complexity of probabilistic verification

Cited in

(2)

• Computer Science Logic
• scientific article; zbMATH DE number 7559425 (Why is no real title available?)

This page was built for publication: Complexity of model checking MDPs against LTL specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5136327)