Name:

Password:


PRAGUE, 15–18 SEPTEMBER 2015

Tutorial day: 15 SEPTEMBER

Conference: 16–18 SEPTEMBER


menu

The goal of Highlights conferences is to integrate the community working on logic, games and automata.


A visit to Highlights conference should offer a wide picture of the latest research in the area and a chance to meet everybody in the field, not just those who happen to publish in one particular proceedings volume.


We encourage you to attend and present your best work, be it already published or not, at the Highlights conference!

Important dates

  • Talk submission deadline: June 12, 2015.
  • Notification: June 19, 2015.
  • Early registration: July 15, 2015 (extended).
  • Tutorial day: September 15, 2015.
  • Conference: September 16-18, 2015.

Previous editions

NO PROCEEDINGS

There are no proceedings. You present your best work, be it published elsewhere or yet unpublished.

SHORT

The conference is three days long. The contributed talks are around ten minutes.

CHEAP

The participation costs are modest. Prague is easy to reach.

EVERYBODY IS DOING IT!

Let's use the conference model that is so successful in other fields, like mathematics.

Highlights 2015

Prague, September 15–18


SPECIAL LECTURE

Moshe Vardi


INVITED SPEAKERS

Christel Baier

Thomas Colcombet

Giuseppe De Giacomo

Philippe Schnoebelen


TUTORIALS

Libor Barto (CSP)

Paul Gastin (Weighted Automata)

Call for paper:

The goal of Highlights conferences is to integrate the community working on logic, games and automata. Papers on these topics are dispersed across many conferences, which makes them difficult to follow.


A visit to Highlights conference should offer a wide picture of the latest research in the area and a chance to meet everybody in the field, not just those who happen to publish in one particular proceedings volume.


We encourage you to attend and present your best work, be it already published or not, at the Highlights conference!


Scope:

Representative areas include, but are not restricted to:

  • logic and finite model theory
  • automata theory
  • games for logic and verification

Important guidelines:

You submit a talk, not a paper. Hence, submissions should have a single author, who is the speaker. Since you should only present your favorite result of the year, there should be at most one submission per speaker. The abstract, of at most 1-2 pages, may include a list of coauthors.


There are no formal proceedings and we encourage submission of work presented elsewhere.


Where and when to submit:

Talk submissions are done via the Highlights 2015 EasyChair site


The submission deadline is June 12, 2015. Notifications will be sent by June 19, 2015.

The registration is now open. Please go to the registration page. After July 15, registration remains open, but the options for cheap accommodation will not be available anymore.

Tuesday 15 September — Tutorials (T1 Lecture room, Suchdol)

09:0009:30 Welcome & Breakfast
09:3012:30 Tutorial
09:3012:30 Libor Barto Tutorial: Constraint Satisfaction Problem
speaker: Libor Barto
12:3014:30 Lunch
14:3017:00 Tutorial
14:3017:00 Paul Gastin Tutorial: Weighted Automata
speaker: Paul Gastin

Wednesday 16 September (Blue Lecture Hall, Karolinum)

09:30 10:30 Invited talk
09:30 10:30 Thomas Colcombet TBA
speaker: Thomas Colcombet

Abstract

  

TBA

10:30 10:50 Coffee Break
10:50 12:02 Session 1
10:50 11:02 Nadia Labai Eliminating Logic from Meta Theorems
speaker: Nadia Labai

Abstract

  

A meta theorem, in our context, is a statement about a logic L of the form: ``If a graph parameter f is definable in L, then it is computable in polynomial time over graph classes of a certain kind.'' A famous example is Courcelle’s theorem, which states that the definability of graph properties in Monadic Second Order Logic implies they are linear time computable over graph classes of bounded tree-width.
In 1998 the theorem was generalized to graph parameters and graph classes of bounded clique-width by Courcelle, Makowsky, and Rotics. In 2004, J.A. Makowsky gave a further generalized meta theorem involving sum-like inductive graph classes, which are inductively defined using a finite set of basic graphs and a finite set of binary sum-like operations.

We eliminate logic from these meta theorems by replacing their definability conditions with finiteness conditions on Hankel matrices. A Hankel matrix H(f,\Box) for a graph parameter f and a binary operation \Box on graphs is an infinite matrix where the rows and columns are labeled with graphs, and the entry corresponding to the row labeled with G and the column labeled with G' is given by the value f(G \Box G'). We show that the graph parameters covered by our logic-free treatment are a proper superset of the graph parameters covered by the meta theorems involving logic.

Joint work with J.A. Makowsky.

11:02 11:14 Michał Skrzypczak Definability of choice over scattered trees in MSO
speaker: Michał Skrzypczak

Abstract

  

Scattered trees (called also tame or thin) are infinite trees with only countably many branches. During the presentation I will introduce and motivate the following problem: is there a formula of monadic second-order logic phi(x,X) such that for every set X of nodes of a scattered tree, phi(x,X) holds for a unique element x of X (such a formula is said to define a choice function).

The problem is a strengthening of a theorem of Gurevich and Shelah proving non-definability of a choice function over the complete binary tree. Somehow surprisingly, the problem is strongly related to unambiguous languages of complete binary trees. In particular, a solution to the problem would imply an effective characterisation of the class of bi-unambiguous languages. Also, the problem admits an equivalent statement in terms of thin algebras (a natural extension of both Wilke algebras and forest algebras).

11:14 11:26 Tomer Kotek Monadic second order finite satisfiability and unbounded tree-width
speaker: Tomer Kotek

Abstract

  

The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result [Seese, D. (1991). The structure of the models of decidable monadic theories of graphs. Annals of pure and applied logic, 53(2), 169-195]. We prove the following problem is decidable:

Input: (i) A monadic second order logic sentence \alpha, and (ii) a sentence \beta in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of \alpha and \beta may intersect.

Output: Is there a finite structure which satisfies both \alpha and \beta such that the restriction of the structure to the vocabulary of \alpha has bounded tree-width? (The tree-width of the desired structure is not bounded.)

As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic extending monadic second order logic with linear cardinality constraints of the form |X_1|+...+|X_r|<|Y_1|+...+|Y_s|, where the X_i and Y_j are monadic second order variables. We prove the decidability of a similar extension of WS1S.

11:26 11:38 Dietrich Kuske Infinite and Bi-infinite Words with Decidable Monadic Theories
speaker: Dietrich Kuske

Abstract

  

We study word structures of the form (D,<,P) where (D,<) denotes the order of the natural numbers or of the integers and P is a unary predicate on D. In particular we show:

(a) the set of recursive omega-words with decidable monadic second order theories is Sigma_3-complete (i.e., complete for the third existential level of the arithmetical hierarchy).

(b) We characterise those sets P of integers that yield bi-infinite words with decidable monadic second order theories.

(c) We show that such "tame" predicates P exist in every Turing degree.

Through these results we demonstrate similarities and differences between logical properties of infinite and bi-infinite words.

These results have been obtained in collaboration with Jiamou Liu and Anastasia Moskvina from Auckland University of Technology.

11:38 11:50 Martin Lang A unified approach to boundedness properties in MSO
speaker: Martin Lang

Abstract

  

In the past years, extensions of monadic second-order logic (\MSO) that can specify boundedness properties by the use of operators referring to the sizes of sets have been considered. In particular, the logics costMSO introduced by T. Colcombet and MSO+U by M. Bojanczyk were analyzed and connections to automaton models have been established to obtain decision procedures for these logics. We propose the logic quantitative counting MSO (qcMSO for short), which combines aspects from both costMSO and MSO+U. We show that both logics can be embedded into qcMSO in a natural way. Moreover, we provide decidability proofs for the theory of its weak variant (quantification only over finite sets) for the natural numbers with order and the infinite binary tree. These decidability results are obtained using a regular cost function extension of automatic structures called resource-automatic structures.

This is joint work with Simon Leßenich, Christof Löding and Lukasz Kaiser. It is currently submitted for publication.

11:50 12:02 Henryk Michalewski How unprovable is Rabin's theorem?
speaker: Leszek Kołodziejczyk

Abstract

  

We study the strength of set-theoretic axioms needed to prove Rabin's theorem on the decidability of the MSO theory of the infinite binary tree. We first show that the complementation theorem for tree automata, which forms the technical core of typical proofs of Rabin's theorem, is equivalent over the modestly strong second-order arithmetic theory ACA_0 to the statement Det asserting the determinacy of all Gale-Stewart games with winning conditions given by boolean combinations of F_\sigma sets. From work of Medsalem and Tanaka it follows that the statement Det is provable from \Pi^1_3- but not \Delta^1_3-comprehension.

