Ockhamist Propositional Dynamic Logic (OPDL) is a logic unifying the family of dynamic logics and the family of branching-time temporal logics, two families of logic widely used in AI to model reactive systems and multi-agent systems (MAS). In this paper, we present two variants of this logic. These two logics share the same language and differ only in one semantic condition. The first logic embeds Bundled CTL∗ while the second embeds CTL∗. We provide a 2EXPTIME decision procedure for the satisfiability problem of each variant. The decision procedure for the first variant of OPDL is based on the elimination of Hintikka sets while the decision procedure for the second variant relies on automata.
CITATION STYLE
Boudou, J., & Lorini, E. (2016). Decidability and expressivity of ockhamist propositional dynamic logics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10021 LNAI, pp. 144–158). Springer Verlag. https://doi.org/10.1007/978-3-319-48758-8_10
Mendeley helps you to discover research relevant for your work.