How Easy it is to Know How: An Upper Bound for the Satisfiability Problem

TL;DR

This paper establishes an upper bound of a_2^P for the satisfiability problem of a modal logic involving 'knowing how' assertions, using an algorithm that eliminates nested modalities and leverages propositional satisfiability checks.

Contribution

It provides the first complexity upper bound for the satisfiability problem of a modal logic of 'knowing how' based on linear plans.

Findings

Satisfiability checking is in a_2^P complexity class.

An algorithm for satisfiability involves eliminating nested modalities.

The approach uses multiple calls to propositional satisfiability oracles.

Abstract

We investigate the complexity of the satisfiability problem for a modal logic expressing `knowing how' assertions, related to an agent's abilities to achieve a certain goal. We take one of the most standard semantics for this kind of logics based on linear plans. Our main result is a proof that checking satisfiability of a `knowing how' formula can be done in $\Sigma_2^P$. The algorithm we present relies on eliminating nested modalities in a formula, and then performing multiple calls to a satisfiability checking oracle for propositional logic.