The Satisfiability Problem for a Quantitative Fragment of PCTL
Identifikátory výsledku
Kód výsledku v 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>
Výsledek na webu
<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>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
The Satisfiability Problem for a Quantitative Fragment of PCTL
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
The Satisfiability Problem for a Quantitative Fragment of PCTL
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10200 - Computer and information sciences
Návaznosti výsledku
Projekt
<a href="/cs/project/GA21-24711S" target="_blank" >GA21-24711S: Efektivní analýza a optimalizace pravděpodobnostních systémů a her</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2021
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Fundamentals of Computation Theory. 23rd International Symposium, FCT 2021
ISBN
9783030865924
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
13
Strana od-do
149-161
Název nakladatele
Springer
Místo vydání
Německo
Místo konání akce
Athens, Greece
Datum konání akce
12. 9. 2021
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
000722594000010