The Satisfiability Problem for a Quantitative Fragment of PCTL

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.

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

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

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

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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 VaV	Ná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 MU	Ná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 MU	Ná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