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: https://drops.dagstuhl.de/opus/volltexte/2018/9570/
Kretínský, Jan ; Rotar, Alexej
The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL
| pdf-format: |
|
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: | 31.08.2018 |
