DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2020.7

Parametric Model Checking Continuous-Time Markov Chains

Authors: Catalin-Andrei Ilie and James Ben Worrell

Published in: LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)

Abstract

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.

Cite as

Catalin-Andrei Ilie and James Ben Worrell. Parametric Model Checking Continuous-Time Markov Chains. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{ilie_et_al:LIPIcs.TIME.2020.7,
  author =	{Ilie, Catalin-Andrei and Worrell, James Ben},
  title =	{{Parametric Model Checking Continuous-Time Markov Chains}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.7},
  URN =		{urn:nbn:de:0030-drops-129752},
  doi =		{10.4230/LIPIcs.TIME.2020.7},
  annote =	{Keywords: Probabilistic Continuous Stochastic Logic, Continuous-time Markov Chains, model checking, Schanuel’s Conjecture, positivity problem}
}

Search Results

Documents authored by Ilie, Catalin-Andrei

Parametric Model Checking Continuous-Time Markov Chains

Abstract

Cite as

Thanks for your feedback!

Could not send message