License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2018.36
URN: urn:nbn:de:0030-drops-95743
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9574/
Go to the corresponding LIPIcs Volume Portal

Gorlin, Andrey ; Ramakrishnan, C. R.

Separable GPL: Decidable Model Checking with More Non-Determinism

pdf-format:
LIPIcs-CONCUR-2018-36.pdf (0.5 MB)

Abstract

Generalized Probabilistic Logic (GPL) is a temporal logic, based on the modal mu-calculus, for specifying properties of branching probabilistic systems. We consider GPL over branching systems that also exhibit internal non-determinism under linear-time semantics (which is resolved by schedulers), and focus on the problem of finding the capacity (supremum probability over all schedulers) of a fuzzy formula. Model checking GPL is undecidable, in general, over such systems, and existing GPL model checking algorithms are limited to systems without internal non-determinism, or to checking non-recursive formulae. We define a subclass, called separable GPL, which includes recursive formulae and for which model checking is decidable. A large class of interesting and decidable problems, such as termination of 1-exit Recursive MDPs, reachability of Branching MDPs, and LTL model checking of MDPs, whose decidability has been studied independently, can be reduced to model checking separable GPL. Thus, GPL is widely applicable and, with a suitable extension of its semantics, yields a uniform framework for studying problems involving systems with non-deterministic and probabilistic behaviors.

BibTeX - Entry

@InProceedings{gorlin_et_al:LIPIcs:2018:9574,
  author =	{Andrey Gorlin and C. R. Ramakrishnan},
  title =	{{Separable GPL: Decidable Model Checking with More Non-Determinism}},
  booktitle =	{29th International Conference on Concurrency Theory  (CONCUR 2018)},
  pages =	{36:1--36:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Sven Schewe and Lijun Zhang},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9574},
  URN =		{urn:nbn:de:0030-drops-95743},
  doi =		{10.4230/LIPIcs.CONCUR.2018.36},
  annote =	{Keywords: Modal mu-calculus, probabilistic logics, probabilistic systems, branching systems, model checking}
}

Keywords: Modal mu-calculus, probabilistic logics, probabilistic systems, branching systems, model checking
Collection: 29th International Conference on Concurrency Theory (CONCUR 2018)
Issue Date: 2018
Date of publication: 31.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI