DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2017.35

Complexity of Model Checking MDPs against LTL Specifications

Authors: Dileep Kini and Mahesh Viswanathan

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract

Given a Markov Decision Process (MDP) M, an LTL formula \varphi, and a threshold \theta \in [0,1], the verification question is to determine if there is a scheduler with respect to which the executions of M satisfying \varphi have probability greater than (or greater than or equal to) \theta. When \theta = 0, we call it the qualitative verification problem, and when \theta \in (0,1], we call it the quantitative verification problem. In this paper we study the precise complexity of these problems when the specification is constrained to be in different fragments of LTL.

Cite as

Dileep Kini and Mahesh Viswanathan. Complexity of Model Checking MDPs against LTL Specifications. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 35:1-35:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kini_et_al:LIPIcs.FSTTCS.2017.35,
  author =	{Kini, Dileep and Viswanathan, Mahesh},
  title =	{{Complexity of Model Checking MDPs against LTL Specifications}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{35:1--35:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.35},
  URN =		{urn:nbn:de:0030-drops-83928},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.35},
  annote =	{Keywords: Markov Decision Processes, Linear Temporal Logic, model checking, complexity}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2011.78

Using non-convex approximations for efficient analysis of timed automata

Authors: Frédéric Herbreteau, Dileep Kini, B. Srivathsan, and Igor Walukiewicz

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract

The reachability problem for timed automata asks if there exists a path from an initial state to a target state. The standard solution to this problem involves computing the zone graph of the automaton, which in principle could be infinite. In order to make the graph finite, zones are approximated using an extrapolation operator. For reasons of efficiency in current algorithms extrapolation of a zone is always a zone; and in particular it is convex. In this paper, we propose to solve the reachability problem without such extrapolation operators. To ensure termination, we provide an efficient algorithm to check if a zone is included in the so called region closure of another. Although theoretically better, closure cannot be used in the standard algorithm since a closure of a zone may not be convex. An additional benefit of the proposed approach is that it permits to calculate approximating parameters on-the-fly during exploration of the zone graph, as opposed to the current methods which do it by a static analysis of the automaton prior to the exploration. This allows for further improvements in the algorithm. Promising experimental results are presented.

Cite as

Frédéric Herbreteau, Dileep Kini, B. Srivathsan, and Igor Walukiewicz. Using non-convex approximations for efficient analysis of timed automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 78-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{herbreteau_et_al:LIPIcs.FSTTCS.2011.78,
  author =	{Herbreteau, Fr\'{e}d\'{e}ric and Kini, Dileep and Srivathsan, B. and Walukiewicz, Igor},
  title =	{{Using non-convex approximations for efficient analysis of timed automata}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{78--89},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.78},
  URN =		{urn:nbn:de:0030-drops-33619},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.78},
  annote =	{Keywords: Timed Automata, Model-checking, Non-convex abstraction, On-the-fly abstraction}
}

Search Results

Documents authored by Kini, Dileep

Complexity of Model Checking MDPs against LTL Specifications

Abstract

Cite as

Using non-convex approximations for efficient analysis of timed automata

Abstract

Cite as

Thanks for your feedback!

Could not send message