
We study rewritability of monadic disjunctive Datalog programs, (the
complements of) MMSNP sentences, and ontologymediated queries (OMQs) based on
expressive description logics of the ALC family and on conjunctive queries. We
show that rewritability into FO and into monadic Datalog (MDLog) are decidable,
and that rewritability into Datalog is decidable when the original query
satisfies a certain condition related to equality. We establish
2NExpTimecompleteness for all studied problems except rewritability into MDLog
for which there remains a gap between 2NExpTime and 3ExpTime. We also analyze
the shape of rewritings, which in the MMSNP case correspond to obstructions,
and give a new construction of canonical Datalog programs that is more
elementary than existing ones and also applies to formulas with free variables.

We develop firstorder logic and some extensions for incomplete information
scenarios and consider related complexity issues.

It was recently shown by van den Broeck at al. that the symmetric weighted
firstorder model counting problem (WFOMC) for sentences of twovariable logic
FO2 is in polynomial time, while it is SharpP_1 complete for some
FO3sentences. We extend the result for FO2 in two independent directions: to
sentences of the form "phi and \forall\exists^=1 psi" with phi and psi in FO2,
and to sentences formulated in the uniform onedimensional fragment of FO, a
recently introduced extension of twovariable logic with the capacity to deal
with relation symbols of all arities. Note that the former generalizes the
extension of FO2 with a functional relation symbol. We also identify a complete
classification of firstorder prefix classes according to whether WFOMC is in
polynomial time or SharpP_1 complete.

We investigate the computational complexity of the satisfiability problem of
modal inclusion logic. We distinguish two variants of the problem: one for the
strict and another one for the lax semantics. Both problems turn out to be
EXPTIMEcomplete on general structures. Finally, we show how for a specific
class of structures NEXPTIMEcompleteness for these problems under strict
semantics can be achieved.

We study pure coordination games where in every outcome, all players have
identical payoffs, 'win' or 'lose'. We identify and discuss a range of 'purely
rational principles' guiding the reasoning of rational players in such games
and analyze which classes of coordination games can be solved by such players
with no preplay communication or conventions. We observe that it is highly
nontrivial to delineate a boundary between purely rational principles and other
decision methods, such as conventions, for solving such coordination games.

We investigate the decidability of the emptiness problem for three classes of
distributed automata. These devices operate on finite directed graphs, acting
as networks of identical finitestate machines that communicate in an infinite
sequence of synchronous rounds. The problem is shown to be decidable in
LogSpace for a class of forgetful automata, where the nodes see the messages
received from their neighbors but cannot remember their own state. When
restricted to the appropriate families of graphs, these forgetful automata are
equivalent to classical finite word automata, but strictly more expressive than
finite tree automata. On the other hand, we also show that the emptiness
problem is undecidable in general. This already holds for two heavily
restricted classes of distributed automata: those that reject immediately if
they receive more than one message per round, and those whose state diagram
must be acyclic except for selfloops.

We define a semantics for firstorder logic with generalized quantifiers
based on double teams. We also define and investigate a notion of a generalized
atom. Such atoms can be used in order to define extensions of firstorder logic
with a teambased semantics. We also define a game semantics and compare it
with the double team semantics.

We introduce a new gametheoretic semantics (GTS) for the modal mucalculus.
Our socalled bounded GTS replaces parity games with novel alternative
evaluation games where only finite paths arise. Infinite paths are not needed
even when the considered transition system is infinite.

We introduce versions of gametheoretic semantics (GTS) for AlternatingTime
Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a
winning strategy in a semantic evaluation game, and thus the gametheoretic
perspective appears in the framework of ATL on two semantic levels: on the
object level in the standard semantics of the strategic operators, and on the
metalevel where gametheoretic logical semantics is applied to ATL. We unify
these two perspectives into semantic evaluation games specially designed for
ATL. The gametheoretic perspective enables us to identify new variants of the
semantics of ATL based on limiting the time resources available to the verifier
and falsifier in the semantic evaluation game. We introduce and analyse an
unbounded and (ordinal) bounded GTS and prove these to be equivalent to the
standard (Tarskistyle) compositional semantics. We show that in these both
versions of GTS, truth of ATL formulae can always be determined in finite time,
i.e., without constructing infinite paths. We also introduce a nonequivalent
finitely bounded semantics and argue that it is natural from both logical and
gametheoretic perspectives.

Propositional and modal inclusion logic are formalisms that belong to the
family of logics based on team semantics. This article investigates the model
checking and validity problems of these logics. We identify complexity bounds
for both problems, covering both lax and strict team semantics. By doing so, we
come close to finalising the programme that ultimately aims to classify the
complexities of the central reasoning problems for modal and propositional
dependence, independence, and inclusion logics.

We develop gametheoretic semantics (GTS) for the fragment ATL+ of the full
Alternatingtime Temporal Logic ATL*, essentially extending a recently
introduced GTS for ATL. We first show that the new gametheoretic semantics is
equivalent to the standard semantics of ATL+ (based on perfect recall
strategies). We then provide an analysis, based on the new semantics, of the
memory and time resources needed for model checking ATL+. Based on that, we
establish that strategies that use only a very limited amount of memory suffice
for ATL+. Furthermore, using the GTS we provide a new algorithm for model
checking of ATL+ and identify a natural hierarchy of tractable fragments of
ATL+ that extend ATL.