We then prove that the decidability of MSO on the infinite binary tree is itself equivalent to the statement Det over \Pi^1_2-comprehension. Hence, \Delta^1_3-comprehension is not enough to prove Rabin's theorem. Moreover, relying on the work of Moellerfeld, we show that Rabin's theorem is equivalent over \Pi^1_2-comprehension to a purely logical reflection principle: "every \Pi^1_3 sentence provable from \Pi^1_2 comprehension is true".

12:02 13:30 Lunch
13:30 14:30 Invited talk
13:30 14:30 Giuseppe De Giacomo TBA
speaker: Giuseppe De Giacomo

Abstract

  

TBA

14:30 14:40 Break
14:40 15:40 Session 2
14:40 14:52 Krishnendu Chatterjee Strategy Complexity of Concurrent Stochastic Games with Safety and Reachability Objectives
speaker: Krishnendu Chatterjee

Abstract

  

We consider finite-state concurrent stochastic games, played by k>=2 players for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. We consider reachability objectives that given a target set of states require that some state in the target is visited, and the dual safety objectives that given a target set require that only states in the target set are visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest nonzero probability employed. Our main results are as follows: We show that in two-player zero-sum concurrent stochastic games (with reachability objective for one player and the complementary safety objective for the other player): (i) the optimal bound on the patience of optimal and epsilon-optimal strategies, for both players is doubly exponential; and (ii) even in games with a single nonabsorbing state exponential (in the number of actions) patience is necessary. In general we study the class of non-zero-sum games admitting stationary epsilon-Nash equilibria. We show that if there is at least one player with reachability objective, then doubly-exponential patience may be needed for epsilon-Nash equilibrium strategies, whereas in contrast if all players have safety objectives, the optimal bound on patience for epsilon-Nash equilibrium strategies is only exponential.

This is a joint work with Kristoffer Arnsfelt Hansen and Rasmus Ibsen-Jensen. The full version of the manuscript is available in Arxiv. The link is as follows: http://arxiv.org/abs/1506.02434

14:52 15:04 Mickael Randour Percentile Queries in Multi-Dimensional Markov Decision Processes
speaker: Mickael Randour

Abstract

  

Markov decision processes (MDPs) with multi-dimensional weights are useful to analyze systems with multiple objectives that may be conflicting and require the analysis of trade-offs. In this paper, we study the complexity of percentile queries in such MDPs and give algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function~$f$, thresholds $v_i$ (one per dimension), and probability thresholds $\alpha_i$, we show how to compute a single strategy to enforce that for all dimensions $i$, the probability of outcomes $\rho$ satisfying $f_i(\rho) \geq v_i$ is at least $\alpha_i$. We consider classical quantitative payoffs from the literature (sup, inf, lim sup, lim inf, mean-payoff, truncated sum, discounted sum). Our work extends to the quantitative case the multi-objective model checking problem studied by Etessami et al. in unweighted MDPs.

15:04 15:16 Quentin Hautem Heterogeneous multi-dimensional quantitative games
speaker: Quentin Hautem

Abstract

  

In most system design problems, there is no unique objective to be op- timized, but multiple, potentially conflicting objectives. For example, in designing a controller, one is interested not only in minimizing the aver- age response time of the system but also in minimizing its average power consumption. Recently, in [CDHR10], multi-objective generalizations of mean-payoff and energy objectives have been studied. Nevertheless, in this work the multi-dimensionality is homogeneous in the sense that each dimension is measured with the same function: either the mean-payoff measure is used for all the dimensions, or the energy measure is used for all the dimensions. In our work, we want instead to consider the more ambitious goal of considering heterogeneous multi-dimensional quantitative games: we want to allow the use of different measures in the multiple quantitative dimensions. For example, we would like to use the energy measure (to record the energy consumption of the system) for one dimension and the mean-payoff measure for another dimension (to measure the mean response time of the system for example). The kind of questions that we try to solve are the following ones. Can we decide whether the system is able to achieve its objective from its initial configuration against any behavior of the environment? In case of positive answer, can we construct an appropriate strategy for the system to reach this goal? Can we optimize the parameters of such a winning strategy (size of required memory, quality of satisfaction of the objective, etc). For all these questions we are also interested in the computational complexities. Games that we here consider are zero-sum turn-based games played on a finite multi-dimensional weighted graph. Given a measure and a threshold (in Z) for each dimension, the objective of player 1 is the set of plays such that, for every dimension, the measure of the play (on the considered dimension) is greater or equal to the corresponding threshold. Since we consider heterogeneous multi-dimensional quantitative games, we allow the use of a different measure for each dimension.

Firstly, we study games with ω-regular objectives in {inf, sup, liminf, limsup}. We prove that the decision problem for these games is PSPACE- complete, and that finite-memory winning strategies are sufficient for both players. Moreover, we get several refinements (on the number of occurrence of each kind of objective) saying when the problem becomes P-complete and when memory requirements can be improved. This is a first step in order to mix ω-regular objectives with one that is not (such as mean-payoff and energy), and more generally with several ones that are not ω-regular objectives. Secondly, we consider an additional ω-regular objective, the window-mean-payoff (WMP) introduced in [CDRR13] which is a conservative approximation of the mean-payoff objective considered over a local finite window sliding along a play, instead of the whole play. Adding this objective to {inf, sup, liminf, limsup} leads to an EXPTIME-complete (in- stead of PSPACE-complete) decision problem but still with finite-memory strategies for both players. We also study in which cases we can get a better complexity and better memory requirements. Finally, the value problem for one-dimensional WMP-games was not studied in [CDRR13], and we prove that it can be solved in polynomial time. Those results are joint work with Bruyère and Raskin.

References [CDHR10] Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-Fran ̧cois Raskin. Generalized mean-payoff and energy games. In IARCS Annual Conference on Foundations of Soft- ware Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, pages 505–516, 2010. [CDRR13] Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-Franc ̧ois Raskin. Looking at mean-payoff and total-payoff through windows. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, pages 118– 132, 2013.

15:16 15:28 Jan Krcal Distributed Synthesis in Continuous Time
speaker: Jan Krcal

Abstract

  

We introduce a formalism modelling communication of distributed agents strictly in continuous-time. Within this framework, we study the problem of synthesizing local strategies for individual agents such that a specified set of goal states is reached, or reached with at least a given probability. The flow of time is modelled explicitly based on continuous-time randomness, with two natural implications: First, the non-determinism stemming from interleaving disappears. Second, when we restrict to a subclass of non-urgent models, both the qualitative and quantitative reachability problem can be solved in EXPTIME. The crucial observation is that explicit continuous time enables the players to communicate their states by delaying synchronization. In general, the quantitative problem is undecidable for two or more players and the qualitative problem is EXPTIME-hard for two players and undecidable for three or more players. The qualitative undecidability is shown by a reduction to decentralized POMDPs for which we provide the strongest (and rather surprising) undecidability result so far.

15:28 15:40 Matthew Hague Detecting Redundant CSS Rules in HTML5 Applications: A Tree Rewriting Approach
speaker: Matthew Hague

Abstract

  

HTML5 applications normally have a large set of CSS (Cascading Style Sheets) rules for data display. As web applications evolve, maintaining CSS files can easily become problematic. Some rules will be replaced by new ones, but these obsolete (hence redundant) rules often remain in the applications. This ``bloats'' the applications, requires more bandwidth, and increases browser processing time. Most works on detecting redundant CSS rules do not consider the dynamic behaviors of HTML5 (specified in JavaScript); in fact, the only proposed method that takes these into account is dynamic analysis, which cannot soundly prove redundancy of CSS rules. We introduce an abstraction of HTML5 applications based on monotonic tree-rewriting and study its ``redundancy problem''. We establish the precise complexity of the problem and various subproblems of practical importance (ranging from P to EXP). In particular, our algorithm relies on an efficient reduction to an analysis of symbolic pushdown systems (for which highly optimised solvers are available), which yields a fast method for checking redundancy in practice. We implemented our algorithm and demonstrated its efficacy in detecting redundant CSS rules in HTML5 applications.

This is joint work with Anthony Lin and C.-H. Luke Ong.

15:40 16:00 Break
16:00 17:00 Invited talk
16:00 17:00 Moshe Vardi The SAT Revolution: Solving, Sampling, and Counting
speaker: Moshe Vardi

Abstract

  

For the past 40 years computer scientists generally believed that NP-complete problems are intractable. In particular, Boolean satisfiability (SAT), asparadigmatic NP-complete problem, has been considered to be intractable. Over the past 20 years, however, there has been a quiet, but dramatic, revolution, and very large SAT instances are now being solved routinely as part of software and hardware design.

In this talk I will review this amazing development and show that we can leverage SAT solving to accomplish other Boolean reasoning tasks. Counting the the number of satisfying truth assignments of a given Boolean formula or sampling such assignments uniformly at random are fundamental computational problems in computer science with numerous applications. While the theory of these problems has been thoroughly investigated in the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances. Algorithms used by the industry offer better scalability, but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and Satisfiability Modulo Theory, that scales to formulas with hundreds of thousands of variable without giving up correctness guarantees.

