D 2021

The Satisfiability Problem for a Quantitative Fragment of PCTL

CHODIL, Miroslav a Antonín KUČERA

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
Změněno: 25. 1. 2022 12:46, prof. RNDr. Antonín Kučera, Ph.D.

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
Zobrazeno: 3. 11. 2024 14:23