On the Influence of Confluence in Modal Logics

Article type: Research Article

Authors: Gasquet, Olivier

Affiliations: Institut de Recherche en Informatique de Toulouse (IRIT) Université Paul Sabatier 118 route de Narbonne Toulouse Cedex 04, France. E-mail: gasquet@irit.fr

Abstract: In this paper we prove that adding a confluence axiom to a modal logic which behaves rather well from the viewpoint of complexity of the satisfaction problem, drastically increases its complexity and blows it up from PSPACE-completeness to NEXPTIME-completeness. More precisely, we investigate here both monomodal K + confluence and bimodal K with confluence between the two modalities.

Keywords: Modal Logics, Tableaux, Confluence, Complexity, Satisfaction problem, Tiling problem, NEXPTIME-completeness

Journal: Fundamenta Informaticae, vol. 70, no. 3, pp. 227-250, 2006