17:00 18:00 Break
18:00 20:00 (?) Dinner

Thursday 17 September (T1 Lecture room, Suchdol)

08:30 09:30 Invited talk
08:30 09:30 Christel Baier TBA
speaker: Christel Baier

Abstract

  

TBA

09:30 09:40 Break
09:40 11:04 Session 3
09:40 09:52 Ismaël Jecker Multi-Sequential Word Relations
speaker: Ismaël Jecker

Abstract

  

Rational relations are binary relations of finite words that are realised by non-deterministic finite state transducers (NFT). A particular kind of rational relations is the sequential functions. Sequential functions are the functions that can be realised by input-deterministic transducers. Some rational functions are not sequential. However, based on a property on transducers, called the twinning property, it is decidable in PTime whether a rational function given by an NFT is sequential. In this paper, we investigate the generalisation of this result to multi-sequential relations, i.e. relations that are equal to a finite union of sequential functions. We show that given an NFT, it is decidable in PTime whether the relation it defines is multi-sequential, based on a property called the fork property. If the fork property is not satisfied, we give a procedure that effectively constructs a finite set of input-deterministic transducers whose union defines the relation. This procedure generalises to arbitrary NFT the determinisation procedure of functional NFT.

09:52 10:04 Frederic Reinhardt Advice Automatic Structures and Uniformly Automatic Classes
speaker: Frederic Reinhardt

Abstract

  

We study structures that are automatic with advice. Building on advice automata we introduce the concept of a parameterised automatic presentation as a means to uniformly represent a class of finite or infinite structures with a regular set of advices. We give a characterisation of the advice automatic countable Boolean algebras and give upper bounds on the complexity of presentable structures for several algebraic classes like semigroups, groups, and integral domains generalising results for ordinary automatic structures. On the positive side we give, among others, parameterised automatic presentations for the class of torsion-free abelian groups of rank 1, the class of all finite abelian groups and the class of all groups having a product decomposition with non-abelian factors of bounded size. Furthermore we apply our results to show that model-checking for first-order logic becomes fixed-parameter tractable on the class of finite abelian groups and the class of all finite groups.

This is joint work with Faried Abu Zaid and Erich Grädel (RWTH Aachen)

10:04 10:16 Nathanaël Fijalkow Substantiating Rabin's Claim about the Dynamic Complexity of Probabilistic Languages
speaker: Nathanaël Fijalkow

Abstract

  

In his seminal paper introducing probabilistic automata in 1963, Rabin defined a computational question that we call the dynamic complexity problem. He studied the dynamic complexity of a subclass of probabilistic automata, and made a claim about the general class of probabilistic automata. Roughly speaking, the claim is that they have a high dynamic complexity, and an example achieving this is attributed to R. E. Stearns, without bibliographical references.

In this work, we follow Rabin's ideas and define the dynamic complexity problem in general, i.e. for all languages. Our first step is then to substantiate Rabin's claim: we prove that indeed, probabilistic automata have the highest possible dynamic complexity.

10:16 10:28 Michaël Cadilhac A Circuit Complexity Approach to Transductions
speaker: Michaël Cadilhac

Abstract

  

Low circuit complexity classes and regular languages exhibit very tight interactions that shade light on their respective expressiveness. We propose to study these interactions at a functional level, by investigating the deterministic rational transductions computable by constant-depth, polysize circuits. To this end, a circuit framework of independent interest that allows variable output length is introduced. Relying on it, there is a general characterization of the set of transductions realizable by circuits. It is then decidable whether a transduction is definable in AC^0 and, assuming a well-established conjecture, the same for ACC^0.

10:28 10:40 Emmanuel Filiot Decision Problems of Tree Transducers with Origin
speaker: Emmanuel Filiot

Abstract

  

A tree transducer with origin translates an input tree into a pair of output tree and origin info. The origin info maps each node in the output tree to the unique input node that created it. In this way, the implementation of the transducer becomes part of its semantics. We show that the landscape of decidable properties changes drastically when origin info is added. For instance, equivalence of nondeterministic top-down and MSO transducers with origin is decidable. Both problems are undecidable without origin. The equivalence of deterministic top-down tree-to-string transducers is decidable with origin, while without origin it is a long standing open problem. With origin, we can decide if a deterministic macro tree transducer can be realized by a deterministic top-down tree transducer; without origin this is an open problem.

10:40 10:52 Nathan Lhote Towards an algebraic characterization of rational word functions
speaker: Nathan Lhote

Abstract

  

In formal language theory, several different models characterize regular languages, such as finite automata, congruences of finite index, or monadic second-order logic (MSO). Moreover, several fragments of MSO have effective characterizations based on algebraic properties. When we consider transducers instead of automata, such characterizations are much more challenging, because many of the properties of regular languages do not generalize to regular word functions.

In this paper we consider word functions that are definable by one-way transducers (rational functions). We show that the canonical bimachine of Reutenauer and Schützenberger preserves certain algebraic properties of rational functions, similar to the case of word languages. In particular, we give an effective characterization of functions that can be defined by an aperiodic one-way transducer.

10:52 11:04 Matteo Mio Regular sets of Trees and Probablity
speaker: Matteo Mio

Abstract

  

T. Gogacz, H. Michalewski, M. Mio, M. Skrzypczak, "Measure Properties of Game Tree Languages", proc. of MFCS 2014.

2) Regular sets of trees are closed under "small/large projection" with Baire-category interpretation. This implies decidability of the finite-SAT problem of probabilistic logics such as qualitative pCTL*.

H. Michalewski, M. Mio, "Baire Category Quantifier in Monadic Second Order Logic", proc. of ICALP 2015.

3) The problem of computing the probability (i.e., coin-flipping measure) of regular sets of trees definable by game automata is decidable.

not yet published.

11:04 11:30 Coffee Break
11:30 12:54 Session 4
11:30 11:42 Guillermo Perez Minimizing Regret in Quantitative Games
speaker: Guillermo Perez

Abstract

  

Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies. We also establish relations between the latter version and other problems studied in the literature.

11:42 11:54 Massimo Benerecetti Solving Parity Games via Priority Promotion
speaker: Massimo Benerecetti

Abstract

  

The main contribution of the paper is a new family of algorithms for solving parity games, based on the notions of region and priority promotion. A region R for a given player is a set of vertices from each of which the player can enforce a winning play that never leaves the region, unless either the opponent can escape from R or the only choice for player itself is to exit from R (i.e. no edge from a vertex of remains in R). Therefore, a region is essentially a weaker form of winning region. Regions can be ordered by assigning to each of them a priority corresponding to the "best" priority the opponent can obtain along a play exiting from that region. An important property of regions is that, under suitable and easy to check assumptions, a higher priority region R1 and a lower priority region R2, with priorities p1 and p2, respectively, of the same parity, can be merged into a single region of the higher priority p1. We call this merging operation a priority promotion for R2. The underlying idea of the approach is then to iteratively enlarge regions by performing suitable sequences of promotions, until a closed -region, namely a region where player can force the game to remain, is obtained. When that happens, a winning region for has been found. Experimental results, comparing the new algorithms with the state of the art solvers, also show that all three algorithms perform very well in practice, most often significantly better than existing ones, on both random games and benchmark families proposed in the literature.

11:54 12:06 Dietmar Berwanger New decidable classes for distributed strategy synthesis
speaker: Dietmar Berwanger

Abstract

  

Infinite games with imperfect information tend to be undecidable unless the information flow is severely restricted. One fundamental decidable case occurs when there is a total ordering among players, such that each player has access to all the information that the following ones receive.

In this talk, we present two information patterns that lead to new decidable classes for which the distributed synthesis problem is solvable with finite-state strategies. One generalises the hierarchical principle by allowing information hierarchies to change along the play, and by admitting transient phases without hierarchical information. The second pattern is orthogonal, it asserts that players attain common knowledge about the actual state of the game over and over again along every play.

Joint work with Anup Basil Mathew and Marie van den Bogaard.

http://lsv.fr/~dwb/rec.pdf
http://lsv.fr/~dwb/hi.pdf

12:06 12:18 Branislav Bosansky Commitments to Correlated Strategies in Finite Sequential Games
speaker: Branislav Bosansky

Abstract

  

12:18 12:30 Stephane Le Roux Infinite subgame perfect equilibrium in the Hausdorff difference hierarchy
speaker: Stephane Le Roux

Abstract

  

