1 Search Results for "Gorlin, Andrey"


Document
Separable GPL: Decidable Model Checking with More Non-Determinism

Authors: Andrey Gorlin and C. R. Ramakrishnan

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


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.

Cite as

Andrey Gorlin and C. R. Ramakrishnan. Separable GPL: Decidable Model Checking with More Non-Determinism. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{gorlin_et_al:LIPIcs.CONCUR.2018.36,
  author =	{Gorlin, Andrey and Ramakrishnan, C. R.},
  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 =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.36},
  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}
}
  • Refine by Author
  • 1 Gorlin, Andrey
  • 1 Ramakrishnan, C. R.

  • Refine by Classification
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 1 Modal mu-calculus
  • 1 branching systems
  • 1 model checking
  • 1 probabilistic logics
  • 1 probabilistic systems

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail