The Satisfiability Problem for a Quantitative Fragment of PCTL

CHODIL, Miroslav and Antonín KUČERA. The Satisfiability Problem for a Quantitative Fragment of PCTL. In Evripidis Bampis and Aris Pagourtzis. Fundamentals of Computation Theory. 23rd International Symposium, FCT 2021. Německo: Springer, 2021, p. 149-161. ISBN 978-3-030-86592-4. Available from: https://dx.doi.org/10.1007/978-3-030-86593-1_10.

Basic information

Original name

The Satisfiability Problem for a Quantitative Fragment of PCTL

Authors

CHODIL, Miroslav (703 Slovakia, belonging to the institution) and Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution)

Edition

Německo, Fundamentals of Computation Theory. 23rd International Symposium, FCT 2021, p. 149-161, 13 pp. 2021

Publisher

Springer

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/21:00119107

Organization unit

Faculty of Informatics

ISBN

978-3-030-86592-4

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-86593-1_10

UT WoS

000722594000010

Keywords in English

Probabilistic temporal logic; satisfiability

Tags

core_B, firank_B

Tags

International impact, Reviewed

---

Abstract

V originále

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.

---

Links

GA21-24711S, research and development project	Name: Efektivní analýza a optimalizace pravděpodobnostních systémů a her (Acronym: Efektivní analýza a optimalizace pravděpodobnostní) Investor: Czech Science Foundation
MUNI/A/1108/2020, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace X. (Acronym: SV-FI MAV X.) Investor: Masaryk University
MUNI/A/1549/2020, interní kód MU	Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 21 (Acronym: SKOMU) Investor: Masaryk University