Room P3.10, Mathematics Building

Temporalization of exogenous probabilistic propositional logic

In this talk we address several properties of the Exogenous Probabilistic Propositional Logic (EPPL) with the purpose of introducing a temporal version - Exogenous Probabilistic Linear Temporal Logic (EPLTL). In detail, we give a small model theorem for EPPL and present a polynomial-space algorithm for the SAT problem of both EPPL and EPLTL. We also show that the model-checking problem of EPLTL is in PSPACE. Finally, we provide a (weakly) complete calculus for EPLTL. We conclude the talk by pointing out future work and open problems that will be pursued with C. Baier at TU. Dresden. Joint work with P. Mateus.