J 2026

The Finite Satisfiability Problem for PCTL is Undecidable

CHODIL, Miroslav a Antonín KUČERA

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í

JOURNAL OF THE ACM, 2026, 0004-5411

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

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í

Odkazy

Impakt faktor

Impact factor: 2.500 v roce 2024

Označené pro přenos do RIV

Ano

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

Klíčová slova anglicky

Probabilistic temporal logics; satisfiability

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 17. 3. 2026 22:48, prof. RNDr. Antonín Kučera, Ph.D.

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 F1 \wedge G=1 F2 where the validity of F1, F2 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

GA26-23441S, interní kód MU
Název: Advanced Method for Analysis and Synthesis of Probabilistic Programs
Investor: Grantová agentura ČR, Advanced Method for Analysis and Synthesis of Probabilistic Programs
101087529, interní kód MU
Název: Cyber-security Excellence Hub in Estonia and South Moravia (CHESS)
Investor: Evropská unie, Cyber-security Excellence Hub in Estonia and South Moravia (CHESS), Rozšiřování účasti a posílení ERA