The Satisfiability Problem for a Quantitative Fragment of PCTL

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F21%3A00119107" target="_blank" >RIV/00216224:14330/21:00119107 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-030-86593-1_10" target="_blank" >http://dx.doi.org/10.1007/978-3-030-86593-1_10</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-86593-1_10" target="_blank" >10.1007/978-3-030-86593-1_10</a>

Result language
angličtina
Original language name
The Satisfiability Problem for a Quantitative Fragment of PCTL
Original language description
We give a sufficient condition under which every finite-satisfiable formula of a given PCTL fragment has a model with at most doubly exponential number of states (consequently, the finite satisfiability problem for the fragment is in 2-EXPSPACE). The condition is semantic and it is based on enforcing a form of ``progress'' in non-bottom SCCs contributing to the satisfaction of a given PCTL formula. We show that the condition is satisfied by PCTL fragments beyond the reach of existing methods.
Czech name
—
Czech description
—

Project
<a href="/en/project/GA21-24711S" target="_blank" >GA21-24711S: Efficient Analysis and Optimization for Probabilistic Systems and Games</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Fundamentals of Computation Theory. 23rd International Symposium, FCT 2021
ISBN
9783030865924
ISSN
0302-9743
e-ISSN
—
Number of pages
13
Pages from-to
149-161
Publisher name
Springer
Place of publication
Německo
Event location
Athens, Greece
Event date
Sep 12, 2021
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000722594000010

Similar results(10)