Subgame perfect equilibria are specific Nash equilibria in perfect information games in extensive form. They are important because they relate to the rationality of the players. They always exist in infinite games with continuous real-valued payoffs, but may fail to exist even in simple games with slightly discontinuous payoffs. This article considers only games whose outcome functions are measurable in the Hausdorff difference hierarchy of the open sets (i.e. Delta^0_2 when in the Baire space), and it characterizes the families of linear preferences such that every game using these preferences has a subgame perfect equilibrium: the preferences without infinite ascending chains (of course), and such that for all players a and b and outcomes x,y,z we have not (z <_a y <_a x and x <_b z <_b y). Moreover at each node of the game, the equilibrium constructed for the proof is Pareto-optimal among all the outcomes occurring in the subgame. Additional results for non-linear preferences are presented.

12:30 12:42 Felix Klein How Much Lookahead is Needed to Win Infinite Games?
speaker: Felix Klein

Abstract

  

Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. For omega-regular winning conditions it is known that such games can be solved in doubly-exponential time and that doubly-exponential lookahead is sufficient.

We improve upon both results by giving an exponential time algorithm and an exponential upper bound on the necessary lookahead. This is complemented by showing EXPTIME-hardness of the solution problem and tight exponential lower bounds on the lookahead. Both lower bounds already hold for safety conditions. Furthermore, solving delay games with reachability conditions is shown to be PSPACE-complete.

12:42 12:54 Martin Zimmermann Delay Games with WMSO+U Winning Conditions
speaker: Martin Zimmermann

Abstract

  

Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. We consider delay games with winning conditions expressed in weak monadic second order logic with the unbounding quantifier, which is able to express (un)boundedness properties.

We show that it is decidable whether the delaying player has a winning strategy using bounded lookahead and give a doubly-exponential upper bound on the necessary lookahead. In contrast, we show that bounded lookahead is not always sufficient to win such a game.

12:54 14:30 Lunch
14:30 15:30 Invited talk
14:30 15:30 Philippe Schnoebelen TBA
speaker: Philippe Schnoebelen

Abstract

  

TBA

15:30 15:40 Break
15:40 17:04 Session 5
15:40 15:52 Ranko Lazic Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time
speaker: Ranko Lazic

Abstract

  

We generalise the hyperplane separation technique (Chatterjee and Velner, 2013) from multi-dimensional mean-payoff to energy games, and achieve an algorithm for solving the latter whose running time is exponential only in the dimension, but not in the number of vertices of the game graph. This answers an open question whether energy games with arbitrary initial credit can be solved in pseudo-polynomial time for fixed dimensions 3 or larger (Chaloupka, 2013). It also improves the complexity of solving multi-dimensional energy games with given initial credit from non-elementary (Brazdil, Jancar, and Kucera, 2010) to 2EXPTIME, thus establishing their 2EXPTIME-completeness.

Joint work with Marcin Jurdzinski and Sylvain Schmitz. Extended abstract to appear in ICALP 2015, long version available at http://arxiv.org/abs/1502.06875.

15:52 16:04 Patrick Totzke Contex-Free Controlled Vector Addition Systems
speaker: Patrick Totzke

Abstract

  

I propose to present recent and ongoing work on Pushdown VASS, that ex- tend Vector Addition Systems with a stack. What can be modelled with these systems? What are interesting open problems and how to attack them?

In [4] we discussed an equivalent formalism, which amounts to VASS that allow only runs from a context-free control language, similar to the regulated rewriting setting [1]. Reachability problems like coverability and boundedness can then be attacked by analysing annotated derivation trees of a GfG. This not only helps to simplify proofs but also to address slightly more general problems. This is joint work with Jerome Leroux and Gregoire Sutre.

16:04 16:16 Paul Hunter Reachability in succinct one-counter games
speaker: Paul Hunter

Abstract

  

We consider two-player games with reachability objectives played on transition systems of succinct one-counter machines, that is, machines where the counter is incremented or decremented by a value given in binary.

We show that the reachability and counter reachability problems are equivalent, in contrast to non-succinct games and that all problems are EXPSPACE-complete.

16:16 16:28 Petr Novotný Long-Run Average Behaviour of Probabilistic Vector Addition Systems
speaker: Petr Novotný

Abstract

  

We study long-run behaviour of probabilistic Vector Addition Systems with States (pVASS) with at most two counters. We show that for one-dimensional pVASS and a broad class of two-dimensional pVASS we are able to compute, up to an arbitrary precision, certain natural characterization of all possible long-run behaviours of a given model. We also show that pVASS with three counters may exhibit unexpected phenomena that make their analysis much more difficult. To obtain our results we use an interesting combination of several deep results from the literature together with non-trivial insights into the behaviour of pVASS. As a byproduct of our study, we discover counterexamples falsifying some classical results about stochastic Petri nets published in the~80s.

16:28 16:40 Lorenzo Clemente Reachability analysis of first-order definable pushdown systems
speaker: Lorenzo Clemente

Abstract

  

We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are first-order definable in a fixed countably-infinite structure. We show that the reachability analysis can be addressed with the well-known saturation technique for the wide class of oligomorphic structures. Moreover, for the more restrictive homogeneous structures, we are able to give concrete complexity upper bounds. We show ample applicability of our technique by presenting several concrete examples of homogeneous structures, subsuming, with optimal complexity, known results from the literature. We show that infinitely many such examples of homogeneous structures can be obtained with the classical wreath product construction. This is joint work with Sławomir Lasota, from the University of Warsaw.

16:40 16:52 Petr Jancar Normed BPA processes as a rational monoid w.r.t. branching bisimilarity
speaker: Petr Jancar

Abstract

  

The proposed talk would aim to highlight why finite transducers are a natural device for deciding branching bisimilarity on normed BPA processes. There has been a recent revival of the research interest in this intriguing equivalence on infinite-state systems, and the proposed talk is based on the paper "Branching Bisimilarity of Normed BPA Processes is in NEXPTIME" by Wojciech Czerwinski and Petr Jancar that has been accepted to LiCS 2015. In this connection it is appropriate to mention that there is the paper "Branching Bisimilarity on Normed BPA Is EXPTIME-complete" by Chaodong He and Mingzhang Huang that has been also accepted to LiCS 2015.

16:52 17:04 Sławomir Lasota Timed pushdown automata revisited
speaker: Sławomir Lasota

Abstract

  

We prove two results on timed extensions of pushdown automata (PDA). As our first result we prove that the model of dense-timed PDA of Abdulla et al. collapses: it is expressively equivalent to dense-timed PDA with timeless stack. Motivated by this result, we advocate the framework of first-order definable PDA, a specialization of PDA in sets with atoms, as the right setting to define and investigate timed extensions of PDA. The general model obtained in this way is Turing complete. As our second result we prove NEXPTIME upper complexity bound for the non-emptiness problem for an expressive subclass. As a byproduct, we obtain a tight EXPTIME complexity bound for a more restrictive subclass of PDA with timeless stack, thus subsuming the complexity bound known for dense-timed PDA.

This is a joint work with with Lorenzo Clemente from University of Warsaw.

17:04 17:15 Break
17:15 18:39 Session 6
17:15 17:27 Michael Vanden Boom Interpolation with Decidable Fixpoint Logics
speaker: Michael Vanden Boom

Abstract

  

A logic satisfies Craig interpolation if whenever one formula phi_1 in the logic entails another formula phi_2 in the logic, there is an intermediate formula in the logic --- one entailed by phi_1 and entailing phi_2 --- using only relations in the common signature of phi_1 and phi_2. Uniform interpolation strengthens this by requiring the interpolant to depend only on phi_1 and the common signature. A uniform interpolant can thus be thought of as a minimal upper approximation of a formula within a subsignature. For first-order logic, interpolation holds but uniform interpolation fails. Uniform interpolation is known to hold for several modal and description logics, but little is known about uniform interpolation for fragments of predicate logic over relations with arbitrary arity. Further, little is known about ordinary Craig interpolation for logics over relations of arbitrary arity that have a recursion mechanism, such as fixpoint logics.

