The Satisfiability Problem for a Quantitative Fragment of PCTL

TL;DR

This paper establishes a semantic condition ensuring finite models with doubly exponential states for certain PCTL formulas, advancing the understanding of satisfiability in probabilistic temporal logic.

Contribution

It introduces a new semantic condition that guarantees finite models for PCTL fragments, extending the applicability beyond existing methods.

Findings

Finite models have at most doubly exponential states under the condition.

Finite satisfiability problem for the fragment is in 2-EXPSPACE.

The condition applies to PCTL fragments beyond current techniques.

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.