3
$\begingroup$

This is kind of multiple questions in one. Let's consider $\phi$ a formula in the basic modal language (that is, in propositional language based on a set of propositional variables $\Phi$, plus one of the basic modal operators, say, $\Diamond$)

1) Define the $\phi-\mathsf{MODEL}$ problem as: Given a finite structure $M = (W, R, V, w)$, where $W$ is a set, $R \subseteq W \times W$, $V : \Phi \rightarrow 2^W$ and $w \in W$, is $\phi$ satisfied in $M$, as per the usual modal logic definition of satisfiability?

2) Define the $\phi-\mathsf{FRAME}$ problem as: Given a finite structure $F = (W, R)$, where $W$ is a set and $R \subseteq W \times W$ is $\phi$ valid in $F$, as per the usual modal logic definition of validity?

We could go on and define other variants, asking if there is a world in which the formula is satisfied (or valid), if there is a valuation such that the formula is satisfied, and so on.

Now consider, for example, the collection of $\phi-\mathsf{MODEL}$ problems, for all basic modal formulas $\phi$. My question could be formulated as thus: Is this class of problems equal to any well-known complexity class? Of course, the question could be formulated for any of the variants i just proposed, so it's as i said earlier, kind of multiple questions in one.

(It goes without saying, but for other logics, such as first and second-order logics, this is a much-studied subject with the name Descriptive Complexity, with classic results such as Fagin's Theorem relating the existential fragment of second-order logic to the complexity class NP)

|cite|improve this question
$\endgroup$
  • $\begingroup$ It would be helpful if you could tell us a bit of context, eg. where the question came up, and what you already know. $\endgroup$ – Jan Johannsen Dec 2 '13 at 10:19
  • $\begingroup$ @JanJohannsen: I'm an undergraduate student in Computer Science, who took a few classes on Modal Logic (mostly following Blackburn, Venema and De Rijke's textbook of the same name), and am enrolled in a class about Computational Complexity (following Papadimitriou's textbook, also of the same name). It's hard to quantify what i already know, but as for where the question came, i guess that's easy; a few google searches on "descriptive complexity of modal logic" didn't turn anything easy to digest (then again i've never been the finest google searcher) $\endgroup$ – hcp Dec 2 '13 at 23:39
5
$\begingroup$

Modal logic does not capture any interesting complexity class. As it is invariant under bisimulation, it cannot even test whether the vertex $w$ has degree greater than $2$, which is a constant time property. We are interested in ML for a different reason: ML is the bisimulation invariant fragment of first-order logic (Theorem of van Benthem). In other words, ML is the "first-order logic of process behaviour". Similarly, the bisimulation invariant fragment of monadic second-order logic is the $\mu$-calculus (Theorem of Janin/Walukiewicz).

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Hold on. Even propositional logic captures an "interesting" complexity class - namely, $NC_0$ (actually i'm not sure but it seems simple enough to prove, given that $NC_0$ problems are limited to a constant number of bits of the input). Not only that, but if you look at basic modal logic at the level of frames, it is able to define frame classes not definable in first-order logic (though i'm not sure how exactly this relates to problems, since these must be a collection of finite structures). Surely if viewed at that level it becomes interesting enough? $\endgroup$ – hcp Dec 2 '13 at 23:40
  • $\begingroup$ But your remark about the $\mu$-calculus interests me; given Van Benthem's Theorem, and knowing that modal logic viewed at the level of frames has a natural translation into monadic second-order logic, i'd have expected that fragment to be the bisimulation invariant one . The $mu$-calculus seems rather complicated, in contrast. (Actually, there's nothing in particular i'd expect; i know nothing about bisimulation invariance other than what it obiously means) $\endgroup$ – hcp Dec 2 '13 at 23:40
  • $\begingroup$ I did not think about propositional logic capturing anything, because it does not naturally speak about structures... Modal logic has a natural translation even to first-order logic and hence has the same weakness in expressing non-local properties as FO (Theorem of Gaifman). Monadic second-order on the other hand can express non-local properties - so can the $\mu$-calculus, which allows definable recursion. $\endgroup$ – Sebastian Siebertz Dec 4 '13 at 12:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.