Decidability and Complexity of Some Finitely-valued Dynamic Logics

Propositional Dynamic Logic, PDL, is a well known modal logic formalizing reasoning about complex actions. We study many-valued generalizations of PDL based on relational models where satisfaction of formulas in states and accessibility between states via action execution are both seen as graded notions, evaluated in a finite Łukasiewicz chain. For each n>1, the logic PDŁn is obtained using the n-element Łukasiewicz chain, PDL being equivalent to PDŁ2. These finitely-valued dynamic logics can be applied in formalizing reasoning about actions specified by graded predicates, reasoning about costs of actions, and as a framework for certain graded description logics with transitive closure of roles. Generalizing techniques used in the case of PDL we obtain completeness and decidability results for all PDŁn. A generalization of Pratt's exponential-time algorithm for checking validity of formulas is given and EXPTIME-hardness of each PDŁn validity problem is established by embedding PDL into PDŁn.