The Satisfiability Problem for a Quantitative Fragment of PCTL

• 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
• 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

• Efektivní analýza a optimalizace pravděpodobnostních systémů a her
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X.
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21