FMT 1b: Computational complexity of first order logic

$% \usepackage{amsmath} % \usepackage{amsfonts} % \usepackage{amssymb} % create the definition symbol \def\bydef{\stackrel{\text{def}}{=}} \newcommand{\qed}{\mbox{ } \Box} \newcommand{\set}[1]{\{#1\}} \newcommand{\eps}{\varepsilon} \newcommand{\NN}{\mathbb N} \newcommand{\Nat}{\mathbb N} \newcommand{\RR}{\mathbb R} \newcommand{\Aa}{\mathcal A} \newcommand{\Bb}{\mathcal B} \newcommand{\Cc}{\mathcal C} \newcommand{\Dd}{\mathcal D} \newcommand{\Ll}{\mathcal L} \newcommand{\str}[1]{\mathbb {#1}} \renewcommand{\implies}{\rightarrow} \newcommand{\lor}{\vee} \newcommand{\land}{\wedge} \renewcommand{\phi}{\varphi} \renewcommand{\subset}{\subseteq} \newcommand{\models}{\vDash} \DeclareMathOperator{\dom}{Dom} \DeclareMathOperator{\ifp}{ifp} \DeclareMathOperator{\lfp}{lfp} \DeclareMathOperator{\gfp}{gfp} \DeclareMathOperator{\tcl}{tcl} \DeclareMathOperator{\ln}{ln} $

From now on, unless stated otherwise, we will consider relational signatures only, i.e., signatures consisting only of relational symbols. Structures over such signatures are relational structures.

Consider the following Model Checking decision problem for first order logic (for a fixed signature $\Sigma$):

Problem: Model Checking of First Order Logic

Input: a sentence $\phi$ of first order logic and a relational structure $\str A$

Decide: does $\phi$ hold in $\str A$?

We will study the computational complexity of this problem.

Representing structures.

The first question is: how is a structure $\str A$ represented on input? Implicitly, we assume that a signature $\Sigma=\set{\sigma_1,\ldots,\sigma_k}$ is fixed.

This can be done in several ways; every “natural” way is equally good. Here we describe one way of representing a structure $\str A$. A representation of $\str A$ consists of a list of identifiers of its elements (one unique binary string per each element of $\str A$) and, for each symbol $i=1,\ldots,k$, a list of the tuples of the interpretation of $\sigma_i$ in $\str A$, where each tuple is referred to by the identifiers of its components. Observe that the size of the representation is at least as large as the cardinality $|\str A|$ of the structure, and is bounded by $poly(|\str A|)$, where poly is a polynomial which depends only on the signature $\Sigma$ (we assume here that the identifiers of the elements form an initial segment of the natural numbers, written in binary).

Example. Consider a simple graph $G$ with two nodes connected by an (undirected) edge. Then $G$ has several representations, e.g. (0,1),((0,1),(1,0)) but also (1,0),((1,0),(0,1)).

Fix a formula $\phi$. What is the complexity of evaluating a fixed sentence $\phi$ on an input structure $\str A$, whose representation has size $n$? If $\phi$ has quantifier rank $k$ then $\phi$ can be evaluated on $\str A$ in time $O(n^{k+1})$ – one loop per each quantifier, and an additional factor $n$ for the time it takes to lookup whether a relation holds in the representation.

Therefore, the data complexity (when only $\str A$ – the data – is treated as input) of evaluation of FO is in PTime (because we treat $k$ as fixed). Also, it is in LogSpace – each loop introduces a variable which stores an identifier, and the size of the identifier is logarithmic in terms of the size of the structure, so even more so in terms of the size of its description. 

The combined complexity (when both $\str A$ and $\phi$ are given on input) of evaluation of first order logic is bounded by $O(n^n)$, where $n$ is the size of the input (since both the quantifier rank of $\phi$ and $\str A$ are bounded by $n$). Therefore, the combined complexity is in ExpTime. Also, it is in PSpace – since the number of identifiers needed to store at each level of the loop is bounded by the quantifier rank, which is bounded by $n$.

 

 

 

 

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>