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.32
URN: urn:nbn:de:0030-drops-95708
URL: http://dagstuhl.sunsite.rwth-aachen.de/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
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