Highlights 2015

Abstract

The constraint satisfaction problem (CSP) provides a common framework for expressing a wide range of both theoretical and real-life combinatorial problems. One solves an instance of CSP by assigning values to the variables so that the constraints are satisfied.

This tutorial will concentrate on the computational (and descriptive) complexity of CSP over a fixed constraint language on a finite domain. This restricted framework is still broad enough to include many NP-complete problems, yet it is narrow enough to potentially allow a complete classification of all such CSP problems. One particularly important achievement is the understanding of what makes a problem in the class computationally easy or hard. It is not surprising that hardness comes from lack of symmetry. However, usual objects capturing symmetry, automorphisms (or endomorphisms) and their groups (or semigroups), are not sufficient in this context. It turned out that the complexity of CSP is determined by more general symmetries: polymorphisms and their clones.

My aim in this tutorial is to introduce the basics of this exciting area and highlight selected deeper results..

Abstract

This talk will focus on a few highlights from the huge theory of weighted automata (WA).

First, we introduce weighted automata and show how they can be used to model quantitative aspects of systems. This model is extremely versatile and by varying the weights/computations it can be used to describe counting, probabilities, optimizations, average power consumption, etc. We focus on sequential finite behaviors (words), and quickly discuss a few extensions (infinite words, trees, pebble-walking automata). We also investigate a few decision problems: emptiness, threshold, equivalence, recognizability of the support, etc.

Second, we concentrate on weights/computations arising from a semiring. Actually, weighted automata were originally studied in this setting only, giving rise to an extensive theory of WA and formal power series (FPS), i.e., quantitative functions over words. This special case allows for specific algorithms/definitions/results. For instance, a weighted automaton can be represented by a morphism to the monoid of matrices. The value/semantics of a WA can be computed efficiently using products of vectors/matrices (linear in the size of the input word, quadratic in the size of the automaton). Further, when the semiring is a field (possibly non-commutative), we will explain how to minimize a WA. As a consequence, the equivalence problem is decidable for WA over a subsemiring of a field. Last, the semiring structure allows one to define a (Cauchy) product of FPS and to obtain the equivalence between functions (FPS) that can be computed by WA and functions that can be denoted by weighted rational expressions. This extension of Kleene’s result is known as Schützenberger's theorem.

Third, we will survey how weighted logics have been developed to match the quantitative expressive power of WA. The story started 10 years ago with the introduction of a quantitative (semiring) semantics for MSO logic over finite words and an equivalence theorem between weighted automata and a restricted weighted MSO logic. Since then, many extensions have been studied. Some extend the structure from words to trees, infinite words, pictures, etc. Others concern the quantitative aspect, moving from semirings to more general weights/computations.

Also, the proof techniques have matured, from low level, carefully mimicking the classical proofs in the boolean setting, to higher level, using various abstract semantics. We illustrate this evolution by introducing a core weighted logic and its abstract semantics as multisets of weight structures. The equivalence between weighted automata and core weighted logic holds at the level of the abstract semantics. Most existing results can be derived easily.

Abstract

A possible way to relax the notion of determinism is to consider unambiguous machines: nondeterministic machines that have at most one accepting run on each input. In this talk, we will consider several situations in which non-ambiguity arises in automata theory, surveying the cases of standard finite words up to infinite trees, as well as data-words. The main conclusion of this talk is that the notion of unambiguity, though relevant in many situations, is so far not well understood and yields difficult open questions.

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.

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).

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.

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.

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.

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".

Abstract

In this talk we look at temporal logics on traces that are assumed to be finite, as typical of action planning in Artificial Intelligence and of processes modeling in Business Process Management. Having to deal with finite traces has been considered a sort of accident in much of the AI and BPM literature, and standard temporal logics (on infinite traces) have been hacked to fit this assumption. Only recently a specific interest in studying the impact of such an assumption has emerged. We will look at two specific logics (i) LTLf, i.e., LTL interpreted over finite traces, which has the expressive power of FOL and star-free regular expression over finite stings; and (ii) LDLf, i.e., Linear-time Dynamic Logic on finite traces, which has the expressive power of MSO and full regular expression. We review the main results on satisfiability, verification, and synthesis, also drawing connections with work in AI planning. The main catch is that working with these logics can be based on manipulation of regular automata on finite strings, simplifying greatly reasoning and especially synthesis. Joint work with Moshe Y. Vardi (Rice Univ., USA)

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

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.

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.

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.

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.

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.

Abstract

Various types of automata models with weights attached to the states and/or transitions have been introduced to model and analyze the resource-awareness and other quantitative phenomena of systems. In this context, weight accumulation appears as a natural concept to reason about cost and utility measures. The accumulation of non-negative weights can, for instance, serve to formalize the total energy consumption of a given task schedule or the total penalty to be paid for missed deadlines. Weight functions with negative and positive values can be used to model the energy level in battery-operated devices or the total win or loss of a share at the stock market over one day. The conceptual similarity between accumulated weights and counter machines causes the undecidability of many verification problems for multi-weighted models and temporal logics with weight accumulation over finite paths of unbounded length. However, decidability can be achieved for verification tasks in specialized structures, such as energy games or models with non-negative weight functions. Likewise, decidability results have been established for temporal logics with restricted forms of weight accumulation, such as modalities for weight accumulation along finite windows or limit-average properties. This extended abstract deals with discrete-time Markovian models and addresses algorithmic problems for a cost-utility analysis. First, it reports on results on linear temporal specifications with weight assertions. The second part addresses algorithms to compute optimal weight bounds for probabilistic reachability constraints and assertions on cost-utility ratios.

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.

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)

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.

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.

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.

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.

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.

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.

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.

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

Abstract

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.

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.

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.

Abstract

Well-structured systems, aka WSTS, are a family of infinite-state computational models that support generic decidability results based on well-quasi-ordering theory. They have many applications in logics of programs and verification. In this talk we present a modern version of the basic WSTS algorithms and describe new techniques for the complexity analysis of WSTS models.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

Abstract

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

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.

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.

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.

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.

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).

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.

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.

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.

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.

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.

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.

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.

Abstract

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.

Abstract

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.

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.

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.

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.

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.

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.

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

Abstract

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.

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.

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.

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.

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

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.

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.