2026-07-24T01:45:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9570 2024-03-06T10:44:45Z ddc:004 open_access

The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL Kretínský, Jan Rotar, Alexej temporal logic probabilistic verification probabilistic computation tree logic satisfiability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jan Kretínský and Alexej Rotar 2018 Is Part Of LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2018.32 urn:nbn:de:0030-drops-95708 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.32 eng https://creativecommons.org/licenses/by/3.0/legalcode