The Finite Satisfiability Problem for PCTL is Undecidable

CHODIL, Miroslav a Antonín KUČERA. The Finite Satisfiability Problem for PCTL is Undecidable. Online. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science. New York, United States: IEEE Computer Society, 2024, s. 1-14. ISBN 979-8-4007-0660-8. Dostupné z: https://doi.org/10.1145/3661814.3662145.

Základní údaje

Originální název

The Finite Satisfiability Problem for PCTL is Undecidable

Autoři

CHODIL, Miroslav a Antonín KUČERA

Vydání

New York, United States, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, od s. 1-14, 14 s. 2024

Nakladatel

IEEE Computer Society

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Kód RIV

RIV/00216224:14330/24:00136941

Organizační jednotka

Fakulta informatiky

ISBN

979-8-4007-0660-8

ISSN

DOI

https://doi.org/10.1145/3661814.3662145

UT WoS

001275042100022

EID Scopus

2-s2.0-85199100766

Klíčová slova anglicky

Markov chains; probabilistic temporal logics

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

We show that the problem of whether a given PCTL formula has a finite model is undecidable. The undecidability result holds even for formulae of the form \phi_1 \wedge G=1 \phi_2 where the validity of \phi_1,\phi_2 depends only on the states reachable in at most two transitions. Consequently, the problem of whether a given PCTL formula is valid in all finite-state Markov chains is not even semi-decidable.

---

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/1592/2023, interní kód MU	Název: Modelování, analýza a verifikace (2024) Investor: Masarykova univerzita, Modelování, analýza a verifikace (2024)
MUNI/A/1608/2023, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 24 Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 24