The Satisfiability Problem for a Quantitative Fragment of PCTL

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři

CHODIL Miroslav KUČERA Antonín

Rok publikování 2021
Druh Článek ve sborníku
Konference Fundamentals of Computation Theory. 23rd International Symposium, FCT 2021
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-030-86593-1_10
Klíčová slova Probabilistic temporal logic; satisfiability
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.