CHODIL, Miroslav a Antonín KUČERA. The Satisfiability Problem for a Quantitative Fragment of PCTL. In Evripidis Bampis and Aris Pagourtzis. Fundamentals of Computation Theory. 23rd International Symposium, FCT 2021. Německo: Springer, 2021, s. 149-161. ISBN 978-3-030-86592-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-86593-1_10.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název The Satisfiability Problem for a Quantitative Fragment of PCTL
Autoři CHODIL, Miroslav (703 Slovensko, domácí) a Antonín KUČERA (203 Česká republika, garant, domácí).
Vydání Německo, Fundamentals of Computation Theory. 23rd International Symposium, FCT 2021, od s. 149-161, 13 s. 2021.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10200 1.2 Computer and information sciences
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/21:00119107
Organizační jednotka Fakulta informatiky
ISBN 978-3-030-86592-4
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-86593-1_10
UT WoS 000722594000010
Klíčová slova anglicky Probabilistic temporal logic; satisfiability
Štítky firank_B
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 25. 1. 2022 12:46.
Anotace
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ávaznosti
GA21-24711S, projekt VaVNázev: Efektivní analýza a optimalizace pravděpodobnostních systémů a her (Akronym: Efektivní analýza a optimalizace pravděpodobnostní)
Investor: Grantová agentura ČR, Efektivní analýza a optimalizace pravděpodobnostních systémů a her
MUNI/A/1108/2020, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X. (Akronym: SV-FI MAV X.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X.
MUNI/A/1549/2020, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21 (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21
VytisknoutZobrazeno: 13. 5. 2024 23:03