3 papers
cs.LO2025
The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable
Miroslav Chodil, Antonín Kučera
The Probabilistic Computational Tree Logic (PCTL) is the main specification formalism for discrete probabilistic systems modeled by Markov chains. Despite serious research attempts…
cs.LO2024
The General and Finite Satisfiability Problems for PCTL are Undecidable
Miroslav Chodil, Antonín Kučera
The general/finite PCTL satisfiability problem asks whether a given PCTL formula has a general/finite model. We show that the finite PCTL satisfiability problem is undecidable, and…
cs.LO2021
The Satisfiability Problem for a Quantitative Fragment of PCTL
Miroslav Chodil, Antonín Kučera
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…