License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2018.32
URN: urn:nbn:de:0030-drops-95708
URL: http://drops.dagstuhl.de/opus/volltexte/2018/9570/
Go to the corresponding LIPIcs Volume Portal


Kretínský, Jan ; Rotar, Alexej

The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL

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


Abstract

We investigate the satisfiability and finite satisfiability problem for probabilistic computation-tree logic (PCTL) where operators are not restricted by any step bounds. We establish decidability for several fragments containing quantitative operators and pinpoint the difficulties arising in more complex fragments where the decidability remains open.

BibTeX - Entry

@InProceedings{kretnsk_et_al:LIPIcs:2018:9570,
  author =	{Jan Kret{\'i}nsk{\'y} and Alexej Rotar},
  title =	{{The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL}},
  booktitle =	{29th International Conference on Concurrency Theory  (CONCUR 2018)},
  pages =	{32:1--32: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/9570},
  URN =		{urn:nbn:de:0030-drops-95708},
  doi =		{10.4230/LIPIcs.CONCUR.2018.32},
  annote =	{Keywords: temporal logic, probabilistic verification, probabilistic computation tree logic, satisfiability}
}

Keywords: temporal logic, probabilistic verification, probabilistic computation tree logic, satisfiability
Seminar: 29th International Conference on Concurrency Theory (CONCUR 2018)
Issue Date: 2018
Date of publication: 13.08.2018


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