eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-09-15
7:1
7:18
10.4230/LIPIcs.TIME.2020.7
article
Parametric Model Checking Continuous-Time Markov Chains
Ilie, Catalin-Andrei
1
Worrell, James Ben
2
Department of Computer Science, University of Bucharest, Romania
Department of Computer Science, University of Oxford, UK
CSL is a well-known temporal logic for specifying properties of real-time stochastic systems, such as continuous-time Markov chains. We introduce PCSL, an extension of CSL that allows using existentially quantified parameters in timing constraints, and investigate its expressiveness and decidability over properties of continuous-time Markov chains. Assuming Schanuel’s Conjecture, we prove the decidability of model checking the one-parameter fragment of PCSL on continuous-time Markov chains. Technically, the central problem we solve (relying on Schanuel’s Conjecture) is to decide positivity of real-valued exponential polynomial functions on bounded intervals. A second contribution is to give a reduction of the Positivity Problem for matrix exponentials to the PCSL model checking problem, suggesting that it will be difficult to give an unconditional proof of the decidability of model checking PCSL.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol178-time2020/LIPIcs.TIME.2020.7/LIPIcs.TIME.2020.7.pdf
Probabilistic Continuous Stochastic Logic
Continuous-time Markov Chains
model checking
Schanuel’s Conjecture
positivity problem