This paper investigates formal logics for reasoning about determinacy and
independence. Propositional Dependence Logic D and Propositional Independence
Logic I are recently developed logical systems, based on team semantics, that
provide a framework for such reasoning tasks. We introduce two new logics L_D
and L_I, based on Kripke semantics, and propose them as alternatives for D and
I, respectively. We analyze the relative expressive powers of these four logics
and discuss the way these systems relate to natural language. We argue that L_D
and L_I naturally resolve a range of interpretational problems that arise in D
and I. We also obtain sound and complete axiomatizations for L_D and L_I.

We study the complexity of predicate logics based on team semantics. We show
that the satisfiability problems of twovariable independence logic and
inclusion logic are both NEXPTIMEcomplete. Furthermore, we show that the
validity problem of twovariable dependence logic is undecidable, thereby
solving an open problem from the team semantics literature. We also briefly
analyse the complexity of the BernaysSch\"onfinkelRamsey prefix classes of
dependence logic.

The uniform onedimensional fragment of firstorder logic, U1, is a recently
introduced formalism that extends twovariable logic in a natural way to
contexts with relations of all arities. We survey properties of U1 and
investigate its relationship to description logics designed to accommodate
higher arity relations, with particular attention given to DLR_reg. We also
define a description logic version of a variant of U1 and prove a range of new
results concerning the expressivity of U1 and related logics.

Uniform onedimensional fragment UF1^= is a formalism obtained from
firstorder logic by limiting quantification to applications of blocks of
existential (universal) quantifiers such that at most one variable remains free
in the quantified formula. The fragment is closed under Boolean operations, but
additional restrictions (called uniformity conditions) apply to combinations of
atomic formulas with two or more variables. The fragment can be seen as a
canonical generalization of twovariable logic, defined in order to be able to
deal with relations of arbitrary arities. The fragment was introduced recently,
and it was shown that the satisfiability problem of the equalityfree fragment
of UF1^= is decidable. In this article we establish that the satisfiability and
finite satisfiability problems of UF1^= are NEXPTIMEcomplete. We also show
that the corresponding problems for the extension of UF1^= with counting
quantifiers are undecidable. In addition to decidability questions, we compare
the expressivities of UF1^= and twovariable logic with counting quantifiers
FOC^2. We show that while the logics are incomparable in general, UF1^= is
strictly contained in FOC^2 when attention is restricted to vocabularies with
the arity bound two.

The immediate past has witnessed an increased amount of interest in local
algorithms, i.e., constant time distributed algorithms. In a recent survey of
the topic (Suomela, ACM Computing Surveys, 2013), it is argued that local
algorithms provide a natural framework that could be used in order to
theoretically control infinite networks in finite time. We study a
comprehensive collection of distributed computing models and prove that if
infinite networks are included in the class of structures investigated, then
every universally halting distributed algorithm is in fact a local algorithm.
To contrast this result, we show that if only finite networks are allowed, then
even very weak distributed computing models can define nonlocal algorithms that
halt everywhere. The investigations in this article continue the studies in the
intersection of logic and distributed computing initiated in (Hella et al.,
PODC 2012) and (Kuusisto, CSL 2013).

We introduce a natural Turingcomplete extension of firstorder logic FO. The
extension adds two novel features to FO. The first one of these is the capacity
to add new points to models and new tuples to relations. The second one is the
possibility of recursive looping when a formula is evaluated using a semantic
game. We first define a gametheoretic semantics for the logic and then prove
that the expressive power of the logic corresponds in a canonical way to the
recognition capacity of Turing machines. Finally, we show how to incorporate
generalized quantifiers into the logic and argue for a highly natural
connection between oracles and generalized quantifiers.

It is well known that dependence logic captures the complexity class NP, and
it has recently been shown that inclusion logic captures P on ordered models.
These results demonstrate that team semantics offers interesting new
possibilities for descriptive complexity theory. In order to properly
understand the connection between team semantics and descriptive complexity, we
introduce an extension D* of dependence logic that can define exactly all
recursively enumerable classes of finite models. Thus D* provides an approach
to computation alternative to Turing machines. The essential novel feature in
D* is an operator that can extend the domain of the considered model by a
finite number of fresh elements. Due to the close relationship between
generalized quantifiers and oracles, we also investigate generalized
quantifiers in team semantics. We show that monotone quantifiers of type (1)
can be canonically eliminated from quantifier extensions of firstorder logic
by introducing corresponding generalized dependence atoms.

