Wednesday 18 September — Tutorials
09:3013:00Tutorial
09:3013:00Jérôme
Leroux Tutorial: The reachability problem for Petri nets
SLIDES speaker: Jérôme Leroux
Abstract
Systems equipped with counters are central when modeling distributed
protocols, programs with recursive parallel threads, programs with pointers, broadcast
protocols, databases, etc. When it comes to modelchecking counter systems and their variants,
the main results are that verification is undecidable when zerotests are allowed, while several
problems can be decided when zerotests are forbidden — one speaks of VASS, for "vector
addition systems with states", or equivalently "Petri nets". In the case of Petri nets,
reachability was shown decidable in 1982, and the reachability problem for Petri nets and
related decidable problems on subclasses of counter systems are pivot problems not only for the
verification of infinitestate systems but also for problems appearing in very active research
areas related to various logics and automata for data words/trees. Hence, the design of
efficient algorithms for the reachability problem for VASS may have a great impact, not only in
the realm of formal verification. It is however a very difficult problem. Therefore, improving
the computational cost for solving the reachability problem for Petri nets would also improve
the complexity of the formal verification of numerous classes of infinitestate systems.
Strikingly, the decision algorithm for Petri net reachability has never been implemented. This is
because of its high complexity, both conceptual (the algorithm is very hard to understand and to
describe) and computational (it is assumed that the complexity of the algorithm is not
primitiverecursive). The general problem is known to be decidable by algorithms exclusively
based on the classical KosarajuLambertMayrSacerdoteTenney decomposition (KLMTS
decomposition). Recently, from this decomposition, it was proved that a final configuration is
not reachable from an initial one if, and only if, there exists a Presburger inductive invariant
that contains the initial configuration but not the final one. Since we can decide if a
Presburger formula denotes an inductive invariant, we deduce from this result that there exist
checkable certificates of nonreachability in the Presburger arithmetic. In particular, there
exists a simple algorithm for deciding the general Petri net reachability problem based on two
semialgorithms. A first one that tries to prove reachability by enumerating finite sequences of
actions and a second one that tries to prove nonreachability by enumerating Presburger
formulas.
In this presentation, we provide a simple proof of the Petri net reachability problem that is not
based on the KLMST decomposition. The proof is based on the notion of production relations,
inspired from Hauschildt, that directly proves the existence of Presburger inductive invariants.
13:0014:30Lunch
14:3018:00Tutorial
14:3018:00Martin
Grohe Tutorial: Logic for algorithms
SLIDES speaker: Martin Grohe
Abstract
The theme of this tutorial is (recent) applications of logic in the
design and analysis of efficient algorithms. I will cover the following three topics.

Logical techniques in the analysis of generic algorithms
Certain generic (families of) algorithms, such as the WeisfeilerLehman algorithm for
graph isomorphism testing and kconsistency tests for constraint satisfaction problems
have logical characterisations. Thus logical techniques can be used to analyse the power
of these algorithms and also to prove lower bounds for their running time.

Algorithmic meta theorems
Algorithmic meta theorems attempt to explain and unify algorithmic results by proving
tractability not only for individual problems, but for whole classes of problems. These
classes are typically defined in terms of logic. The prototypical example of an
algorithmic meta theorem is Courcelle's Theorem, stating that all properties of graphs
of bounded treewidth that are definable in monadic secondorder logic are decidable in
linear time.
In the tutorial, I will focus on meta theorems for firstorder logic, where by now we
have a fairly complete picture of graph classes admitting a nontrivial meta theorem
 Applications of meta theorems in algorithmic graph structure theory
