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 LerouxAbstract
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 GroheAbstract
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 GodefroidAbstract
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 SirangeloAbstract
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 VrgocAbstract
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 FontaineAbstract
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 BoomAbstract
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ńskiAbstract
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 KaiserAbstract
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 BruseAbstract
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 HunterAbstract
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 HarwathAbstract
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ńskiAbstract
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 RooijenAbstract
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 MayrAbstract
12:4813:00Nathanaël Fijalkow, Krishnendu Chatterjee, Thomas Colcombet, Florian Horn, Denis Kuperberg,Michał Skrzypczak and Martin Zimmermann Boundedness games
SLIDES speaker: Nathanael FijalkowAbstract
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 LucAbstract
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 DaviaudAbstract
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 RaghothamanAbstract
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 SakarovitchAbstract
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öllerAbstract
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 FigueiraAbstract
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öllerAbstract
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 LazicAbstract
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ąszczAbstract
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 SchmitzAbstract
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 BrihayeAbstract
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 BrihayeAbstract
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 ChatterjeeAbstract
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 ShirmohammadiAbstract
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 KretinskyAbstract
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 BrazdilAbstract
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ädelAbstract
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 DawarAbstract
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 LindellAbstract
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žálekAbstract
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 VerbitskyAbstract
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 HeimbergAbstract
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 PapermanAbstract
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 KlinAbstract
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 SuzukiAbstract
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 TorunczykAbstract
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 ManuelAbstract
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 LasotaAbstract
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 BundalaAbstract
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 FigueiraAbstract
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 ScarsiniAbstract
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 StephaneAbstract
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 JamrogaAbstract
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 FaellaAbstract
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 RandourAbstract
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 LangAbstract
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 GelderieAbstract
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 MioAbstract
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 FinkelAbstract
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 FacchiniAbstract
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 PequignotAbstract
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 MichalewskiAbstract
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 VenemaAbstract
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 JaninAbstract
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. VardiAbstract
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 MuranoAbstract
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 MarkeyAbstract
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 DavidAbstract
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 BelardinelliAbstract
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 DimaAbstract
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 MichaliszynAbstract
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 SalaAbstract
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 MilchiorAbstract
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 KuskeAbstract
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 ColcombetAbstract
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 SorrentinoAbstract
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 GorankoAbstract
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 LomuscioAbstract
12:3012:45Romain Brenguier, JeanFrançois Raskin and Mathieu Sassolas The complexity of admissibility in omegaregular games
SLIDES speaker: Mathieu SassolasAbstract
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 TentrupAbstract
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 DurandGasselinAbstract
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 CarapelleAbstract
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 StrejcekAbstract
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. FreydenbergerAbstract
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'AntoniAbstract
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'AntoniAbstract
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 FiliotAbstract
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 InesAbstract
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ł SkrzypczakAbstract
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 HummelAbstract
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 BaskentAbstract
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 KulackaAbstract
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 FengAbstract
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 TotzkeAbstract
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 HofmanAbstract
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 EisentrautAbstract
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 SangnierAbstract
16:3016:45Maria Svorenova, Ivana Černá and Călin Belta Optimal control of MDPs with Temporal Logic constraints
SLIDES speaker: Maria SvorenovaAbstract
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čálAbstract
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 VenemaAbstract
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 WinterAbstract
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üdderAbstract
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 KnightAbstract
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.