The Satisfiability Problem for a Quantitative Fragment of PCTL

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.

21 Jul 2021 Antonín Kučera

FCT Proceedings

Authors: Miroslav Chodil, Antonín Kučera

Arxiv submission

More articles

All articles

You are running an old browser version. We recommend updating your browser to its latest version.

More info