In this last part I will discuss applications of algorithmic meta theorems to problems in
algorithmic graph structure theory. By this I mean graph algorithms that use meta
theorems to solve tasks for which no other (direct combinatorial) algorithm is known.
It is worth noting that the algorithmic problems considered in all three parts are not derived
from logic, such as satisfiability or modelchecking problems, but "standard" algorithmic
problems, often with a strong combinatorial and graph theoretical flavour. On the way, I will
introduce the necessary graph theory, including nowhere dense graphs and certain aspects of
graph minor theory.
Thursday 19 September
09:0009:50Invited talk
09:0009:50Patrice
Godefroid Invited talk: 500 Machineyears of software model checking and
SMT solving
SLIDES speaker: Patrice Godefroid
Abstract
I will report on our experience running SAGE for over 500machine
years in Microsoft's security testing labs. SAGE is a whitebox fuzzing
tool for security testing. It performs symbolic execution dynamically
at the binary (x86) level, generates constraints on program inputs,
and solves those constraints with an SMT solver in order to generate
new inputs to exercize previously uncovered program paths or trigger
security vulnerabilities (like buffer overflows). This process is
repeated using novel statespace exploration techniques that attempt
to sweep through all (in practice, many) feasible execution paths of
the program while checking simultaneously many properties. This
approach thus combines program analysis, testing, model checking and
automated theorem proving (constraint solving).
Since 2009, SAGE has been running 24/7 on average 100+ machines
automatically ``fuzzing'' hundreds of applications. This is the
largest computational usage ever for any SMT solver, with over 4
billion constraints processed to date. In the process, SAGE found many
new security vulnerabilities (missed by blackbox fuzzing and static
program analysis) and was credited to have found roughly one third of
all the bugs discovered by file fuzzing during the development of
Microsoft's Windows 7, saving millions of dollars by avoiding
expensive security patches to nearly a billion PCs.
In this talk, I will present the SAGE project, highlight connections
with program verification, and discuss open research challenges.
This is joint work with Michael Levin, David Molnar, Ella Bounimova,
and other contributors.
09:5010:00Break
10:0011:12Session 1
10:0010:12Amélie
Gheerbrant, Leonid Libkin and Cristina Sirangelo Incomplete information,
monotonicity, and homomorphism preservation
SLIDES speaker: Cristina Sirangelo
Abstract
Incomplete information is ubiquitous in database applications, and yet
our understanding of it is still rather basic.
Since an incomplete database can represent multiple databases, query answering boils down to solving
an entailment problem, while database systems are good at performing modelchecking algorithms on
firstorder structures. Thus, to take advantage of them, we need to understand when entailment can
be reduced to modelchecking. We show that this happens for queries which are monotone with respect
to the semantics of incompleteness, and that such monotonicity can be described via homomorphism
preservation, for different notions of homomorphisms. Combining the latter with preservation
theorems from logic (existing as well as new), we obtain classes of queries for which standard
database systems can correctly compute answers over incomplete databases, or, logically speaking,
for which entailment can be solved by simple modelchecking.
10:1210:24Domagoj
Vrgoč Querying graphs with data
SLIDES speaker: Domagoj Vrgoc
Abstract
With the recent resurgence of graph data model several languages for
querying such data have been proposed. Traditionally these languages concentrated on querying
topological properties while largely ignoring the actual data stored in the graph. In this
presentation we will highlight how adding features that enable querying both data and
topology affects the languages used to extract information from graph databases.
10:2410:36Pablo
Barcelo, Gaëlle Fontaine, Miguel Romero and Moshe Y. Vardi Semantic
acyclicity on graph databases
SLIDES speaker: Gaelle Fontaine
Abstract
Unions of acyclic conjunctive queries (CQs) can be evaluated in linear
time, as opposed to arbitrary CQs, for which the evaluation problem is NPcomplete. It is known that
evaluation of semantically acyclic unions of CQs  i.e., unions of CQs that are equivalent to a
union of acyclic ones  is tractable.
We study the notion of semantic acyclicity in the context of graph databases and unions of
conjunctive regular path queries (UCRPQs). We prove that checking whether a UCRPQ is semantically
acyclic is decidable in 2ExpSpace and is ExpSpacehard. We show that evaluation of semantically
acyclic UCRPQs is fixedparameter tractable.
10:3610:48Michael
Vanden Boom Constructive interpolation for guarded logics
SLIDES speaker: Michael Vanden Boom
Abstract
The guarded fragment of firstorder logic (GFO) shares many useful
properties with modal logic, but fails to have Craig interpolation. Recently, an extension called
the guarded negation fragment (GNFO) was shown to have interpolation, but the proof was
nonconstructive. The goal in this research (suggested by Benedikt, ten Cate, and Lutz) is to
develop constructive methods for interpolation, in order to see whether interpolation can be
performed in practice and to better understand the complexity of the problem. I describe some
preliminary work on constructive interpolation for GNFO.
10:4811:00Eryk
Kopczyński and Tony Tan Regular graphs and the spectra of twovariable
logic with counting
SLIDES speaker: Eryk Kopczyński
Abstract
For a formula $\phi$ over a signature including predicates $P_1...P_k$,
we define the image of $\phi$ as the set of tuples $(n_1...n_k)$ such that
there is a model of $\phi$ where exactly $n_i$ elements satisfy $P_i$. For example,
if each author has written exactly 2 papers, and each paper has exactly 3 authors, then
2*total number of authors=3*total number of authors. This can be seen as a
generalization of the well known notion of a spectrum. Our main result is that,
for formulae of FO2C, spectra and images are definable in
Presburger arithmetic, and thus semilinear (and closed under complement).
11:0011:12Łukasz
Kaiser and Charles Jordan Machine learning using descriptive complexity
and SATsolvers
SLIDES speaker: Lukasz Kaiser
Abstract
In machine learning there is an inherent tradeoff between the
efficiency of
the learning algorithm and the expressiveness of the hypothesis that one is
allowed to learn. Even though this tradeoff is present in almost every machine
learning task, it is hard to capture formally and still often resolved based
on instinct and experience. We propose using parametrized logical formulas
to represent hypotheses and then exploit propositional solvers for efficient
learning and results from descriptive complexity to get expressiveness
guarantees. This allows a more systematic study of the above tradeoff and,
as we show on a few examples, it is applicable to practical learning tasks.
11:1211:36Coffee break
11:3613:00Session 2
11:3611:48Florian
Bruse, Oliver Friedmann and Martin Lange Polynomial guarded
transformation for the modal mucalculus is still open
SLIDES speaker: Florian Bruse
Abstract
Guarded normal form requires occurrences of fixpoint variables in a
μcalculus formula to occur under the scope of a modal operator. The literature contains guarded
transformations that effectively bring a μcalculus formula into guarded normal form. We
show that the known guarded transformations can cause an exponential blowup in formula
size, contrary to existing claims of polynomial behaviour. We also show that any poly
nomial guarded transformation for μcalculus formulas in the more relaxed vectorial form
gives rise to a polynomial solution algorithm for parity games, the existence of which is an
open problem.
11:4812:00Paul
Hunter The expressive completeness of Metric Temporal Logic
SLIDES speaker: Paul Hunter
Abstract
LTL has emerged as the primary logic for specifying temporal
properties. This is largely due to the low complexity of its associated model checking problem and
its high expressibility  with the celebrated result of Kamp showing that LTL has the same
expressive power as firstorder logic. In the quantitative setting, Metric Temporal Logic is quickly
becoming the standard to which all other temporal logics are compared. It turns out that the
expressive power of MTL is dependent on the set of constants available, and I will give a precise
characterization of when MTL has the same expressive power as firstorder logic.
12:0012:12Frederik
Harwath and Nicole Schweikardt On the locality of arbinvariant
firstorder logic with modulo counting quantifiers
SLIDES speaker: Frederik Harwath
Abstract
We study Gaifman and Hanf locality of an extension of firstorder logic
with modulo p counting quantifiers
(FO+MODp, for short) with arbitrary numerical predicates. We require that the validity of formulas
is
independent of the particular interpretation of the numerical predicates and refer to such formulas
as
arbinvariant formulas. We give a detailed picture of locality and nonlocality properties of arb
invariant FO+MODp.
12:1212:24Wojciech
Czerwiński, Wim Martens and Tomas Masopust Efficient separability of
regular languages by subsequences and suffixes
SLIDES speaker: Wojciech Czerwiński
Abstract
When can two regular word languages K and L be separated by a simple
language? We investigate this question and consider separation by piecewise and suffixtestable
languages and variants thereof.
We give characterizations of when two languages can be separated and present an overview of when
these problems can be decided in polynomial time if K and L are given by nondeterministic automata.
12:2412:36Thomas
Place, Lorijn van Rooijen and Marc Zeitoun Separating regular languages
by piecewise testable and unambiguous languages
SLIDES speaker: Lorijn van Rooijen
Abstract
We discuss the separation problem for regular
languages. We give a Ptime algorithm to check whether two
given regular languages are separable by a piecewise testable
language, that is, whether a $\mathcal{B}\Sigma_1(<)$ sentence can
witness that the languages are disjoint. If this
is possible, we express a separator by saturating one of the
original languages by a suitable congruence. Following the same line,
we show that one can also decide whether two regular languages can
be separated by an unambiguous (i.e. $FO^2(<)$definable) language, albeit with a higher
complexity.
12:3612:48Richard
Mayr and Lorenzo Clemente Advanced automata minimization
SLIDES speaker: Richard Mayr
Abstract
12:4813:00Nathanaël
Fijalkow, Krishnendu Chatterjee, Thomas Colcombet, Florian Horn, Denis Kuperberg,Michał Skrzypczak
and Martin Zimmermann Boundedness games
SLIDES speaker: Nathanael Fijalkow
Abstract
In this talk, I will discuss some recent developments about boundedness
games. They are twoplayer games played over graphs, featuring counters. The first player's
objective is to satisfy a parity condition and that the counter values are bounded.
A lot of questions are open: what is the algorithmic complexity of deciding the winner, and does
there always exist finitememory winning strategies?
In particular, as shown by Thomas Colcombet, proving the existence of finitememory winning
strategies for (some) boundedness games is the last missing item to prove the decidability of
costMSO over infinite trees.
I will give an overview of where we stand now and what are the next challenges.
13:0014:30Lunch
14:3615:24Session 3
14:3614:48Olivier
Carton and Luc Dartois Aperiodic twoway transducers
SLIDES speaker: Dartois Luc
Abstract
A twoway transducer is a finite state sequential machine with a
twoway input tape and a oneway output tape. At each step of the computation, it reads the current
symbol, outputs a possibly empty word, then changes its internal state and moves its input head,
according to the transition taken with current state and the letter read.
It computes a partial function from words over an alphabet to another set of words.
Similarly, a MSOdefinable function over words is defined as interpretations of linear graphs
through logic.
A result by Engelfriet and Hoogeboom proved the equivalence of the two models.
I will recall the definition of both models, and state an extension of this result to the natural
subclass of aperiodic twoway transducers.
14:4815:00Laure
Daviaud and Thomas Colcombet Approximate comparison of distance
automata
SLIDES speaker: Laure Daviaud
Abstract
Distance automata are automata weighted over the semiring (N U
{+infinity},min,+) that compute functions from words to N U {+infinity}.
It is known that testing f0 and two functions f,g computed by distance automata, answers "yes"
if f(1+e)g(w), and may answer "yes" or "no" in all other
cases.
This is a joint work with Thomas Colcombet.
15:0015:12Rajeev Alur
and Mukund Raghothaman Decision problems for additive regular
functions
SLIDES speaker: Mukund Raghothaman
Abstract
We introduce cost register automata (CRA)  this is a deterministic
model to associate costs with strings that is parametrized by operations of interest (such as
addition, scaling, and minimum), and a notion of regularity that provides a yardstick to measure
expressiveness. Our notion of regularity relies on the notion of stringtotree transducers, and
allows associating costs with events that are conditioned on regular properties of future events.
CRAs compute regular functions using multiple writeonly registers whose values can be combined
using the allowed set of operations. We then discuss various analysis problems associated with CRAs
and regular functions, including the decidability of equivalance and containment, register and state
minimization, and Angluinstyle learning of cost functions.
15:1215:24Sylvain
Lombardy and Jacques Sakarovitch The validity of weighted automata
SLIDES speaker: Jacques Sakarovitch
Abstract
This work addresses, and proposes a solution to, the problem of the
validity of weighted automata in which epsilontransitions may result in
infinite summations.
With a topological approach, a definition of validity is taken that insures
that any closure algorithm will succeed on every valid weighted automaton.
This definition is stable with respect to natural transformations of
automata.
Validity is shown to be decidable when weights are taken in Q or R. The
corresponding algorithm is implemented in the VAUCANSON platform. The
problem remains open in general.
15:2415:36Break
15:3616:48Session 4
15:3615:48Stanislav
Böhm, Stefan Göller and Petr Jančar Equivalence of deterministic
onecounter automata is NLcomplete
SLIDES speaker: Stefan Göller
Abstract
We prove that language equivalence of deterministic one counter
automata is NLcomplete. This improves the super polynomial time complexity upper bound shown by
Valiant and Paterson in 1975. Our main contribution is to prove that two deterministic onecounter
automata are inequivalent if and only if they can be distinguished by a word of length polynomial in
the size of the two input automata.
15:4816:00Stéphane
Demri, Diego Figueira and M. Praveen Reasoning about data repetitions
with counter systems
SLIDES speaker: Diego Figueira
Abstract
We study lineartime temporal logics interpreted over data words with
multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive
positions and to repetitions of attribute values in the future or past. We demonstrate
correspondences between satisfiability problems for logics and reachabilitylike decision problems
for counter systems. We show that allowing/disallowing atomic formulas expressing repetitions of
values in the past corresponds to the reachability/coverability problem in Petri nets. This gives us
2EXPSPACE upper bounds for several satisfiability problems. We prove matching lower bounds by
reduction from a reachability problem for a newly introduced class of counter systems. This new
class is a succinct version of vector addition systems with states in which counters are accessed
via pointers, a poten tially useful feature in other contexts. We strengthen further the
correspondences between data logics and counter systems by characterizing the complexity of
fragments, extensions and variants of the logic. For instance, we precisely characterize the
relationship between the number of attributes allowed in the logic and the number of counters needed
in the counter system.
16:0016:12Michael
Benedikt, Stefan Göller, Stefan Kiefer and Andrzej Murawski Bisimilarity
of pushdown automata is nonelementary
SLIDES speaker: Stefan Göller
Abstract
Given two pushdown systems, the bisimilarity problem asks whether they
are bisimilar.
While this problem is known to be decidable our main result states that it is nonelementary,
improving EXPTIMEhardness, which was the previously best known lower bound for this problem.
Our lower bound result holds for normed pushdown systems as well.
16:1216:24Ranko
Lazic, Joel Ouaknine and James Worrell Zeno, Hercules and the Hydra:
Downward rational termination is Ackermannian
SLIDES speaker: Ranko Lazic
Abstract
Metric temporal logic (MTL) is one of the most prominent specification
formalisms for realtime systems. Over infinite timed words, full MTL
is undecidable, but satisfiability for its safety fragment was proved
decidable several years ago. The problem is also known to be
equivalent to a fair termination problem for a class of channel
machines with insertion errors. However, the complexity has remained
elusive, except for a nonelementary lower bound. Via another
equivalent problem, namely termination for a class of rational
relations, we show that satisfiability for safety MTL is not primitive
recursive, yet is Ackermannian, i.e., among the simplest nonprimitive
recursive problems. This is surprising since decidability was
originally established using Higman's Lemma, suggesting a much higher
nonmultiply recursive complexity.
16:2416:36Aleksy
Schubert, Daria WalukiewiczChrząszcz and Paweł Urzyczyn Positive logic
is not elementary
SLIDES speaker: Daria WalukiewiczChrząszcz
Abstract
We prove that the positive fragment of minimal firstorder
intuitionistic logic is not of elementary complexity. The proof
uses an automatatheoretic approach taking advantage of
the computational power of alternation.
16:3616:48Sylvain
Schmitz Complexity hierarchies beyond elementary
SLIDES speaker: Sylvain Schmitz
Abstract
Decision problems with a nonelementary complexity occur naturally in
logic, combinatorics, formal language, verification, etc., with
complexities ranging from simple towers of exponentials to
Ackermannian and beyond. Somewhat surprisingly, we lack the
definitions of classes and reductions that would allow to state
completeness results at such high complexities. We introduce a
hierarchy of fastgrowing complexity classes and discuss its
suitability for completeness statements of nonelementary problems.
16:4817:12Coffee Break
17:1218:24Session 5
17:1217:24Thomas
Brihaye and Quentin Menet Simple strategies for BanachMazur games and
fairly correct systems
SLIDES speaker: Thomas Brihaye
Abstract
In 2006, Varacca and Voelzer proved that on finite graphs,
omegaregular large sets coincide with omegaregular sets of
probability 1, by using the existence of positional strategies in the
related BanachMazur games. Motivated by this result, we try to
understand relations between sets of probability~1 and various notions
of simple strategy (including those introduced in a recent paper of
Graedel and Lessenich). Then, we introduce a generalisation of the
classical BanachMazur game and in particular, a probabilistic version
whose goal is to characterise sets of probability~1 (as classical
BanachMazur games characterise large sets). We obtain a determinacy
result for these games, when the winning set is a countable
intersection of open sets.
17:2417:36Thomas
Brihaye, Gilles Geeraerts, S. Krishna, Lakshmi Manasa and Ashutosh Trivedi On the decidability of priced timed games
SLIDES speaker: Thomas Brihaye
Abstract
Twoplayer zerosum games on finite automata are a classical metaphor
for controller synthesis. An extension of this model to timecritical
systems are twoplayer games on priced timed automata. For those
games, the optimal reachability synthesis problem asks to compute a
strategy (for one of the players) that guarantees to reach a given
target with a total cost satisfying some optimality constraint. While,
some versions of this problem have already been showed undecidable, we
propose to complete the global picture by studying other variants
(such as the timedbounded version).
17:3617:48Krishnendu
Chatterjee Survey of recent results for stochastic games
SLIDES speaker: Krishnendu Chatterjee
Abstract
Stochastic games provide a powerful framework to model fundamental
problems in the design and analysis of stochastic reactive
systems. While this connection is well understood, and several results
have enriched the framework, there is a wealth of research questions
that are open, including some longstanding ones (such as the
complexity of perfectinformation stochastic reachability games). In
this talk, I will survey some recent results for general model of
stochastic games and related models. The talk is based on several
papers, and presents an overview of recent results based on joint
works with several coauthors, as well as results from other
researchers.
17:4818:00Mahsa
Shirmohammadi, Laurent Doyen and Thierry Massart Synchronization in
Markov decision processes
SLIDES speaker: Mahsa Shirmohammadi
Abstract
Markov Decision Processes (MDPs) are 11/2 player stochastic games.
The player tries to maximize the probability to satisfy an objective.
Traditionally, the objective of the player is expressed
as a set of desired sequences of states
visited during the game.
Recently, MDPs are viewed as generators of probability distributions
over states, and objectives are defined as sets of sequences of probability distributions.
We study synchronizing objectives that require that some state tend to
accumulate all the probability mass.
We consider three winning modes: sure, almostsure and limitsure.
18:0018:12Tomáš
Brázdil, Holger Hermanns, Jan Krčál, Jan Kretinsky and Vojtĕch Řehák Verification of open interactive Markov chains
SLIDES speaker: Jan Kretinsky
Abstract
We provide the first assumeguarantee reasoning for stochastic
continuoustime systems. Interactive Markov chains (IMC) are compositional behavioural models
similar to continuoustime Markov decision processes. Given a timebounded property and an IMC
component, we synthesize its scheduler optimizing the probability that the property is satisfied
when the IMC is working in an unknown environment. We also give a specification formalism for IMC
and consider unknown environments satisfying a given specification.
18:1218:24Tomáš
Brázdil, Antonin Kučera, Vojtĕch Forejt and Krishnendu Chatterjee Trading
performance for stability in Markov decision processes
SLIDES speaker: Tomas Brazdil
Abstract
We study the central controller synthesis problems for finitestate
Markov decision processes, where the objective is to optimize both the expected meanpayoff
performance of the system and its stability. We argue that the basic theoretical notion of
expressing the stability in terms of the variance of the meanpayoff (called global variance in our
paper) is not always sufficient, since it ignores possible instabilities on respective runs. For
this reason we propose alernative definitions of stability, which we call local and hybrid variance,
and which express how rewards on each run deviate from the run's own meanpayoff and from the
expected meanpayoff, respectively. We show that a strategy ensuring both the expected meanpayoff
and the variance below given bounds requires randomization and memory, under all the above semantics
of variance. We then look at complexity of the problem of determining whether there is a such a
strategy.
Friday 20 September
09:0009:50Invited Talk
09:0009:50Erich
Grädel Invited talk: Linear Algebra and the quest for a logic for
PTIME
SLIDES speaker: Erich Grädel
Abstract
The quest for a logic for PTIME is one of the central open problems in
both
finite model theory and database theory. It asks whether there is a logic in which a property of
finite structures is definable if, and only if,
it is decidable in polynomial time.
Much of the research in this area has focused on the logic FPC, the extension
of least or inflationary fixedpoint logic by counting terms. In fact, FPC has been shown to capture
PTIME on many natural classes of structures. On the other side, already in 1992, a graph query has
been
constructed that can be decided in PTIME but is not definable in FPC. But while this CFI query, as
it is now called, is very elegant and has led to new insights in many different areas, it can hardly
be called a natural problem in polynomial time. Therefore it was often remarked that possibly all
natural polynomialtime properties of finite structures could be expressed in
FPC. However, this hope was eventually refuted in a strong sense by Atserias,
Bulatov and Dawar who proved that the important problem of solvability of
linear equation systems (over any finite Abelian group) is not definable in FPC and that, indeed,
the CFI query reduces to this problem.
This motivates the study of the relationship between finite model theory and linear algebra, and
suggests that operators from linear
algebra, such as matrix ranks or solvability operators, could be a source of new extensions to
fixedpoint logic, in an attempt to find a logical characterisation of PTIME.
We will discuss such approaches and study the relations between different polynomialtime computable
problems over (finite) rings, fields and Abelian groups in the context of logical manytoone and
Turing reductions,
i.e., interpretations and generalised quantiers.
In this context, we will also discuss an alternative approach towards
a logic for PTIME, proposed by Blass, Gurevich and Shelah, based on choiceless computations
operating directly on structures.
09:5010:00Break
10:0011:12Session 6
10:0010:12Matthew
Anderson and Anuj Dawar On symmetric circuits and FPC
SLIDES speaker: Anuj Dawar
Abstract
We study queries on graphs (and other relational structures) defined
by families of Boolean circuits that are invariant under permutations of
the vertices. In particular, we study circuits that are symmetric,
that is, circuits whose invariance is explicitly witnessed by
automorphisms of the circuit induced by the permutation of their
inputs. We show a close connection between queries defined on
structures by uniform families of symmetric circuits and definability
in fixedpoint logics.
10:1211:24Steven
Lindell and Scott Weinstein Presentationinvariant definability
SLIDES speaker: Steven Lindell
Abstract
We extend the notion of invariant elementary definability to a variety
of different graph representations, including those that strictly extend the power of firstorder
logic with an arbitrary linear order.
11:2410:36Robert
Ganian, Petr Hliněný, Daniel Kral, Jan Obdržálek, Jarett Schwartz and Jakub Teska FO model checking of interval graphs
SLIDES speaker: Jan Obdržálek
Abstract
We study the computational complexity of the model checking problem for
the
first order (FO) logic on interval graphs, i.e., interscetion graphs of
intervals on the real line. As the main result we show that for nvertex
interval graphs this problem can be solved in time O(n log n) if we take
intervals with lengths from a fixed finite set. On the other hand, we show
that this is no longer true once the interval lengths taken from any set
that is dense in some open subset.
10:3611:48Oleg
Verbitsky Bounds for the quantifier depth in twovariable logics
SLIDES speaker: Oleg Verbitsky
Abstract
Given structures $G$ and $H$ and a firstorder formula $F$
over the same vocabulary, we say that $F$ distinguishes $G$ from $H$
if $F$ is true on $G$ but false on $H$.
By alternation depth of $F$ we mean
the maximum length of a sequence of nested alternating quantifiers in $F$.
Obviously, this parameter is bounded from above by the quantifier depth of $F$.
We will examine the maximum alternation depth and quantifier depth needed
to distinguish two structures in twovariable firstorder logic and its fragments.
Lower bounds for the quantifier depth in the existentialpositive fragment
have applications to analysis of the computational complexity of Arc Consistency testing,
one of the most popular heuristics for the constraint satisfaction problem.
10:4811:00Lucas
Heimberg, Dietrich Kuske and Nicole Schweikardt An optimal Gaifman normal
form construction for structures of bounded degree
SLIDES speaker: Lucas Heimberg
Abstract
This paper's main result presents a $3$fold exponential algorithm that
transforms a firstorder formula $\varphi$ together with a number $d$ into a formula in Gaifman
normal form that is equivalent to $\varphi$ on the class of structures of degree at most~$d$. For
structures of polynomial growth, we even get a $2$fold exponential algorithm.
These results are complemented by matching lower bounds: We show that for structures of degree $2$,
a $2$fold exponential blowup in the size of formulas cannot be avoided. And for structures of
degree $3$, a $3$fold exponential blowup is unavoidable.
As a result of independent interest we obtain a $1$fold exponential algorithm which transforms a
given firstorder sentence~$\varphi$ of a very restricted shape into a sentence in Gaifman normal
form that is equivalent to $\varphi$ on all structures.
11:0011:12Nathanaël
Fijalkow and Charles Paperman On properties of logical sentences with
arbitrary monadic predicates
SLIDES speaker: Charles Paperman
Abstract
In this talk, we introduce two properties for logical sentences using
arbitrary numerical predicates: the Straubing property and the Crane Beach property.
Both properties state that formulae defining simple languages do not need to use arbitrary
complicated predicates, where simple either means regular or with a neutral letter.
We restrict our attention to monadic predicates, and show that both properties hold in a strong
syntactical sense.
11:1211:36Coffee break
11:3613:00Session 7
11:3611:48Mikołaj
Bojańczyk, Bartek Klin, Sławomir Lasota and Szymon Toruńczyk Turing
machines with atoms
SLIDES speaker: Bartek Klin
Abstract
We study Turing machines over sets with atoms, also known as nominal
sets.
Our main result is that deterministic machines are weaker than nondeterministic ones; in particular,
P!=NP in sets with atoms. Our main construction is closely related to the CaiFuererImmerman graphs
used in descriptive complexity theory.
11:4812:00Alexander
Kurz, Tomoyuki Suzuki and Emilio Tuosto On regular expressions and
nominal automata
SLIDES speaker: Tomoyuki Suzuki
Abstract
In several branches of computer sciences, automata are often used to
describe computational behaviours. Among those developments, automata
equipped with resource devices, e.g. a finitememory or local
registers, and languages over infinite alphabets are collecting more
and more attentions. In this talk, we would like to discuss a possible
general theory for those resourcehandling automata from the point of
nominal regular expressions. As already published works, we shall
present the layweredtechnique and the Kleenestyle theorem. On top,
as our ongoing work, by comparing possible actions (labels) on
transitions, we will provide how those actions differentiate their
languagerecognisability and show the automatahierarchy of languages
over infinite alphabets.
12:0012:12Szymon
Toruńczyk, Mikołaj Bojańczyk and Luc Segoufin Verification of database
driven systems via amalgamation
SLIDES speaker: Szymon Torunczyk
Abstract
We describe a general framework for static verification of systems
that base their decisions upon queries to databases. The database is
specified using constraints, typically a schema, and is not modified
during a run of the system. The system is equipped with a finite
number of registers for storing intermediate information from the
database and the specification consists of a transition table described
using quantifierfree formulas that can query either the database or the registers.
Our main result concerns systems querying XML databases  modeled as
data trees  using quantifierfree formulas with predicates such as
the descendant axis or comparison of data values.
Our technique is based on the notion of amalgamation and is quite
general. For instance it also applies to relational databases (with
an optimal \pspace algorithm).
12:1212:24Thomas
Colcombet and Amaldev Manuel μcalculus on data words
SLIDES speaker: Amaldev Manuel
Abstract
We introduce and explore various fragments of μcalculus on data words.
We show that full μcalculus is undecidable,
but its νfragment is decidable by reduction to data automata. We disclose two subclasses of the
νfragment
that enjoy the further property of being closed under negation, namely the class of Bounded Reversal
(BR)
and the class of Bounded Mode Alternation (BMA). The latter is contained in the former class and
is already sufficiently expressive for capturing several logics studied in the literature like
$\fotwo$
and DataLTL. We then characterize these two fragments as cascades of suitably defined transducer
models.
We finally prove the separation of BMA from BR using a novel paradigm of circuits and prove
hierarchy theorems
for BMA, DataLTL and $\fotwo$.
12:2412:36Mikołaj
Bojańczyk and Sławomir Lasota A machineindependent characterization of
timed languages
SLIDES speaker: Slawomir Lasota
Abstract
We use a variant of sets with atoms (known also as nominal sets) as a
framework suitable
for stating and proving the following two results on timed automata. The first result
is a machineindependent characterization of languages of deterministic timed automata,
a la MyhillNerode Theorem. As our second result we define a class of automata
that slightly extends timed automata and is effectively closed under minimization.
12:3612:48Daniel
Bundala and Joël Ouaknine On the complexity of path checking in temporal
logics
SLIDES speaker: Daniel Bundala
Abstract
Given a formula in a temporal logic such as LTL or MTL, a fundamental
problem is the complexity of evaluating the formula on a given word. For LTL, the complexity of this
task was recently shown to be in NC hierarchy. In this paper, we establish a connection between LTL
path checking and planar circuits. We use the connection to show that the pathchecking problem for
LTL extended with exclusive or is already Phard. We then present an NC algorithm for MTL, a
quantitative (or metric) extension of LTL and give an AC1 algorithm for UTL, the unary fragment of
LTL.
12:4813:00Diego
Figueira On XPath with transitive axes and data tests
SLIDES speaker: Diego Figueira
Abstract
We study the satisfiability problem for XPath with data equality tests.
XPath is a node selecting language for XML documents whose satisfiability problem is known to be
undecidable, even for very simple fragments. However, we show that the satisfiability for XPath with
the rightward, leftward and downward reflexivetransitive axes (namely following siblingorself,
precedingsiblingorself, descendantorself) is decidable. Our algorithm yields a complexity of
3ExpSpace, and we also identify an expressiveequivalent normal form for the logic for which the
satisfiability problem is in 2ExpSpace. These results are in contrast with the undecidability of the
satisfiability problem as soon as we replace the reflexivetransitive axes with just transitive
(nonreflexive) ones.
13:0014:30Lunch
14:3015:20Invited Talk
14:3015:20Marco
Scarsini Invited talk: Existence of equilibria in countable games
SLIDES speaker: Marco Scarsini
Abstract
Although mixed extensions of finite games always admit equilibria,
this
is not the case for countable games, the bestknown example being Wald's
pickthelargerinteger game. Several authors have provided conditions for the
existence of equilibria in infinite games. These conditions are
typically of topological nature and are not applicable to countable
games. Here we establish
an existence result for the equilibrium of countable games when the strategy
sets are a countable group and the payoffs are functions of the group operation.
In order to obtain the existence of equilibria, finitely additive mixed
strategies
have to be allowed. This creates a problem of selection of a product measure of
mixed strategies. We propose a family of such selections and prove existence of
an equilibrium that does not depend on the selection. As a byproduct we show
that if finitely additive mixed strategies are allowed, then Wald's game admits
an equilibrium.
15:2015:30Break
15:3616:48Session 8
15:3615:48Stéphane Le
Roux Infinite sequential Nash equilibrium
SLIDES speaker: Le Roux Stephane
Abstract
Borel determinacy says that all infinitetree winlose twoplayer games
have a Nash equilibrium provided that the winning sets of the players are Borel. This talk
generalises it and shows that all infinitetree multioutcome multiplayer games have a Nash
equilibrium provided that the outcome function is "Borel measurable" and that the player preferences
have no infinite ascending chains.
open access to the article at
http://lmcsonline.org/ojs/viewarticle.php?id=985&layout;=abstract&iid;=39
15:4816:00Valentin
Goranko, Wojtek Jamroga and Paolo Turrini Strategic games and truly
playable effectivity functions
SLIDES speaker: Wojtek Jamroga
Abstract
A wellknown result states that every strategic game generates a
playable effectivity function, and every playable effectivity function can be implemented with a
strategic game. We show that the latter does not hold for infinite games. We identify the error in
the proof, and present examples of playable effectivity functions for which no equivalent strategic
game exists. Then, we characterize the class of *truly playable* functions that do correspond to
strategic games. We also show that Coalition Logic cannot distinguish between the two classes, and
we extend it to a logic that is expressive enough.
16:0016:12Laurent
Doyen and Marco Faella Besteffort control for Markov decision
processes
SLIDES speaker: Marco Faella
Abstract
The premise of this talk is that in order to obtain realistic decision
plans for Markov Decision Processes (or other decisiontheoretic models) it is useful to consider
solution concepts that are as discriminating as possible, by exploiting as much as possible the
information provided in the model.
Hence, we propose novel solution concepts for MDPs, obtained by lexicographically composing
different risk attitudes, ranging from absolutely riskaverse, or pessimistic, to riskseeking, or
optimistic, in an order that depends on the application domain.
16:1216:24Krishnendu
Chatterjee, Laurent Doyen, Mickael Randour and JeanFrançois Raskin Looking at meanpayoff and totalpayoff through windows
SLIDES speaker: Mickael Randour
Abstract
We consider twoplayer games with meanpayoff (MP) and totalpayoff
(TP) objectives. In single dimension, their complexities coincide. In multi dimensions, MP games are
coNPcomplete. We show that TP games are undecidable. We introduce conservative approximations,
considering the payoff over a local finite window sliding along a play. For single dimension, we
show that (i) if the window is polynomial, deciding the winner is in P, and (ii) the existence of a
bounded window can be decided in NP $\cap$ coNP, and is at least as hard as solving MP games. For
multi dimensions, we show that (i) the fixed window size problem is EXPcomplete, and (ii) there is
no primitiverecursive algorithm to decide the existence of a bounded window.
16:2416:36Martin Lang
and Christof Löding Resource reachability games on pushdown graphs
SLIDES speaker: Martin Lang
Abstract
We consider twoplayer games on the configuration graph of pushdown
systems with an additional finite set of nonnegative integer counters. These counters can be
incremented, reset to zero or left unchanged by the transition rules of the pushdown system. We
associate the cost of a play with the highest counter value that occurs and look at a combined
reachability and costlimit winning condition. Is there a uniform costbound k such that one can win
from a set of configurations A with this bound? We provide a solution to this question by an
extension of the wellknown saturation principle.
16:3616:48Marcus
Gelderie Strategy composition in compositional games
SLIDES speaker: Marcus Gelderie
Abstract
When studying games played on finite arenas, the arena is given
explicitly, hiding the underlying structure of the arena. We study games
where the global arena is a product of several smaller, constituent
arenas. We investigate how these "global games" can be solved by
playing "component games" on the constituent arenas. To this end, we
introduce two kinds of products of arenas. Moreover, we define a
suitable notion of strategy composition and show how, for the first
notion of product, winning strategies in reachability games can be
composed from winning strategies in games on the constituent arenas. For
the second kind of product, the complexity of solving the global game
shows that a general composition theorem is equivalent to proving Pspace
= Exptime.
16:4817:12Coffee Break
17:1218:36Session 9
17:1217:24Matteo
Mio Game semantics for probabilistic mucalculi
SLIDES speaker: Matteo Mio
Abstract
I will introduce a novel class of twoplayer games, called "TwoPlayer
Stochastic metaParity Games", which are used in my PhD Thesis to give Game Semantics to expressive
probabilisticvariants of the Modal muCalculus. This new class of games is proven to be
"determined". I will discuss some of the technical aspects of the proof.
17:2417:36Olivier
Finkel The determinacy of infinite games specified by automata
SLIDES speaker: Olivier Finkel
Abstract
We prove that the determinacy of GaleStewart games whose winning sets
are accepted by realtime 1counter BŁchi automata is equivalent
to the determinacy of (effective) analytic GaleStewart games which is known to be a large cardinal
assumption.
Using some results of set theory we prove that one can effectively construct a 1counter BŁchi
automaton A such that:
(1) There exists a model of ZFC in which Player 1 has a winning strategy in the GaleStewart game
G(L(A));
but the winning strategies cannot be recursive and not even hyperarithmetical.
(2) There exists a model of ZFC in which the GaleStewart game is not determined.
17:3617:48Alessandro
Facchini, Michał Skrzypczak and Filip Murlak Game or not Game?
SLIDES speaker: Alessandro Facchini
Abstract
Recently the present authors have shown that both the nondeterministic
and the alternating RabinMostowski index problems are decidable for languages recognisable by
socalled game automata, which can be seen as the closure of deterministic ones under
complementation and composition.
In order to be able to claim decidability of the index problem for a given subclass of regular
languages, one should however prove that membership in is decidable too. In this talk we show that
membership in the class of languages recognizable by game automata is decidable.
17:4818:00Jacques
Duparc and Yann Pequignot Playing reduction games on Scott domains
SLIDES speaker: Yann Pequignot
Abstract
If we take the complexity of a property to mean the difficulty of
determining when it holds, 'simple` reductions provide a way to organise properties in terms of
their complexity. In a topological space, the notion of Wadge reducibility is obtained by
interpreting 'simple` as continuous. While on the Cantor space this gives a nice and useful
hierarchy on the Borel sets, on the real line, for example, Wadge reducibility gives no hierarchy at
all.
We define a notion of reducibility for second countable T0 topological spaces, based on admissible
representations, which always semiwellorders the Borel sets.
18:0018:12Henryk
Michalewski Regular languages of infinite trees of low Borel
complexity
SLIDES speaker: Henryk Michalewski
Abstract
M. Bojanczyk and T. Place proved that for a regular language of
infinite trees it is decidable if it is a boolean combination of open sets. The class of Delta^0_2
sets consists of sets which are simultaneously F_sigma and G_delta. Every boolean combination of
open sets belongs to the class Delta^0_2. I will present a small modification of the result of M.
Bojanczyk and T. Place. Namely, provide an algorithm to decide whether a given regular language of
infinite trees belongs to the class \Delta^0_2.
18:1218:24Yde
Venema Game bisimulations between basic positions
SLIDES speaker: Yde Venema
Abstract
Acceptance games and evaluation games provide examples of parity games
in which some positions can be singled out as being *basic*, in the sense
that (1) matches proceed in *rounds*, moving from one basic position to
another, and (2) when determining the winner of an infinite match, only
the basic positions matter.
We introduce a notion of bisimulation between two such games that
combines Pauly's bisimulation between extensive strategic games, with a
combinatorial part for the parity condition.
Applications include the proof of complementation lemmas in automata
theory.
18:2418:36David
Janin From strings to higher dimensional strings
SLIDES speaker: David Janin
Abstract
There are wellknown connections between word language theory and
semigroup theory, mediated by free monoids, with deep link with the theory of finite state automata.
By considering free inverse monoids instead of free monoids and premorphisms into ordered monoids
instead of morphisms into monoids, we manage to lift these connections to languages of finite trees
and, beyond, towards a more general notion of higher dimensional strings. In this talk, we will give
a quick overview of the background results with a special emphasis on the main underlying concepts
and methods.
Saturday 21 September
09:0009:50Invited Talk
09:0009:50Moshe Y.
Vardi Invited Talk: The rise and fall of Linear Temporal Logic
SLIDES speaker: Moshe Y. Vardi
Abstract
One of the surprising developments in the area of program verification
in the late part of the 20th Century is the emergence of Linear Temporal Logic (LTL), a logic that
emerged in philisophical studies of free will, as the cannonical language for describing temporal
behavior of computer systems. LTL, however, is not expressive enough for industrial applications.
The first decade of the 21 Century saw the emergence of industrial temporal logics such as ForSpec,
PSL, and SVA. These logics, however, are not clean enough to serve as objects of theoretical study.
This talk will describe the
rise and fall of LTL, and will propose a new cannonical temporal logic: Linear Dynamic Logic (LDL).
09:5010:00Break
10:0011:15Session 10A
10:0010:15Fabio
Mogavero, Aniello Murano and Luigi Sauro On the boundary of behavioral
strategies
SLIDES speaker: Aniello Murano
Abstract
In multiagent games, a recent contribution is given by Strategy Logic
(SL),
a powerful formalism that allows to reason explicitly about strategies as first order objects.
The price to pay for the high expressiveness of SL is that it admits nonbehavioral strategies,
i.e., a choice of an agent in a play may depend on choices made in another counterfactual play.
As the latter moves are unpredictable, these strategies cannot be synthesized in practice.
In this talk, we introduce two maximal syntactical fragments of SL admitting behavioral strategies
only.
As a consequence, we show that the modelchecking problem for both fragments is solvable in
2EXPTIME,
as it is for the subsumed ATL*.
10:1510:30Francois
Laroussinie and Nicolas Markey Satisfiability of ATL with strategy
contexts
SLIDES speaker: Nicolas Markey
Abstract
ATLsc is a powerful formalism for reasoning about multiagent systems;
it is a
natural variant of the semantics of the logic ATL, as defined by Alur,
Henzinger and Kupferman. Using a translation into QCTL (CTL extended with
quantification over atomic propositions), we prove that ATLsc satisfiability
is decidable when satisfiability is restricted to turnbased games, or when
the set of moves allowed to the players in advance. On the other hand, when
strategy quantification is restricted to memoryless strategies, satisfiability
is undecidable in all considered cases.
10:3010:45Amélie
David and Serenella Cerrito From ATL tableaux to alternating
automata
SLIDES speaker: Amélie David
Abstract
In a global context of formal specification, a theoritecal question is
: as for LTL, is it possible to construct an automaton from a tableaubased decision procedure for
ATL (Alternatingtime Temporal Logic)? To answer that question, we propose a new way of constructing
a specific kind of alternating tree automaton, the so called joker automaton, from the construction
of the tableaubased decision procedure for ATL [Goranko,Shkatov/2009]. This new automaton recognize
all models of a formulae without restrictions on the moves of agents.
10:4511:00Francesco
Belardinelli, Andrew Vaughan Jones and Alessio Lomuscio Model checking
TemporalEpistemic Logic using alternating tree automata
SLIDES speaker: Francesco Belardinelli
Abstract
We introduce a novel automatatheoretic approach for the
verification of multiagent systems. We present epistemic
alternating tree automata, an extension of alternating tree
automata, and use them to represent specifications in the
temporal epistemic logic CTLK. We show that model check
ing a memoryless interpreted system against a CTLK prop
erty can be reduced to checking the language nonemptiness
of the composition of two epistemic tree automata. We report
on an experimental implementation and discuss preliminary
results. We evaluate the effectiveness of the technique using
two reallife scenarios: a gossip protocol and the train gate
controller.
11:0011:15Rodica
Bozianu, Cătălin Dima and Constantin Enea: The epistemic
μcalculus
SLIDES speaker: Catalin Dima
Abstract
We discuss expressivity issues concerning the epistemic mucalculus
with
synchronous and perfect recall semantics w.r.t. games with partial observation,
alternating temporal logics with incomplete observation, and an extension of the
monadic secondorder logic on trees.
10:0011:15Session 10B
10:0010:15Jakub
Michaliszyn, Jan Otop and Emanuel Kieronski Elementary modal logics 
decidability and complexity
SLIDES speaker: Jakub Michaliszyn
Abstract
Modal logic is called "elementary" if it is considered over class of
frames definable by a firstorder formula. Different formulae lead to different logics, and many of
them find their applications in computer science.
The aim of the Highlights conference talk is to present a wide picture of the latest research on the
satisfiability problem of elementary modal logics.
The talk will provide all the necessarily definitions, discuss the motivation, summarise the recent
research papers on this topic, and discuss some open problems.
10:1510:30Angelo
Montanari and Pietro Sala Adding an equivalence relation to the interval
logic complexity and expressiveness
SLIDES speaker: Pietro Sala
Abstract
We study the effects of the addition of an equivalence relation to one
of the most representative
interval temporal logics, namely, the logic ABBbar of Allen's relations "meets", "begun by", and
"begins".
We first prove that the satisfiability problem for the resulting logic ABBbarsim remains decidable
over finite linear orders, but it becomes nonprimitive recursive, while decidability is lost over
$\bbN$.
Then, we show that ABBbarsim is expressive enough to define $\omega{S}$regular languages.
10:3010:45Arthur
Milchior Deciding in polynomial time whether a set recognized by an
automaton is definable in FO[<,mod]
SLIDES speaker: Arthur Milchior
Abstract
In this talk, we are interested by expressivity of automaton
reading a base b rtuple of natural numbers.
It is well known that those automaton recognize brecognizable set.
We will study how to decide, in polynomial time if the set recognized
by an automaton is definable a smaller structure as \FO[+] or
\FO[<,\moda], and how to compute a formula in this structure that
accepts this set.
10:4511:00Dietrich
Kuske Logical aspects of the lexicographic order on 1counter
languages
SLIDES speaker: Dietrich Kuske
Abstract
From Rabin's tree theorem, one can infer that the monadic second order
theory of the lexicographic order on any regular language is
decidable. The same holds for deterministic contextfree languages
since they belong to Caucal's hierarchy. When dropping determinism,
not even the firstorder theory remains decidable (\'Esik \&
Carayol). This talk demonstrates that undecidability occurs already for
\begin{itemize}
\item small fragments of firstorder logic and
\item 1counter automata that are very close to being deterministic.
\end{itemize}
11:0011:15Thomas
Colcombet Magnitude Monadic Logic over words and the use of relative
internal set theory
SLIDES speaker: Thomas Colcombet
Abstract
Cost monadic logic extends monadic secondorder logic with the ability
to measure the cardinality of sets and comes with decision procedures for boundedness related
questions. We provide new decidability results allowing the systematic investigation of questions
involving “relative boundedness”. We first introduce a suitable logic, magnitude monadic logic. We
then establish the decidability of this logic over finite words. We finally advocate that developing
the proofs in the axiomatic system of “relative internal set theory”, a variant of nonstandard
analysis, entails a significant simplification of the proofs.
11:1511:45Coffee break
11:4513:00Session 11A
11:4512:00Fabio
Mogavero, Aniello Murano and Loredana Sorrentino On promptness in parity
games
SLIDES speaker: Loredana Sorrentino
Abstract
In this paper, we make a general study of the concept of promptness in
parity
games that allows to put under a unique theoretical framework several of the
cited variants along with new ones.
Also, we describe simple polynomial reductions from all these conditions to
either Buchi or parity games, which simplify all previous known procedures.
12:0012:15Nils
Bulling and Valentin Goranko Combining quantitative and qualitative
strategic reasoning in concurrent multiplayer games
SLIDES speaker: Valentin Goranko
Abstract
We propose a logical modeling framework, combining a gametheoretic
study of the abilities of players to achieve quantitative objectives in multiplayer games
(optimizing payoffs or preferences on outcomes) with a logical analysis of the abilities of players
for achieving qualitative objectives (reaching or maintaining game states with desired properties).
We enrich concurrent game models with payoffs for the normal form games associated with each state
of the model and propose a quantitative extension of the logic ATL* enabling combination of
quantitative and qualitative reasoning.
12:1512:30Alessio
Lomuscio, Hongyang Qu and Franco Raimondi MCMAS: A model checker for the
verification of multiagent systems
SLIDES speaker: Alessio Lomuscio
Abstract
12:3012:45Romain
Brenguier, JeanFrançois Raskin and Mathieu Sassolas The complexity of
admissibility in omegaregular games
SLIDES speaker: Mathieu Sassolas
Abstract
11A2Sassolas.txt
Iterated admissibility is a wellknown and important concept in classical game theory, e.g. to
determine rational behaviors in multiplayer matrix games.
As recently shown by Berwanger, this concept can be soundly extended to infinite games played on
graphs with omegaregular objectives.
In this talk, we study the algorithmic properties of this concept for such games.
We settle the exact complexity of natural decision problems on the set of strategies that survive
iterated elimination of dominated strategies.
As a byproduct of our construction, we obtain automata which recognize all the possible outcomes of
such strategies.
12:4513:00Leander
Tentrup A compositional proof rule for Coordination Logic
SLIDES speaker: Leander Tentrup
Abstract
We present the first proof system for Coordination Logic (CL). CL
provides a logical representation for the distributed realizability problem and extends the
gamebased temporal logics with quantification over strategies under incomplete information.
The proof system is based on a reduction from CL to its decidable fragment.
We propose a compositional proof rule which splits a given CL formula into two parts, a decidable CL
formula and another, simplified, CL formula. Applying the rule repeatedly transforms the original CL
formula into a collection of decidable CL formulas.
Our proof system is a complete framework for the synthesis of distributed systems.
11:4513:00Session 11B
11:4512:00Antoine
DurandGasselin Is the generic algorithm for firstorder modelchecking
automatic structures optimal ?
SLIDES speaker: Antoine DurandGasselin
Abstract
Automatic structures are relational structures whose domain can be
presented as a regular language and predicates as synchronously
regular relations. The main result on automatic structures is an
explicit algorithm to build an automaton that accepts any
firstorder relation, relying on the correspondance between logical
connectives and classical operations over automata.
In general, building this automaton is nonelementary, but for some
automatic structures with elementary firstorder theory, we show that
this construction has a complexity close to that of the logic.
12:0012:15Claudia
Carapelle, Alexander Kartzow and Markus Lohrey Satisfiability of CTL*
with constraints
SLIDES speaker: Claudia Carapelle
Abstract
CTL* formulas can be enriched to express relations between variables
whose value can range in a chosen
concrete domain.
Chosen the appropriate domain one can express quantitative properties that ordinary CTL^* formulas
can only approximate through abstraction. We can refer directly to concrete values and describe how
they
change in time.
In this talk we show that satisfiability for CTL* with equality, order, and modulo
constraints over the Z is decidable
12:1512:30Tomáš
Babiak, František Blahoudek, Mojmir Kretinsky and Jan Strejček Effective
translation of LTL to deterministic Rabin automata: Beyond the (F,G)fragment
SLIDES speaker: Jan Strejcek
Abstract
Some applications of linear temporal logic (LTL) require to translate
formulae of the logic to deterministic omegaautomata. There are currently
two translators producing deterministic automata: ltl2dstar working for the
whole LTL and Rabinizer applicable to LTL(F,G) which is the LTL fragment
using only modalities F and G. We present a new translation to
deterministic Rabin automata via alternating automata and deterministic
transitionbased generalized Rabin automata. Our translation applies to a
fragment that is strictly larger than LTL(F,G). Experimental results show
that our algorithm can produce significantly smaller automata compared to
Rabinizer and ltl2dstar, especially for more complex LTL formulae.
12:3012:45Dominik D.
Freydenberger and Timo Kötzing Fast learning of restricted regular
expressions and DTDs
SLIDES speaker: Dominik D. Freydenberger
Abstract
We study the problem of generalizing from a finite sample to a language
taken from a predefined language class. The two language classes we consider are generated by
restricted regular expressions (CHAREs and SOREs) that have significance in the specification of XML
documents.
For each of the two language classes we give an efficient algorithm returning a minimal
generalization from the given finite sample to an element of the fixed language class; such
generalizations are called descriptive. In this sense, both our algorithms are optimal.
12:4513:00Rajeev
Alur, Loris D'Antoni, Sumit Gulwani, Dileep Kini and Mahesh Viswanathan Automated grading of DFA constructions
SLIDES speaker: Loris D'Antoni
Abstract
One challenge in making online education more effective is to develop
automatic grading software that can provide meaningful feedback. This paper provides a solution to
automatic grading of the standard computationtheory problem that asks a student to construct a
deterministic finite automaton from the given description of its language. We focus on how to assign
partial grades for incorrect answers. We experimentally show that the tool is able to assign partial
grades in a meaningful way, and should be preferred over the human graders for both scalability and
consistency.
13:0014:00Lunch
14:0015:15Session 12A
14:0014:15Loris
D'Antoni and Rajeev Alur Streaming tree transducers
SLIDES speaker: Loris D'Antoni
Abstract
We introduce streaming tree transducers as an analyzable, executable,
and expressive model for transforming unranked ordered trees. Given a linear encoding of the input
tree, the transducer makes a single lefttoright pass through the input, and computes the output
using a finitestate control, a visibly pushdown stack, and a finite set of variables storing output
chunks that can be combined using concatenation and insertion. We prove the model to be equivalent
to monadic secondorder logic transductions. We show complexity bounds of ExpTime for typechecking
and NExpTime for equivalence.
14:1514:30Emmanuel
Filiot, Olivier Gauwin, PierreAlain Reynier and Frédéric Servais From
twoway to oneway finite state transducers
SLIDES speaker: Emmanuel Filiot
Abstract
Any twoway finite state automaton is equivalent to some oneway
finite state automaton.
This wellknown result, shown by Rabin and Scott and independently
by Shepherdson, states that twoway finite state automata (even nondeterministic) characterize
the class of regular languages. It is also known that this result
does not extend to finite string transductions: (deterministic)
twoway finite state transducers strictly extend the expressive
power of (functional) oneway transducers. In particular
deterministic twoway transducers capture exactly the class of MSOtransductions of finite strings.
In this talk, we address the following definability problem: given
a function defined by a twoway finite state transducer, is it definable by
a oneway finite state transducer? By extending Rabin and Scott's proof to
transductions, we show that this problem is decidable.
Our procedure builds a oneway transducer, which is equivalent to
the twoway transducer, whenever one exists.
14:3014:45Inès
Klimann Automaton semigroups: the twostate case
SLIDES speaker: Klimann Ines
Abstract
A Mealy automaton is a deterministic, complete, letterbyletter
transducer, with same input and output alphabet. We can consider the
semigroup generated by the functions on words induced by its states.
We prove that semigroups generated by reversible twostate Mealy
automata have remarkable growth properties: they are either finite or
free. We give an effective procedure to decide finiteness or freeness
of such semigroups when the generating automaton is also invertible.
14:4515:00Henryk
Michalewski and Michał Skrzypczak Complexity collapse for unambiguous
languages
SLIDES speaker: Michał Skrzypczak
Abstract
A nondeterministic automaton is unambiguous if it has at most one
accepting run on every input. The class of languages recognisable by unambiguous tree automata is
still not wellunderstood. In this paper we show the following complexity collapse: if A is an
unambiguous Buchi tree automaton then L(A) is recognisable by a weak alternating automaton. We
present also some extensions of this result. To our best knowledge this is the first parity index
collapse that exploits unambiguity of an automaton.
15:0015:15Szczepan
Hummel Unambiguitypreserving operation on tree languages that lifts
topological complexity
SLIDES speaker: Szczepan Hummel
Abstract
We propose an operation on languages of infinite trees that
significantly increases topological complexity but preserves unambiguity.
We prove that iterating the operation yields topologically harder and harder sets.
As an illustration, we might note that application of the operation to the empty language already
produces a nonBorel set, and the next application of the operation produces a set that is outside
the sigmafield generated by analytic sets.
Moreover, we show how to perform a limit step of the iteration.
14:0015:15Session 12B
14:0014:15Can
Bașkent What is game theoretical negation?
SLIDES speaker: Can Baskent
Abstract
In this talk, I will give a game semantics for a paraconsistent logic,
and define a paraconsistent "win"  parallel to the paraconsistent understanding of truth.
14:1514:30Agnieszka
Kulacka Expressive completeness of some logics
SLIDES speaker: Agnieszka Kulacka
Abstract
Expressive completeness, which is one of the themes in this field of
research, compares the power of these logics to fragments of firstorder logic over some class of
frames. If logic is as expressive as first order logic, as logic US (with connectives Until, Since)
is shown to be, it is as powerful as possible. It can express the same statements, but in a more
concise and readable way.
In this presentation I will show a method of proving expressive completeness of a temporal logic by
the use of games. This will be demonstrated on example of a temporal logic with connectives Future
and Past.
14:3014:45Claudia
Carapelle, Shiguang Feng, Oliver Gil and Karin Quaas EhrenfeuchtFraisse
games for Freeze LTL and Metric Temporal Logic over data words
SLIDES speaker: Shiguang Feng
Abstract
We consider TPTL(Z) and MTL(Z) whose semantics are based on
nonmonotonic data words in which every point is assigned a natural number as its weight. We define a
weighted version of the EF game on MTL. Using these games, we prove the following:
1. TPTL(Z) is strictly more expressive than MTL(Z).
2. The until hierarchy and the constant hierarchy are strict for MTL(Z).
3. It is undecidable whether a given TPTL(Z) formula can be expressed in MTL(Z).
14:4515:00Piotr
Hofman, Richard Mayr and Patrick Totzke Decidability of weak simulation
on onecounter nets
SLIDES speaker: Patrick Totzke
Abstract
Onecounter nets (OCN) are Petri nets with exactly one unbounded place.
They are equivalent to a subclass of onecounter automata with only a
weak test for zero.
We show that weak simulation preorder is decidable for OCN. In contrast,
other semantic relations like weak bisimulation are undecidable for OCN,
and so are weak (and strong) trace inclusion.
15:0015:15Piotr
Hofman, Sławomir Lasota, Patrick Totzke and Richard Mayr Strong
simulation for one counter nets is PSPACEcomplete
SLIDES speaker: Piotrek Hofman
Abstract
A one counter net is a one counter automaton without possibility of
testing 0 value. We proved that solving the simulation problem for one counter nets is PSPACE
complete.
15:1515:45Coffee break
15:4517:00Session 13A
15:4516:00Christian
Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini and Lijun Zhang The quest for minimal quotients for probabilistic automata
SLIDES speaker: Christian Eisentraut
Abstract
16:0016:15Nathanaël
Fijalkow and Florian Horn We tried and we tried, and we applied and
implied, and still probabilistic automata we could not decide!
16:1516:30Parosh Aziz
Abdulla, Richard Mayr, Arnaud Sangnier and Jeremy Sproston Solving parity
games on integer vectors
SLIDES speaker: Arnaud Sangnier
Abstract
16:3016:45Maria
Svorenova, Ivana Černá and Călin Belta Optimal control of MDPs with
Temporal Logic constraints
SLIDES speaker: Maria Svorenova
Abstract
In this work, we focus on control of Markov decision processes with nonnegative realvalued costs.
We develop an algorithm to design a control strategy that guarantees the satisfaction of a
correctness specification expressed as a formula of Linear Temporal Logic, while at the same time
minimizing the expected average cost between two consecutive satisfactions of a desired property.
The existing solutions to this problem in control theory are suboptimal. By leveraging ideas from
automatabased model checking and game theory, we provide an optimal solution.
16:4517:00Holger
Hermanns, Jan Krčál and Jan Kretinsky Compositional verification and
optimization of interactive Markov chains
SLIDES speaker: Jan Krčál
Abstract
We provide the first assumeguarantee reasoning for stochastic
continuoustime systems. Interactive Markov chains (IMC) are compositional behavioural models
similar to continuoustime Markov decision processes. Given a timebounded property, an IMC
component and a specification of the environment, we synthesize a scheduler optimizing the
probability that the property is satisfied when the IMC is working in an unknown environment that
satisfies the specification. In this talk we focus on a twoplayer continuoustime stochastic game
model that we call controllerenvironment games that is the crucial step in the solution of the
problem above.
15:4517:00Session 13B
15:4516:00Yde
Venema Expressiveness modulo bisimilarity: a coalgebraic
perspective
SLIDES speaker: Yde Venema
Abstract
Janin and Walukiewicz showed that the modal mucalculus MC is the
bisimulationinvariant fragment of monadic secondorder logic MSO.
Their proof uses parity automata with a transition map defined in
terms of monadic firstorder logic. We decompose their proof in
three parts:
(1) automatatheoretic characterizations of MSO and MC respectively,
(2) a simple modeltheoretic characterization of the identityfree
fragment of monadic firstorder logic, and
(3) a coalgebraic result, stating that the second result propagates
from the `onestep level' to the level of full fixpoint logics.
16:0016:15Joost
Winter, Helle Hvid Hansen, Clemens Kupke and Jan Rutten A final coalgebra
for kregular and kautomatic sequences
SLIDES speaker: Joost Winter
Abstract
We offer a coalgebraic perspective on the kregular sequences. For any
k >= 1 and semiring S, the set of sequences with output in S is the carrier of a final coalgebra.
This allows us to give a coalgebraic characterization of the kregular sequences. Using an
isomorphism based on a bijective numeration system, we thus obtain a structural correspondence
between Srational series over k nonterminals, and kregular sequences with output in S. We will
furthermore discuss a connection with sequences definable by divide and conquer recurrences.
16:1516:30Boris
Düdder, Moritz Martens and Jakob Rehof: Combinatory Logic synthesis and
alternation
SLIDES speaker: Boris Düdder
Abstract
We discuss complexity theoretic results in the context of Combinatory
Logic Synthesis which is a new approach to componentbased synthesis using type inhabitation. The
complexity theoretic reductions behind these results establish explicit and effective connections
between combinatory logic inhabitation and automata theoretic models, in the form of alternating
tree automata and alternating space bounded Turing machines. These computational models that are
commonly found in automata theoretic approaches are related to synthesis based on logics within the
MSO family of logics.
16:3016:45Sophia
Knight, Catuscia Palamidessi, Prakash Panangaden and Frank Valencia Spatial and epistemic modalities in constraintbased process calculi
SLIDES speaker: Sophia Knight
Abstract
We describe the role epistemic reasoning can play in concurrency
theory. The idea of using modalities as programming constructs has been largely unexplored. We add
epistemic and spatial modalities as part of the programming language, not just as part of the
metalanguage to reason about protocols.
We introduce spatial and epistemic process calculi to reason about information and knowledge
distributed among agents in a system. We give domaintheoretic structures to represent this
information, operational and denotational means to reason about possibly infinite behavior, and
compact versions of infinite objects to simulate public announcement.