The Satisfiability Problem for a Quantitative Fragment of PCTL

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

CHODIL Miroslav KUČERA Antonín

Year of publication 2021
Type Article in Proceedings
Conference Fundamentals of Computation Theory. 23rd International Symposium, FCT 2021
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-030-86593-1_10
Keywords Probabilistic temporal logic; satisfiability
Description 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.
Related projects:

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