In recent joint work with Michael Benedikt and Balder ten Cate (to appear in LICS'15), we have taken a step towards filling these gaps, proving interpolation for a decidable fragment of least fixpoint logic called unary negation fixpoint logic (UNFP). UNFP restricts least fixpoint logic by only allowing monadic fixpoint predicates and the negation of formulas with at most one free variable. This leads to decidable satisfiability and many other nice properties, include the tree-like model property.

To prove interpolation for UNFP, we show that for any fixed k, uniform interpolation holds for the k-variable fragment of the logic. In order to show this we develop the technique of reducing questions about logics with tree-like models to questions about modal logics, following an approach by Graedel, Hirsch, and Otto. While this technique has been applied to expressivity and satisfiability questions before, we show how to extend it to reduce interpolation questions about such logics to interpolation for the modal mu-calculus.

17:27 17:39 Giovanna D'Agostino Interpolation for the Alternation Free Fragment of the Mu-Calculus
speaker: Giovanna D'Agostino

Abstract

  

We discuss the problem of interpolation in the alternation levels of the mu-Calculus. In particular, we consider interpolation and uniform interpolation for the alternation free fragment.

17:39 17:51 Frank Valencia An Algebraic View of Space/Belief and Extrusion/Utterance for Concurrency/Epistemic Logic
speaker: Frank Valencia

Abstract

  

In this talk I shall introduce a family of algebraic structures to express and reason about spatial concepts such as locality, globality and mobility (extrusion) as well as epistemic phenomena such as beliefs, objectivity, subjectivity, utterances, lies and opinions. The structures can be seen as complete Heyting algebras equipped with operators to account for spatial and epistemic specifications.

17:51 18:03 Boris Duedder Modal Logic and Staged Computation
speaker: Boris Duedder

Abstract

  

In our talk we will discuss connections between modal logics (Gödels' S4 and K4) via modal type systems (intuitionistic logic) and computational models for code generation. The computational interpretation in lambda([],->) of axioms of S4 and K4 lead to interesting insights. For example, the interpretation of the modal axiom K, [](t->s)->([]t->[]s), is a function that takes code of a function from domain t to range s and returns a function that maps code of t to code of s. Regarding the system as staged gives the following interpretation of K: Ks argument is a function within an implementation language that is different from functions over boxes. By introducing ->_[] as a function operator on implementation languages, axiom K can be rewritten as [](t->_[] s)\to ([]t->[]s)$. Now axiom K maps code of functions in implementation languages to functions operating on code. Especially, if [] forms a homomorphism, $[](t->_[] s)=[]t->[]s, then the [] can be used to inject a function application ->_[] into an implement language. We provide examples and applications for this idea.

18:03 18:15 Szabolcs Ivan Algebraic characterization of temporal logics on forests
speaker: Szabolcs Ivan

Abstract

  

We associate a temporal logic $\mathrm{FL}(\cL)$ to class $\cL$ of (regular) forest languages where a forest is an ordered finite sum of finite unranked trees. Under a natural assumption of the set $\cL$ of modalities we derive an algebraic characterization of the forest languages definable in $\mathrm{FL}(\cL)$, in terms of the iterated ``Moore product'' of forest automata. Using this characterization we derive a polynomial-time algorithm to decide definability of the fragment $\mathrm{EF}^*$ of $\mathrm{CTL}$, evaluated on forests.

18:15 18:27 Filip Mazowiecki Maximal partition logic: towards a logical characterization of copyless cost register automata
speaker: Filip Mazowiecki

Abstract

  

It is desirable for a computational model to have a logic characterization like in the seminal work from Buchi that connects MSO with finite automata. For example, weighted automata are the quantitative extension of finite automata for computing functions over words and they can be naturally characterized by a fragment of weighted logic introduced by Droste and Gastin. Recently, cost register automata (CRA) were introduced by Alur et al. as an alternative model for weighted automata. In hope of finding decidable subclasses of weighted automata, they proposed to restrict their model with the so-called copyless restriction. Unfortunately, copyless CRA do not enjoy good closure properties and, therefore, a logical characterization of this class seems to be unlikely.

We introduce a new logic called maximal partition logic (MP) for studying the expressiveness of copyless CRA. In contrast from the previous approaches (i.e. weighted logics), MP is based on a new set of regular quantifiers that partition a word into maximal subwords, compute the output of a subformula over each subword separately, and then aggregate these outputs with a semiring operation. We study the expressiveness of MP and compare it with weighted logics. Furthermore, we show that MP is equally expressive to a natural subclass of copyless CRA. This shows the first logical characterization of copyless CRA and it gives a better understanding of the copyless restriction in weighted automata.

This is joint work with Cristian Riveros.

18:27 18:39 Bastien Maubert Relating paths in transition systems: the fall of the modal mu-calculus
speaker: Bastien Maubert

Abstract

  

We revisit Janin and Walukiewicz’s classic result on the expressive completeness of the modal mu-calculus w.r.t. MSO, when transition systems are equipped with a binary relation over paths. We obtain two natural extensions of MSO and the mu-calculus: MSO with path relation and the jumping mu-calculus. While “bounded-memory” binary relations bring about no extra expressivity to either of the two logics, “unbounded-memory” binary relations make the bisimulation-invariant fragment of MSO with path relation more expressive than the jumping mu-calculus: the existence of winning strategies in games with imperfect-information inhabits the gap.

Friday 18 September (EI and EII Lecture rooms, Suchdol)

08:30 09:54 Session 7A (EI Lecture room)
08:30 08:42 Wojciech Czerwiński The (Almost) Complete Guide to Tree Pattern Containment
speaker: Wojciech Czerwiński

Abstract

  

Tree pattern queries are being investigated in database theory for more than a decade. They are a fundamental and flexible query mechanism and have been considered in the context of querying tree structured as well as graph structured data. We revisit their containment, validity, and satisfiability problem, both with and without schema information. We present a comprehensive overview of what is known about the complexity of containment and develop new techniques which allow us to obtain tractability and hardness results for cases that have been open since the early work on tree pattern containment. For the tree pattern queries we consider in this paper, it is known that the containment problem does not depend on whether patterns are evaluated on trees or on graphs. This means that our results also shed new light on tree pattern queries on graphs.

08:42 08:54 Vojtech Forejt On Frequency LTL in Probabilistic Systems
speaker: Vojtech Forejt

Abstract

  

We study frequency linear-time temporal logic (fLTL) which extends the linear-time temporal logic (LTL) with a path operator $\Gf{p}$ expressing that on a path, certain formula holds with at least a given frequency $p$, thus relaxing the semantics of the usual $\mathbf{G}$ operator of LTL. Such logic is particularly useful in probabilistic systems, where some undesirable events such as random failures may occur and are acceptable if they are rare enough. Frequency-related extensions of LTL have been previously studied by several authors, where mostly the logic is equipped with an extended ``until'' and ``globally'' operator, leading to undecidability of most interesting problems.

For the variant we study, we are able to establish fundamental decidability results. We show that for Markov chains, the problem of computing the probability with which a given fLTL formula holds has the same complexity as the analogous problem for LTL. We also show that for Markov decision processes the problem becomes more delicate, but when restricting the frequency bound $p$ to be 1 and negations not to be outside any $\mathbf{G}^p$ operator, we can compute the maximum probability of satisfying the fLTL formula. This can be again performed with the same time complexity as for the ordinary LTL formulas.

08:54 09:06 Markus Latte Definability by Weakly Deterministic Regular Expressions with Counters is Decidable
speaker: Markus Latte

Abstract

  

We show that weakly deterministic regular expressions with counters (WDREs) -- as they are used in XML Schema -- are at most exponentially larger than equivalent DFAs. As a consequence, the problem, whether a given DFA is equivalent to any WDRE, is decidable in EXPSPACE.

The underlying paper is accepted for MFCS2015. A preprint is available at http://www.theoinf.uni-bayreuth.de/download/mfcs15-appendix.pdf

09:06 09:18 Tomasz Gogacz The Hunt for a Red Spider: Conjunctive Query Determinacy Is Undecidable.
speaker: Tomasz Gogacz

Abstract

  

We solve an open problem in relational databases theory, showing that the conjunctive query determinacy problem is undecidable.

09:18 09:30 Gaetano Geck Parallel-Correctness and Transferability for Conjunctive Queries
speaker: Gaetano Geck

Abstract

  

In traditional database systems, the complexity of query processing for large datasets is mainly determined by the number of IO requests to external memory. A factor dominating complexity in modern massively distributed database systems, however, is the number of communication steps. Motivated by recent in-memory systems like Spark and Shark, Koutris and Suciu introduced the massively parallel communication model (MPC) where computation proceeds in a sequence of parallel steps each followed by global synchronization of all servers. In this model, evaluation of conjunctive queries and skyline queries has been considered.

Of particular interest in the MPC model are the queries that can be evaluated in one round of communication. To this end, data is first redistributed among the nodes, according to some distribution policy, and then each node computes a partial result on its own.

We considered the correctness of this particular evaluation algorithm: a query Q is parallel-correct for a given distribution policy P, if for any instance I, the evaluation of Q(I) equals the union of the evaluation of Q on the nodes' local instances as induced by P.

We studied the complexity of deciding parallel-correctness. For various representations of distribution policies, we obtained an upper bound of \Pi^p_2. For a simple (explicit) representation, we could also provide a matching lower bound via a reduction from \Pi_2-QBF. One-round evaluation algorithms redistribute data for the evaluation of every query. In an attempt to minimize the amount of necessary communication, it is natural to also consider parallel-correctness transfer from a query Q to another query Q', i.e. when Q' is parallel-correct under every distribution policy that Q is parallel-correct under. Again, we studied the complexity of deciding parallel-correctness transfer from Q to Q' and obtained an upper bound of \Pi^p_3. Also, we obtained a matching lower bound via a reduction from \Pi_3-QBF. We note that the evaluation algorithm on which our results are based, is---for a specific family of distribution policies---well-known as the hypercube algorithm.

09:30 09:42 Thomas Zeume Reachability is in DynFO
speaker: Thomas Zeume

Abstract

  

A dynamic program, as introduced by Dong, Su Topor (1993) and Pat- naik and Immerman (1994), maintains a fixed query for an input database which is subject to tuple insertions and deletions. It can use an auxiliary database whose relations are updated via first-order formulas upon modi- fications of the input database. In this talk I will present how Reachability in directed graphs can be maintained in this fashion. This result confirms a two decade old conjecture of Patnaik and Immerman (1997).

The talk is based on joint work with Samir Datta, Raghav Kulkarni, Anish Mukherjee and Thomas Schwentick.

09:42 09:54 Joanna Ochremiak Algebraic Necessary Condition for Tractability of Valued CSP
speaker: Joanna Ochremiak

Abstract

  

Many natural optimisation problems are expressible as Valued Constraint Satisfaction Problems (VCSPs). Examples include: Max-Cut, Minimum Vertex Cover, Max-3-Sat.

We present an algebraic framework for VCSPs, generalising the algebraic framework for its decision version (CSPs) provided by Bulatov et al. We formulate an Algebraic VCSP Dichotomy Conjecture, which says that each valued constraint language gives rise to an optimisation problem solvable in PTime, or to an NP-hard one. It also proposes a criterion to distinguish those two cases. We prove the hardness direction, establishing a necessary algebraic condition for tractability of VCSPs with fixed constraint languages.

This is joint work with Marcin Kozik.

08:30 09:54 Session 7B (EII Lecture room)
08:30 08:42 Guilhem Jaber A Categorical Equivalence between Trace and Game Semantics
speaker: Guilhem Jaber

Abstract

  

In this talk, we present a formal correspondence between Laird's trace semantics and the nominal game model of Murawski and Tzevelekos for \textrm{RefML}, a call-by-value language with higher-order references.

To do so, we put a categorical structure on the trace model, where the denotation of terms is normally computed via a labeled transition systems. Then, we build a functor between the trace models equipped with this structure, and the game model.

08:42 08:54 C. Aiswarya Maintaining Latest Information beyond Channel Bounds
speaker: C. Aiswarya

Abstract

  

Consider distributed systems consisting of a number of processes communicating with each other asynchronously by sending messages via FIFO channels. It is crucial for such systems that every process can maintain deterministically the latest information about other processes. To do so, any process $p$, upon receiving a message from a process $q$, should determine for every process $r$, whether the latest event on $r$ that $p$ knows of is more recent than the latest event on $r$ that $q$ knows of. Solving this problem, while storing and exchanging only a bounded amount of information, is extremely challenging and not always possible. This is known as the gossip problem. A solution to this is the key to solving numerous important problems on distributed systems. So far, gossip has been solved only for channel bounded systems. We solve the gossip problem for a much richer class, going beyond a priori channel bounds.

Joint work with Paul Gastin (LSV, ENS Cachan, France) and K. Narayan Kumar (Chennai Mathematical Institute, India).

08:54 09:06 Vahid Hashemi Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs
speaker: Vahid Hashemi

Abstract

  

Verification of PCTL properties of MDPs with convex uncertainties has been investigated recently by Puggelli et al. However, model checking algorithms typically suffer from state space explosion. In this paper, we address probabilistic bisimulation to reduce the size of such an MDPs while preserving PCTL properties it satisfies. We discuss different interpretations of uncertainty in the models which are studied in the literature and that result in two different definitions of bisimulations. We give algorithms to compute the quotients of these bisimulations in time polynomial in the size of the model and exponential in the uncertain branching. Finally, we show by a case study that large models in practice can have small branching and that a substantial state space reduction can be achieved by our approach.

09:06 09:18 Florian Zuleger Liveness of Parameterized Timed Networks
speaker: Florian Zuleger

Abstract

  

We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decidable with respect to specifications given by B- or S-automata. Such specifications are very expressive (they strictly subsume omega-regular specifications), and easily express complex liveness and safety properties. Our results are obtained by modeling the passage of time using symmetric broadcast, and by solving the model checking problem of parameterized systems of (un-timed) processes communicating using k-wise rendezvous and symmetric broadcast. Our decidability proof makes use of automata theory, rational linear programming, and geometric reasoning for solving certain reachability questions in vector addition systems; we believe these proof techniques will be useful in solving related problems.

09:18 09:30 Lubos Korenciak Optimizing Performance of Continuous-Time Stochastic Systems using Timeout Synthesis
speaker: Lubos Korenciak

Abstract

  

We consider parametric version of fixed-delay continuous-time Markov chains (or equivalently deterministic and stochastic Petri nets, DSPN) where fixed- delay transitions are specified by parameters, rather than concrete values. Our goal is to synthesize values of these parameters that, for a given cost function, minimize expected total cost incurred before reaching a given set of target states. We show that under mild assumptions, optimal values of parameters can be effectively approximated using translation to a Markov decision process (MDP) whose actions correspond to discretized values of these parameters. To this end we identify and overcome several interesting phenomena arising in systems with fixed delays.

09:30 09:42 Karin Quaas The Language Inclusion Problem for Timed Automata extended with Pushdown Stack and Counters
speaker: Karin Quaas

Abstract

  

We study decidability of verication problems for timed automata extended with a pushdown stack or discrete counters. In this way, we obtain a strong model that may for instance be used to model real-time programs with procedure calls. It is long known that the reachability problem for this model is decidable. The goal of this work is to investigate the language inclusion problem and related problems for this class of automata and over finite timed words. On the negative side, we prove that the language inclusion problem is undecidable for the case that A is a pushdown timed automaton and B is a one-clock timed automaton. This is even the case if A is a deterministic instance of a very restricted subclass of timed pushdown automata called timed visibly one-counter nets. On the positive side, we prove that the language inclusion problem is decidable if A is a timed automaton and B is a timed automaton extended with a finite set of counters that can be incremented and decremented, and which we call timed counter nets. As a special case, we obtain the decidability of the universality problem for timed counter nets: given a timed automaton A with input alphabet $\Sigma$, does L(A) accept the set of all timed words over $\Sigma$? Finally, we give the precise decidability border for the universality problem by proving that the universality problem is undecidable for the class of timed visibly one-counter automata.

09:42 09:54 Jan Strejcek The Hanoi Omega-Automata Format
speaker: Jan Strejcek

Abstract

  

We propose a succinct, human-readable, flexible, and extensible exchange format for omega-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people's work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin.

09:54 10:20 Coffee Break
10:20 11:20 Session 8A (EI Lecture room)
10:20 10:32 Jakub Michaliszyn Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions
speaker: Jakub Michaliszyn

Abstract

  

We put forward a specification language based on epistemic logic and a variant of the logic ATL interpreted on a three-valued semantics. We show that the model checking problem for multi-agent systems in this setting is tractable by giving a provably correct procedure which admits a PTime bound. We give a constructive technique for generating abstract approximations of concrete multiagent systems models and show that the truth values are preserved between abstract and concrete models.

The talk will summarise the main results from A. Lomuscio and J. Michaliszyn. An abstraction technique for the verification of multi-agent systems against ATL specifications. In Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR14), pages 428–437. AAAI Press, 2014. A. Lomuscio and J. Michaliszyn. Verifying multi-agent systems by model checking three-valued abstractions. In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems (AAMAS15), pages 189–198, 2015.

10:32 10:44 Giuseppe Perelli Pushdown Multi-Agent System Verification
speaker: Giuseppe Perelli

Abstract

  

In this paper we investigate the model-checking problem of pushdown multi-agent systems for ATL* specifications. To this aim, we introduce pushdown game structures over ATL* formulas are interpreted. We show an algorithm that solves the addressed model-checking problem in 3ExpTime. We also provide a 2ExpSpace lower bound by showing a reduction from the word acceptance problem for deterministic Turing machines with doubly exponential space.

10:44 10:56 Alberto Molinari Model Checking and Interval Temporal Logics: Checking Interval Properties of Computations
speaker: Alberto Molinari

Abstract

  

10:56 11:08 Panagiotis Kouvaros Verifying Emergent Properties of Swarms
speaker: Panagiotis Kouvaros

Abstract

  

We investigate the general problem of establishing whether a swarm satisfies an emergent property. We put forward a formal model for swarms that accounts for their nature of unbounded collections of agents following simple local protocols. We formally define the decision problem of determining whether a swarm satisfies an emergent property. We introduce a sound and complete procedure for solving the problem. We illustrate the technique by applying it to the Beta aggregation algorithm.

11:08 11:20 Sasha Rubin Parameterised Verification: Recent Advances
speaker: Sasha Rubin

Abstract

  

10:20 11:20 Session 8B (EII Lecture room)
10:20 10:32 Arthur Milchior Expressivity of FO[+1, f (x)] and ∃MSO[+1, ×b] by its Spectra and its Finite Satisfiability Problem.
speaker: Arthur Milchior

Abstract

  

This talk consider two logics, both with the successor function:
-The first order logic with an uninterpreted function and
-The existential monadic second order logic — that is first-order logic over words —, with the multiplication by a constant b.
The finite satisfiability of those logics is proven to be undecidable. A b-regular set is a set accepted by an automaton reading number in base b. A spectrum is a set of cardinal of models of a formula. Every b-regular set are spectra of those logics. Furthermore, it is proven that an encoding of the halting times of a non deterministic 2-counter automaton, which is a Turing-complete model, is also a spectrum. Finally, it is shown that the logic with uninterpreted function and successor can encode some function that increase quickly, such as the Knuth Arrows.

10:32 10:44 Charles Paperman Finite-Degree Predicates and Two-Variable First-Order Logic
speaker: Charles Paperman

Abstract

  

In this talk, I will resent two new results about the expressivity of two-variable first-order logic over finite words equipped with arbitrary numerical predicates. This fragment of logic is equivalent to languages recognized by linear size and constant depth boolean circuit. I will focus on the so-called Crane Beach conjecture for FO^2. Proving the Crane Beach conjecture in this context would improve on a known lower bound for addition, stating that the function of addition is not computable by circuits of constant depth with a linear number of wires.

First we will explain how languages with a neutral letter definable in two-variable logic with arbitrary numerical predicates can be defined using only the linear order and the following predicates:
•The class F of finite-degree predicates,that is, binary predicates that are relations over integers and such that each vertex of their underlying infinite directed graph has a finite degree.
•A predicate called MSB0, true of positions x and y if the binary decomposition of y is obtained by zeroing the most significant bit of x.

Then, a Crane Beach result will be presented for the restricted signature containing < and F predicates. Thus, this a result which is one predicate shy from showing the Crane Beach conjecture for FO^2.

10:44 10:56 Jan Obdržálek FO Model Checking on Posets of Bounded Width
speaker: Jan Obdržálek

Abstract

  

Over the past two decades the main focus of research into first-order (FO) model checking algorithms have been sparse relational structures—culminating in the FPT-algorithm by Grohe, Kreutzer and Siebertz for FO model checking of nowhere dense classes of graphs [STOC’14], with dense structures starting to attract attention only recently. Bova, Ganian and Szeider [LICS’14] initiated the study of the complexity of FO model checking on partially ordered sets (posets). Bova, Ganian and Szeider showed that model checking existential FO logic is fixed-parameter tractable (FPT) on posets of bounded width, where the width of a poset is the size of the largest antichain in the poset. The existence of an FPT algorithm for general FO model checking on posets of bounded width, however, remained open. We resolve this question in the positive by giving an algorithm that takes as its input an n- element poset P of width w and an FO logic formula φ, and determines whether φ holds on P in time f(φ, w)·n^2 .

Joint work with Jakub Gajarský, Petr Hliněný, Daniel Lokshtanov, Sebastian Ordyniak, M. S. Ramanujan and Saket Saurabh.

10:56 11:08 Jakub Gajarský First order limits of sparse graphs: Plane trees and path-width
speaker: Jakub Gajarský

Abstract

  

Asymptotic properties of a sequence $G_1, G_2, \ldots$ of graphs can be analysed, similarly to a sequence of numbers, using the concepts of convergence and limit. However, unlike in the case of numbers, it is not immediately clear what it means for a sequence of graphs to converge and what should the limiting object be. This has lead to several different notions of convergence, the two most studied being dependent on the density of graphs in the sequence -- the convergence of dense graphs developed by Lovász and coauthors and Benjamini-Schramm convergence for graphs of bounded degree.

As an attempt to unify the notions of convergence for sparse and dense graphs, Nešetřil and Ossona de Mendez introduced the notion of first-order convergence. If the sequence of graphs is first-order convergent, we are interested in its representation by a single analytical object called the limit modeling. Since it is known that there exist first-order convergent sequences of graphs with no limit modeling, it is a natural question to ask which properties of graphs in the convergent sequence guarantee the existence of the corresponding limit modeling. It is conjectured that a sufficient condition on the existence of limit modeling is that the graphs in the convergent sequence come from nowhere dense graph class (here the notion of nowhere dense graph class captures, in a very robust sense, graph classes which can be called sparse). So far little progress has been made towards this conjecture -- until recently the best result was that every first-order convergent sequence of trees or graphs with no long path (graphs with bounded tree-depth) has a limit modeling.

In the talk we present strengthening of this result by showing that every first-order convergent sequence of plane trees (trees with embeddings in the plane) and every first-order convergent sequence of graphs with bounded path-width has a limit modeling.

This talk is based on joint work with Petr Hliněný, Tomáš Kaiser, Daniel Král', Martin Kupec, Jan Obdržálek, Sebastian Ordyniak and Vojtěch Tůma.

11:08 11:20 A V Sreejith Limited set quantifiers over countable linear orderings
speaker: A V Sreejith

Abstract

  

In this paper, we study several sublogics of monadic second-order logic over countable linear orderings, such as first-order logic, first-order logic on cuts, weak monadic second-order logic, weak monadic second-ordered logic with cuts, as well as fragments of monadic second-order logic in which sets have to be well ordered or scattered. We give decidable algebraic characterizations of all these logics and compare their respective expressive power.

11:20 11:30 Break
11:30 12:30 Session 9A (EI Lecture room)
11:30 11:42 Wojtek Jamroga State and Path Coalition Effectivity Models of Concurrent Multi-Player Games
speaker: Wojtek Jamroga

Abstract

  

We consider models of multi-player games where abilities of players and coalitions are defined in terms of sets of outcomes which they can effectively enforce. We extend the well studied state effectivity models of one-step games in two different ways. On the one hand, we develop multiple state effectivity functions associated with different long-term temporal operators. On the other hand, we define and study coalitional path effectivity models where the outcomes of strategic plays are infinite paths. For both extensions we obtain representation results with respect to concrete models arising from concurrent game structures. We also apply state and path coalitional effectivity models to provide alternative, arguably more natural and elegant semantics to the alternating-time temporal logic ATL*, and discuss their technical and conceptual advantages.

11:42 11:54 Vadim Malvone Reasoning about graded modalities in strategy logic
speaker: Vadim Malvone

Abstract

  

Strategy Logic is a powerful formalism useful to describe game concepts in multi-agent settings by explicitly quantifying over strategies treated as first-order citizens. In this talk we introduce Graded Strategy Logic (GSL), an extension of Strategy Logic along with graded quantifiers. This allows us to express properties such as “there are at least g strategies" satisfying a given objective. As different strategies may induce the same outcome, although looking different, the main difficulty in defining GSL is the design of a valid machinery to count strategies, as we show. To give an evidence of GSL usability, we investigate basic questions over this logic. In particular, we report on positive results about the determinacy of turn-based games and the related model-checking problem over a restricted fragment of this logic, which we show to be PTime-Complete.

This talk is based of a paper autored by: Vadim Malvone, Fabio Mogavero, Aniello Murano and Loredana Sorrentino

11:54 12:06 Jan Bok Cooperative Interval Games
speaker: Jan Bok

Abstract

  

12:06 12:18 Marie van den Bogaard Consensus game acceptors
speaker: Marie van den Bogaard

Abstract

  

We present a game for recognising formal languages, in which two players with imperfect information need to coordinate on a common decision, given private input strings correlated by a finite graph. The players have a joint objective to avoid an inadmissible decision, in spite of the uncertainty induced by the input. We show that the acceptor model based on consensus games characterises context-sensitive languages, and conversely, that winning strategies in such games can be described by context-sensitive languages. We also discuss consensus game acceptors with a restricted observation pattern that describe nondeterministic linear-time languages. Joint work with Dietmar Berwanger. To appear in DLT 2015.

12:18 12:30 Eryk Kopczyński First-order definable Constraint Satisfaction Problems
speaker: Eryk Kopczyński

Abstract

  

First-order definable structures with atoms are infinite, but exhibit enough symmetry to be effectively manipulated. We study Constraint Satisfaction Problems (CSPs) where both the instance and the template can be definable structures with atoms. We argue that such templates and instances occur naturally in Descriptive Complexity Theory.

In this talk we will concentrate on CSPs over finite templates and infinite, definable instances. In this case even decidability is not obvious, and to prove it we apply results from topological dynamics. We also prove that the complexity of solving such CSPs is one exponential level higher than the complexity of the finite CSP problem over the same template.

11:30 12:30 Session 9B (EII Lecture room)
11:30 11:42 Parvaneh Babari Weighted Register Automata and Weighted Existential MSO Logic on Data Words
speaker: Parvaneh Babari

Abstract

  

In these paper, we deal with the automata models for quantitative aspects of systems with infinite data domains, e.g., the costs of storing data on a remote server or the consumption of resources (e.g., memory, energy, time) during a data analysis. We introduce weighted register automata on data words, study their closure properties and introduce a determinizable subclass of them. In our main result, we give a logical characterization of weighted register automata by means of weighted existential monadic second-order logic.

11:42 11:54 Raffaella Gentilini Finite Valued Weighted Automata
speaker: Raffaella Gentilini

Abstract

  

Any weighted automaton (WA) defines a relation from finite words to values: given an input word, its set of values is obtained as the set of values computed by each accepting run on that word. A WA is $k$-valued if the relation it defines has degree at most $k$, i.e., every set of values associated with an input word has cardinality at most $k$. We investigate the class of quantitative languages defined by $k$-valued automata, for all parameters $k$. We consider several measures to associate values with runs: sum, discounted-sum, and more generally values in groups.

We define a general procedure which decides, given a bound $k$ and a WA over a group, whether this automaton is $k$-valued. We also show that any $k$-valued WA over a group, under some general conditions, can be decomposed as a union of $k$ unambiguous WA. While inclusion and equivalence are undecidable problems for arbitrary sum-automata, we show, based on this decomposition, that they are decidable for $k$-valued sum-automata, and $k$-valued discounted sum-automata over inverted integer discount factors. We finally show that the quantitative Church problem is undecidable for $k$-valued sum-automata, even given as finite unions of deterministic sum-automata.

11:54 12:06 Nikos Tzevelekos Bisimilarity in fresh-register automata
speaker: Nikos Tzevelekos

Abstract

  

Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name creation. This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have appeared in the literature: general register assignments; assignments where duplicate register values are disallowed; and assignments without duplicates in which registers cannot be empty. In the general case, we show that the problem is EXPTIME-complete. However, the absence of duplicate values in registers enables us to identify inherent symmetries inside the associated bisimulation relations, which can be used to establish a polynomial bound on the depth of Attacker-winning strategies. Furthermore, they enable a highly succinct representation of the corresponding bisimulations. By exploiting results from group theory and computational group theory, we can then show solvability in PSPACE and NP respectively for the latter two register disciplines. In each case, we find that freshness does not affect the complexity class of the problem. The results allow us to close a complexity gap for language equivalence of deterministic register automata. We show that deterministic language inequivalence for the no-duplicates fragment is NP-complete, which disproves an old conjecture of Sakamoto. Finally, we discover that, unlike in the finite-alphabet case, the addition of pushdown store makes bisimilarity undecidable, even in the case of visibly pushdown storage.

This is joint work with Andrzej Murawski and Steven Ramsay

12:06 12:18 Shiguang Feng Path-Checking for MTL and TPTL over Data Words
speaker: Shiguang Feng

Abstract

  

Precise complexity results are derived for the model checking problems for MTL (metric temporal logic) and TPTL (timed propositional temporal logic) on (in)finite data words and deterministic one-counter machines. Depending on the number of register variables and the encoding of numbers in constraints (unary or binary), the complexity is either P-complete or PSPACE-complete.

12:18 12:30 Karoliina Lehtinen Disjunctive form and the modal mu alternation hierarchy
speaker: Karoliina Lehtinen

Abstract

  

The modal mu calculus consists of a propositional modal logic augmented with its namesake least fixpoint operator and the dual, the greatest fixpoint operator. The alternating usage of these operators is the root of both the expressiveness and complexity of the logic: the more alternations are allowed, the richer the fragment but the more difficult its model-checking.

It is therefore of both practical and theoretical interest to reduce, whenever possible, the number of alternations used to express a property. However only properties expressible in modal logic or with a single type of fixpoint operator are currently known to be recognisable. One of the difficulties of deciding the least number of alternations required to express a property is the lack of canonical normal form: misleadingly different formulas can be semantically equivalent and in general it is poorly understood how to produce or even recognise a good syntactic representation of a property. There are however various syntactic restrictions which lead to better behaved formulas. One such restriction is disjunctive form, which only allows very restricted use of conjunctions. Although less concise than the whole logic, disjunctive modal mu is equally expressive. The transformation into disjunctive form is based on a tableau decomposition of a formula which forces it to be in many ways well-behaved. In particular, satisfiability and synthesis are straight-forward for disjunctive modal mu.

This talk presents how disjunctive form also makes deciding the first levels of the alternation hierarchy straight-forward. Given a disjunctive formula F, one can obtain a formula no larger than F, with no least fixpoint operators, which is equivalent F if and only if F can be expressed without \least fixpoint operators. Although the first levels of the alternation hierarchy have been known to be decidable for some time, the target formulas, which from a model checking point of view are a rather crucial by-product of decidability, have received little attention. The ones described as part of the proof of decidability, can incur a double-exponential blow-up in the size of the formula and do not necessarily resemble the original formulas. By using disjunctive form, least fixpoint operators can be eliminated elegantly at little cost in addition to that of the transformation into disjunctive form.

The transformation into disjunctive form is involved and it has so far been an open question whether it preserves the alternation depth of formulas. If this was the case, it would be sufficient to study the long-standing open problem of the decidability of the alternation hierarchy on this well-behaved fragment. I show that although the disjunctive fragment of modal mu is in some sense itself very well-behaved with respect to the alternation hierarchy, the transformation into it does not preserve alternation depth.

On one hand, the alternation hierarchy is decidable for the disjunctive fragment of modal mu with respect to tableau equivalence, a stricter notion of equivalence than semantic equivalence. In fact, for disjunctive formulas, tableau equivalence preserves alternation depth. However, this does not extend to non-disjunctive formulas. Not only does the transformation into disjunctive form not preserve alternation depth, there is in fact no hope for an upper bound on the alternation depth of the tableau-equivalent disjunctive formula with respect to the alternation depth of the original non-disjunctive formula. Indeed, for arbitrarily large n, there are formulas with a single alternation which are tableau equivalent only to disjunctive formulas with at least n alternations.

Conversely, there are formulas of modal mu with arbitrarily large alternation depth which are tableau equivalent to a disjunctive formula without alternations. This shows that the alternation depths of tableau equivalent formulas are only directly related within the disjunctive fragment.

The immediate consequence of these results is that deciding the alternation hierarchy for the disjunctive fragment of modal mu , an open but easier problem, is not sufficient for deciding the alternation hierarchy in the general case. The formulas which prove this are examples for which deciding the semantic alternation of a formula is seemingly difficult. Indeed, disjunctive form eliminates some types of accidental complexity, but these formulas illustrate cases of accidental complexity which need to be tackled with novel methods.

Location

Highlights 2015 will be held in the campus of Faculty of Economics and Management, Czech University of Life Sciences in Prague-Suchdol. On Wednesday, the whole program, including conference dinner and a special Mathematical Colloquia talk by Moshe Vardi, will take place in Karolinum, the historical seat of the Charles University in Prague (see the map).

Accommodation

You can find a variety of hotels in Prague, the workshop venue is easily reachable public transport. The organizers reserved a number of modestly prized rooms at the campus where the workshop will be held.

Directions

There is bus station "Zemědělská univerzita" in front of the campus where the conference is held. The buses to "Zemědělská univerzita" are departing from various places in Prague. One good entry point is "Dejvická" station which is easily reachable by metro. Busses No. 107, 147 depart from "Dejvická" and go directly to "Zemědělská univerzita". An optimal connection can be found at Prague Public Transit Company site (station names can be entered without Czech accents).

By flight

From Prague airport: in front of the main airport hall, take a bus No. 119 to "Nádraží Veleslavín" metro station. From there, go by metro A to "Dejvická". Then, take a bus No. 107 or 147 and go to "Zemědělská univerzita".

By train

From the main station (Hlavní nádraží): There is a Metro station "Hlavní nádraží" directly in the main station building. You can reach "Dejvická" by metro, but you need need to change at "Museum". Another option is to take a tram No. 26 which goes directly to "Dejvická". At "Dejvická", take a bus No. 107 or 147 and go to "Zemědělská univerzita".

How to Reach Karolinum

Go to "Můstek" metro station and walk for about 200m. If you travel from "Zemědělská univerzita", take a bus No. 107 or 147, go to "Dejvická" metro station, and then to "Můstek". The whole trip takes about 30 minutes.

Information about public transportation in Prague is available at the Prague Public Transit Company site.

Organizers