We introduce a novel decidable fragment of firstorder logic. The fragment is
onedimensional in the sense that quantification is limited to applications of
blocks of existential (universal) quantifiers such that at most one variable
remains free in the quantified formula. The fragment is closed under Boolean
operations, but additional restrictions (called uniformity conditions) apply to
combinations of atomic formulae with two or more variables. We argue that the
notions of onedimensionality and uniformity together offer a novel perspective
on the robust decidability of modal logics. We also establish that minor
modifications to the restrictions of the syntax of the onedimensional fragment
lead to undecidable formalisms. Namely, the twodimensional and nonuniform
onedimensional fragments are shown undecidable. Finally, we prove that with
regard to expressivity, the onedimensional fragment is incomparable with both
the guarded negation fragment and twovariable logic with counting. Our proof
of the decidability of the onedimensional fragment is based on a technique
involving a direct reduction to the monadic class of firstorder logic. The
novel technique is itself of an independent mathematical interest.

Tarski initiated a logicbased approach to formal geometry that studies
firstorder structures with a ternary betweenness relation \beta, and a
quaternary equidistance relation \equiv. Tarski established, inter alia, that
the firstorder (FO) theory of (R^2,\beta,\equiv) is decidable. Aiello and van
Benthem (2002) conjectured that the FOtheory of expansions of (R^2,\beta) with
unary predicates is decidable. We refute this conjecture by showing that for
all n>1, the FOtheory of the class of expansions of (R^2,\beta) with just one
unary predicate is not even arithmetical. We also define a natural and
comprehensive class C of geometric structures (T,\beta), and show that for each
structure (T,\beta) in C, the FOtheory of the class of expansions of (T,\beta)
with a single unary predicate is undecidable. We then consider classes of
expansions of structures (T,\beta) with a restricted unary predicate, for
example a finite predicate, and establish a variety of related undecidability
results. In addition to decidability questions, we briefly study the
expressivities of universal MSO and weak universal MSO over expansions of
(R^n,\beta). While the logics are incomparable in general, over expansions of
(R^n,\beta), formulae of weak universal MSO translate into equivalent formulae
of universal MSO.

This work presents a classification of weak models of distributed computing.
We focus on deterministic distributed algorithms, and study models of computing
that are weaker versions of the widelystudied portnumbering model. In the
portnumbering model, a node of degree d receives messages through d input
ports and sends messages through d output ports, both numbered with 1,2,...,d.
In this work, VVc is the class of all graph problems that can be solved in the
standard portnumbering model. We study the following subclasses of VVc:
VV: Input port i and output port i are not necessarily connected to the same
neighbour.
MV: Input ports are not numbered; algorithms receive a multiset of messages.
SV: Input ports are not numbered; algorithms receive a set of messages.
VB: Output ports are not numbered; algorithms send the same message to all
output ports.
MB: Combination of MV and VB.
SB: Combination of SV and VB.
Now we have many trivial containment relations, such as SB \subseteq MB
\subseteq VB \subseteq VV \subseteq VVc, but it is not obvious if, for example,
either of VB \subseteq SV or SV \subseteq VB should hold. Nevertheless, it
turns out that we can identify a linear order on these classes. We prove that
SB \subsetneq MB = VB \subsetneq SV = MV = VV \subsetneq VVc. The same holds
for the constanttime versions of these classes.
We also show that the constanttime variants of these classes can be
characterised by a corresponding modal logic. Hence the linear order identified
in this work has direct implications in the study of the expressibility of
modal logic. Conversely, one can use tools from modal logic to study these
classes.

Tarski initiated a logicbased approach to formal geometry that studies
firstorder structures with a ternary betweenness relation (\beta) and a
quaternary equidistance relation (\equiv). Tarski established, inter alia, that
the firstorder (FO) theory of (R^2,\beta,\equiv) is decidable. Aiello and van
Benthem (2002) conjectured that the FOtheory of expansions of (R^2,\beta) with
unary predicates is decidable. We refute this conjecture by showing that for
all n>1, the FOtheory of monadic expansions of (R^2,\beta) is \Pi^1_1hard and
therefore not even arithmetical. We also define a natural and comprehensive
class C of geometric structures (T,\beta), where T is a subset of R^2, and show
that for each structure (T,\beta) in C, the FOtheory of the class of monadic
expansions of (T,\beta) is undecidable. We then consider classes of expansions
of structures (T,\beta) with restricted unary predicates, for example finite
predicates, and establish a variety of related undecidability results. In
addition to decidability questions, we briefly study the expressivity of
universal MSO and weak universal MSO over expansions of (R^n,\beta). While the
logics are incomparable in general, over expansions of (R^n,\beta), formulae of
weak universal MSO translate into equivalent formulae of universal MSO.
This is an extended version of a publication in the proceedings of the 21st
EACSL Annual Conferences on Computer Science Logic (CSL 2012).

We study the twovariable fragments D^2 and IF^2 of dependence logic and
independencefriendly logic. We consider the satisfiability and finite
satisfiability problems of these logics and show that for D^2, both problems
are NEXPTIMEcomplete, whereas for IF^2, the problems are undecidable. We also
show that D^2 is strictly less expressive than IF^2 and that already in D^2,
equicardinality of two unary predicates and infinity can be expressed (the
latter in the presence of a constant symbol). This is an extended version of a
publication in the proceedings of the 26th Annual IEEE Symposium on Logic in
Computer Science (LICS 2011).