The Satisfiability Problem for a Quantitative Fragment of PCTL
Logic in Computer Science
2021-07-09 v1
Abstract
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.
Cite
@article{arxiv.2107.03794,
title = {The Satisfiability Problem for a Quantitative Fragment of PCTL},
author = {Miroslav Chodil and Antonín Kučera},
journal= {arXiv preprint arXiv:2107.03794},
year = {2021}
}