Highlights 2013

Abstract

  

Systems equipped with counters are central when modeling distributed protocols, programs with recursive parallel threads, programs with pointers, broadcast protocols, databases, etc. When it comes to model-checking counter systems and their variants, the main results are that verification is undecidable when zero-tests are allowed, while several problems can be decided when zero-tests are forbidden — one speaks of VASS, for "vector addition systems with states", or equivalently "Petri nets". In the case of Petri nets, reachability was shown decidable in 1982, and the reachability problem for Petri nets and related decidable problems on subclasses of counter systems are pivot problems not only for the verification of infinite-state systems but also for problems appearing in very active research areas related to various logics and automata for data words/trees. Hence, the design of efficient algorithms for the reachability problem for VASS may have a great impact, not only in the realm of formal verification. It is however a very difficult problem. Therefore, improving the computational cost for solving the reachability problem for Petri nets would also improve the complexity of the formal verification of numerous classes of infinite-state systems.

Strikingly, the decision algorithm for Petri net reachability has never been implemented. This is because of its high complexity, both conceptual (the algorithm is very hard to understand and to describe) and computational (it is assumed that the complexity of the algorithm is not primitive-recursive). The general problem is known to be decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently, from this decomposition, it was proved that a final configuration is not reachable from an initial one if, and only if, there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general Petri net reachability problem based on two semi-algorithms. A first one that tries to prove reachability by enumerating finite sequences of actions and a second one that tries to prove non-reachability by enumerating Presburger formulas.

In this presentation, we provide a simple proof of the Petri net reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations, inspired from Hauschildt, that directly proves the existence of Presburger inductive invariants.

Abstract

  

The theme of this tutorial is (recent) applications of logic in the design and analysis of efficient algorithms. I will cover the following three topics.

1. Logical techniques in the analysis of generic algorithms

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

2. Algorithmic meta theorems

   Algorithmic meta theorems attempt to explain and unify algorithmic results by proving tractability not only for individual problems, but for whole classes of problems. These classes are typically defined in terms of logic. The prototypical example of an algorithmic meta theorem is Courcelle's Theorem, stating that all properties of graphs of bounded tree-width that are definable in monadic second-order logic are decidable in linear time.

   In the tutorial, I will focus on meta theorems for first-order logic, where by now we have a fairly complete picture of graph classes admitting a nontrivial meta theorem

3. Applications of meta theorems in algorithmic graph structure theory

   In this last part I will discuss applications of algorithmic meta theorems to problems in algorithmic graph structure theory. By this I mean graph algorithms that use meta theorems to solve tasks for which no other (direct combinatorial) algorithm is known.

It is worth noting that the algorithmic problems considered in all three parts are not derived from logic, such as satisfiability or model-checking problems, but "standard" algorithmic problems, often with a strong combinatorial and graph theoretical flavour. On the way, I will introduce the necessary graph theory, including nowhere dense graphs and certain aspects of graph minor theory.

Abstract

  I will report on our experience running SAGE for over 500-machine years in Microsoft's security testing labs. SAGE is a whitebox fuzzing tool for security testing. It performs symbolic execution dynamically at the binary (x86) level, generates constraints on program inputs, and solves those constraints with an SMT solver in order to generate new inputs to exercize previously uncovered program paths or trigger security vulnerabilities (like buffer overflows). This process is repeated using novel state-space exploration techniques that attempt to sweep through all (in practice, many) feasible execution paths of the program while checking simultaneously many properties. This approach thus combines program analysis, testing, model checking and automated theorem proving (constraint solving). Since 2009, SAGE has been running 24/7 on average 100+ machines automatically ``fuzzing'' hundreds of applications. This is the largest computational usage ever for any SMT solver, with over 4 billion constraints processed to date. In the process, SAGE found many new security vulnerabilities (missed by blackbox fuzzing and static program analysis) and was credited to have found roughly one third of all the bugs discovered by file fuzzing during the development of Microsoft's Windows 7, saving millions of dollars by avoiding expensive security patches to nearly a billion PCs. In this talk, I will present the SAGE project, highlight connections with program verification, and discuss open research challenges. This is joint work with Michael Levin, David Molnar, Ella Bounimova, and other contributors.

Abstract

  Incomplete information is ubiquitous in database applications, and yet our understanding of it is still rather basic. Since an incomplete database can represent multiple databases, query answering boils down to solving an entailment problem, while database systems are good at performing model-checking algorithms on first-order structures. Thus, to take advantage of them, we need to understand when entailment can be reduced to model-checking. We show that this happens for queries which are monotone with respect to the semantics of incompleteness, and that such monotonicity can be described via homomorphism preservation, for different notions of homomorphisms. Combining the latter with preservation theorems from logic (existing as well as new), we obtain classes of queries for which standard database systems can correctly compute answers over incomplete databases, or, logically speaking, for which entailment can be solved by simple model-checking.

Abstract

  With the recent resurgence of graph data model several languages for querying such data have been proposed. Traditionally these languages concentrated on querying topological properties while largely ignoring the actual data stored in the graph. In this presentation we will highlight how adding features that enable querying both data and topology affects the languages used to extract information from graph databases.

Abstract

  Unions of acyclic conjunctive queries (CQs) can be evaluated in linear time, as opposed to arbitrary CQs, for which the evaluation problem is NP-complete. It is known that evaluation of semantically acyclic unions of CQs - i.e., unions of CQs that are equivalent to a union of acyclic ones - is tractable. We study the notion of semantic acyclicity in the context of graph databases and unions of conjunctive regular path queries (UCRPQs). We prove that checking whether a UCRPQ is semantically acyclic is decidable in 2ExpSpace and is ExpSpace-hard. We show that evaluation of semantically acyclic UCRPQs is fixed-parameter tractable.

Abstract

  The guarded fragment of first-order logic (GFO) shares many useful properties with modal logic, but fails to have Craig interpolation. Recently, an extension called the guarded negation fragment (GNFO) was shown to have interpolation, but the proof was non-constructive. The goal in this research (suggested by Benedikt, ten Cate, and Lutz) is to develop constructive methods for interpolation, in order to see whether interpolation can be performed in practice and to better understand the complexity of the problem. I describe some preliminary work on constructive interpolation for GNFO.

Abstract

  For a formula $\phi$ over a signature including predicates $P_1...P_k$, we define the image of $\phi$ as the set of tuples $(n_1...n_k)$ such that there is a model of $\phi$ where exactly $n_i$ elements satisfy $P_i$. For example, if each author has written exactly 2 papers, and each paper has exactly 3 authors, then 2*total number of authors=3*total number of authors. This can be seen as a generalization of the well known notion of a spectrum. Our main result is that, for formulae of FO2C, spectra and images are definable in Presburger arithmetic, and thus semilinear (and closed under complement).

Abstract

  In machine learning there is an inherent trade-off between the efficiency of the learning algorithm and the expressiveness of the hypothesis that one is allowed to learn. Even though this trade-off is present in almost every machine learning task, it is hard to capture formally and still often resolved based on instinct and experience. We propose using parametrized logical formulas to represent hypotheses and then exploit propositional solvers for efficient learning and results from descriptive complexity to get expressiveness guarantees. This allows a more systematic study of the above trade-off and, as we show on a few examples, it is applicable to practical learning tasks.

Abstract

  Guarded normal form requires occurrences of fixpoint variables in a μ-calculus formula to occur under the scope of a modal operator. The literature contains guarded transformations that effectively bring a μ-calculus formula into guarded normal form. We show that the known guarded transformations can cause an exponential blowup in formula size, contrary to existing claims of polynomial behaviour. We also show that any poly- nomial guarded transformation for μ-calculus formulas in the more relaxed vectorial form gives rise to a polynomial solution algorithm for parity games, the existence of which is an open problem.

Abstract

  LTL has emerged as the primary logic for specifying temporal properties. This is largely due to the low complexity of its associated model checking problem and its high expressibility - with the celebrated result of Kamp showing that LTL has the same expressive power as first-order logic. In the quantitative setting, Metric Temporal Logic is quickly becoming the standard to which all other temporal logics are compared. It turns out that the expressive power of MTL is dependent on the set of constants available, and I will give a precise characterization of when MTL has the same expressive power as first-order logic.

Abstract

  We study Gaifman and Hanf locality of an extension of first-order logic with modulo p counting quantifiers (FO+MODp, for short) with arbitrary numerical predicates. We require that the validity of formulas is independent of the particular interpretation of the numerical predicates and refer to such formulas as arb-invariant formulas. We give a detailed picture of locality and non-locality properties of arb- invariant FO+MODp.

Abstract

  When can two regular word languages K and L be separated by a simple language? We investigate this question and consider separation by piecewise- and suffix-testable languages and variants thereof. We give characterizations of when two languages can be separated and present an overview of when these problems can be decided in polynomial time if K and L are given by nondeterministic automata.

Abstract

  We discuss the separation problem for regular languages. We give a Ptime algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a $\mathcal{B}\Sigma_1(<)$ sentence can witness that the languages are disjoint. If this is possible, we express a separator by saturating one of the original languages by a suitable congruence. Following the same line, we show that one can also decide whether two regular languages can be separated by an unambiguous (i.e. $FO^2(<)$-definable) language, albeit with a higher complexity.

Abstract

  

Abstract

  In this talk, I will discuss some recent developments about boundedness games. They are two-player games played over graphs, featuring counters. The first player's objective is to satisfy a parity condition and that the counter values are bounded. A lot of questions are open: what is the algorithmic complexity of deciding the winner, and does there always exist finite-memory winning strategies? In particular, as shown by Thomas Colcombet, proving the existence of finite-memory winning strategies for (some) boundedness games is the last missing item to prove the decidability of cost-MSO over infinite trees. I will give an overview of where we stand now and what are the next challenges.

Abstract

  A two-way transducer is a finite state sequential machine with a two-way input tape and a one-way output tape. At each step of the computation, it reads the current symbol, outputs a possibly empty word, then changes its internal state and moves its input head, according to the transition taken with current state and the letter read. It computes a partial function from words over an alphabet to another set of words. Similarly, a MSO-definable function over words is defined as interpretations of linear graphs through logic. A result by Engelfriet and Hoogeboom proved the equivalence of the two models. I will recall the definition of both models, and state an extension of this result to the natural subclass of aperiodic two-way transducers.

Abstract

  Distance automata are automata weighted over the semiring (N U {+infinity},min,+) that compute functions from words to N U {+infinity}. It is known that testing f0 and two functions f,g computed by distance automata, answers "yes" if f(1+e)g(w), and may answer "yes" or "no" in all other cases. This is a joint work with Thomas Colcombet.

Abstract

  We introduce cost register automata (CRA) -- this is a deterministic model to associate costs with strings that is parametrized by operations of interest (such as addition, scaling, and minimum), and a notion of regularity that provides a yardstick to measure expressiveness. Our notion of regularity relies on the notion of string-to-tree transducers, and allows associating costs with events that are conditioned on regular properties of future events. CRAs compute regular functions using multiple write-only registers whose values can be combined using the allowed set of operations. We then discuss various analysis problems associated with CRAs and regular functions, including the decidability of equivalance and containment, register and state minimization, and Angluin-style learning of cost functions.

Abstract

  This work addresses, and proposes a solution to, the problem of the validity of weighted automata in which epsilon-transitions may result in infinite summations. With a topological approach, a definition of validity is taken that insures that any closure algorithm will succeed on every valid weighted automaton. This definition is stable with respect to natural transformations of automata. Validity is shown to be decidable when weights are taken in Q or R. The corresponding algorithm is implemented in the VAUCANSON platform. The problem remains open in general.

Abstract

  We prove that language equivalence of deterministic one- counter automata is NL-complete. This improves the super- polynomial time complexity upper bound shown by Valiant and Paterson in 1975. Our main contribution is to prove that two deterministic one-counter automata are inequivalent if and only if they can be distinguished by a word of length polynomial in the size of the two input automata.

Abstract

  We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachability-like decision problems for counter systems. We show that allowing/disallowing atomic formulas expressing repetitions of values in the past corresponds to the reachability/coverability problem in Petri nets. This gives us 2EXPSPACE upper bounds for several satisfiability problems. We prove matching lower bounds by reduction from a reachability problem for a newly introduced class of counter systems. This new class is a succinct version of vector addition systems with states in which counters are accessed via pointers, a poten- tially useful feature in other contexts. We strengthen further the correspondences between data logics and counter systems by characterizing the complexity of fragments, extensions and variants of the logic. For instance, we precisely characterize the relationship between the number of attributes allowed in the logic and the number of counters needed in the counter system.

Abstract

  Given two pushdown systems, the bisimilarity problem asks whether they are bisimilar. While this problem is known to be decidable our main result states that it is nonelementary, improving EXPTIME-hardness, which was the previously best known lower bound for this problem. Our lower bound result holds for normed pushdown systems as well.

Abstract

  Metric temporal logic (MTL) is one of the most prominent specification formalisms for real-time systems. Over infinite timed words, full MTL is undecidable, but satisfiability for its safety fragment was proved decidable several years ago. The problem is also known to be equivalent to a fair termination problem for a class of channel machines with insertion errors. However, the complexity has remained elusive, except for a non-elementary lower bound. Via another equivalent problem, namely termination for a class of rational relations, we show that satisfiability for safety MTL is not primitive recursive, yet is Ackermannian, i.e., among the simplest non-primitive recursive problems. This is surprising since decidability was originally established using Higman's Lemma, suggesting a much higher non-multiply recursive complexity.

Abstract

  We prove that the positive fragment of minimal first-order intuitionistic logic is not of elementary complexity. The proof uses an automata-theoretic approach taking advantage of the computational power of alternation.

Abstract

  Decision problems with a non-elementary complexity occur naturally in logic, combinatorics, formal language, verification, etc., with complexities ranging from simple towers of exponentials to Ackermannian and beyond. Somewhat surprisingly, we lack the definitions of classes and reductions that would allow to state completeness results at such high complexities. We introduce a hierarchy of fast-growing complexity classes and discuss its suitability for completeness statements of non-elementary problems.

Abstract

  In 2006, Varacca and Voelzer proved that on finite graphs, omega-regular large sets coincide with omega-regular sets of probability 1, by using the existence of positional strategies in the related Banach-Mazur games. Motivated by this result, we try to understand relations between sets of probability~1 and various notions of simple strategy (including those introduced in a recent paper of Graedel and Lessenich). Then, we introduce a generalisation of the classical Banach-Mazur game and in particular, a probabilistic version whose goal is to characterise sets of probability~1 (as classical Banach-Mazur games characterise large sets). We obtain a determinacy result for these games, when the winning set is a countable intersection of open sets.

Abstract

  Two-player zero-sum games on finite automata are a classical metaphor for controller synthesis. An extension of this model to time-critical systems are two-player games on priced timed automata. For those games, the optimal reachability synthesis problem asks to compute a strategy (for one of the players) that guarantees to reach a given target with a total cost satisfying some optimality constraint. While, some versions of this problem have already been showed undecidable, we propose to complete the global picture by studying other variants (such as the timed-bounded version).

Abstract

  Stochastic games provide a powerful framework to model fundamental problems in the design and analysis of stochastic reactive systems. While this connection is well understood, and several results have enriched the framework, there is a wealth of research questions that are open, including some long-standing ones (such as the complexity of perfect-information stochastic reachability games). In this talk, I will survey some recent results for general model of stochastic games and related models. The talk is based on several papers, and presents an overview of recent results based on joint works with several co-authors, as well as results from other researchers.

Abstract

  Markov Decision Processes (MDPs) are 1-1/2 player stochastic games. The player tries to maximize the probability to satisfy an objective. Traditionally, the objective of the player is expressed as a set of desired sequences of states visited during the game. Recently, MDPs are viewed as generators of probability distributions over states, and objectives are defined as sets of sequences of probability distributions. We study synchronizing objectives that require that some state tend to accumulate all the probability mass. We consider three winning modes: sure, almost-sure and limit-sure.

Abstract

  We provide the first assume-guarantee reasoning for stochastic continuous-time systems. Interactive Markov chains (IMC) are compositional behavioural models similar to continuous-time Markov decision processes. Given a time-bounded property and an IMC component, we synthesize its scheduler optimizing the probability that the property is satisfied when the IMC is working in an unknown environment. We also give a specification formalism for IMC and consider unknown environments satisfying a given specification.

Abstract

  We study the central controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize both the expected mean-payoff performance of the system and its stability. We argue that the basic theoretical notion of expressing the stability in terms of the variance of the mean-payoff (called global variance in our paper) is not always sufficient, since it ignores possible instabilities on respective runs. For this reason we propose alernative definitions of stability, which we call local and hybrid variance, and which express how rewards on each run deviate from the run's own mean-payoff and from the expected mean-payoff, respectively. We show that a strategy ensuring both the expected mean-payoff and the variance below given bounds requires randomization and memory, under all the above semantics of variance. We then look at complexity of the problem of determining whether there is a such a strategy.

Abstract

  The quest for a logic for PTIME is one of the central open problems in both finite model theory and database theory. It asks whether there is a logic in which a property of finite structures is definable if, and only if, it is decidable in polynomial time. Much of the research in this area has focused on the logic FPC, the extension of least or inflationary fixed-point logic by counting terms. In fact, FPC has been shown to capture PTIME on many natural classes of structures. On the other side, already in 1992, a graph query has been constructed that can be decided in PTIME but is not definable in FPC. But while this CFI query, as it is now called, is very elegant and has led to new insights in many different areas, it can hardly be called a natural problem in polynomial time. Therefore it was often remarked that possibly all natural polynomial-time properties of finite structures could be expressed in FPC. However, this hope was eventually refuted in a strong sense by Atserias, Bulatov and Dawar who proved that the important problem of solvability of linear equation systems (over any finite Abelian group) is not definable in FPC and that, indeed, the CFI query reduces to this problem. This motivates the study of the relationship between finite model theory and linear algebra, and suggests that operators from linear algebra, such as matrix ranks or solvability operators, could be a source of new extensions to fixed-point logic, in an attempt to find a logical characterisation of PTIME. We will discuss such approaches and study the relations between different polynomial-time computable problems over (finite) rings, fields and Abelian groups in the context of logical many-to-one and Turing reductions, i.e., interpretations and generalised quantiers. In this context, we will also discuss an alternative approach towards a logic for PTIME, proposed by Blass, Gurevich and Shelah, based on choiceless computations operating directly on structures.

Abstract

  We study queries on graphs (and other relational structures) defined by families of Boolean circuits that are invariant under permutations of the vertices. In particular, we study circuits that are symmetric, that is, circuits whose invariance is explicitly witnessed by automorphisms of the circuit induced by the permutation of their inputs. We show a close connection between queries defined on structures by uniform families of symmetric circuits and definability in fixed-point logics.

Abstract

  We extend the notion of invariant elementary definability to a variety of different graph representations, including those that strictly extend the power of first-order logic with an arbitrary linear order.

Abstract

  We study the computational complexity of the model checking problem for the first order (FO) logic on interval graphs, i.e., interscetion graphs of intervals on the real line. As the main result we show that for n-vertex interval graphs this problem can be solved in time O(n log n) if we take intervals with lengths from a fixed finite set. On the other hand, we show that this is no longer true once the interval lengths taken from any set that is dense in some open subset.

Abstract

  Given structures $G$ and $H$ and a first-order formula $F$ over the same vocabulary, we say that $F$ distinguishes $G$ from $H$ if $F$ is true on $G$ but false on $H$. By alternation depth of $F$ we mean the maximum length of a sequence of nested alternating quantifiers in $F$. Obviously, this parameter is bounded from above by the quantifier depth of $F$. We will examine the maximum alternation depth and quantifier depth needed to distinguish two structures in two-variable first-order logic and its fragments. Lower bounds for the quantifier depth in the existential-positive fragment have applications to analysis of the computational complexity of Arc Consistency testing, one of the most popular heuristics for the constraint satisfaction problem.

Abstract

  This paper's main result presents a $3$-fold exponential algorithm that transforms a first-order formula $\varphi$ together with a number $d$ into a formula in Gaifman normal form that is equivalent to $\varphi$ on the class of structures of degree at most~$d$. For structures of polynomial growth, we even get a $2$-fold exponential algorithm. These results are complemented by matching lower bounds: We show that for structures of degree $2$, a $2$-fold exponential blow-up in the size of formulas cannot be avoided. And for structures of degree $3$, a $3$-fold exponential blow-up is unavoidable. As a result of independent interest we obtain a $1$-fold exponential algorithm which transforms a given first-order sentence~$\varphi$ of a very restricted shape into a sentence in Gaifman normal form that is equivalent to $\varphi$ on all structures.

Abstract

  In this talk, we introduce two properties for logical sentences using arbitrary numerical predicates: the Straubing property and the Crane Beach property. Both properties state that formulae defining simple languages do not need to use arbitrary complicated predicates, where simple either means regular or with a neutral letter. We restrict our attention to monadic predicates, and show that both properties hold in a strong syntactical sense.

Abstract

  We study Turing machines over sets with atoms, also known as nominal sets. Our main result is that deterministic machines are weaker than nondeterministic ones; in particular, P!=NP in sets with atoms. Our main construction is closely related to the Cai-Fuerer-Immerman graphs used in descriptive complexity theory.

Abstract

  In several branches of computer sciences, automata are often used to describe computational behaviours. Among those developments, automata equipped with resource devices, e.g. a finite-memory or local registers, and languages over infinite alphabets are collecting more and more attentions. In this talk, we would like to discuss a possible general theory for those resource-handling automata from the point of nominal regular expressions. As already published works, we shall present the laywered-technique and the Kleene-style theorem. On top, as our ongoing work, by comparing possible actions (labels) on transitions, we will provide how those actions differentiate their language-recognisability and show the automata-hierarchy of languages over infinite alphabets.

Abstract

  We describe a general framework for static verification of systems that base their decisions upon queries to databases. The database is specified using constraints, typically a schema, and is not modified during a run of the system. The system is equipped with a finite number of registers for storing intermediate information from the database and the specification consists of a transition table described using quantifier-free formulas that can query either the database or the registers. Our main result concerns systems querying XML databases -- modeled as data trees -- using quantifier-free formulas with predicates such as the descendant axis or comparison of data values. Our technique is based on the notion of amalgamation and is quite general. For instance it also applies to relational databases (with an optimal \pspace algorithm).

Abstract

  We introduce and explore various fragments of μ-calculus on data words. We show that full μ-calculus is undecidable, but its ν-fragment is decidable by reduction to data automata. We disclose two subclasses of the ν-fragment that enjoy the further property of being closed under negation, namely the class of Bounded Reversal (BR) and the class of Bounded Mode Alternation (BMA). The latter is contained in the former class and is already sufficiently expressive for capturing several logics studied in the literature like $\fotwo$ and Data-LTL. We then characterize these two fragments as cascades of suitably defined transducer models. We finally prove the separation of BMA from BR using a novel paradigm of circuits and prove hierarchy theorems for BMA, Data-LTL and $\fotwo$.

Abstract

  We use a variant of sets with atoms (known also as nominal sets) as a framework suitable for stating and proving the following two results on timed automata. The first result is a machine-independent characterization of languages of deterministic timed automata, a la Myhill-Nerode Theorem. As our second result we define a class of automata that slightly extends timed automata and is effectively closed under minimization.

Abstract

  Given a formula in a temporal logic such as LTL or MTL, a fundamental problem is the complexity of evaluating the formula on a given word. For LTL, the complexity of this task was recently shown to be in NC hierarchy. In this paper, we establish a connection between LTL path checking and planar circuits. We use the connection to show that the path-checking problem for LTL extended with exclusive or is already P-hard. We then present an NC algorithm for MTL, a quantitative (or metric) extension of LTL and give an AC-1 algorithm for UTL, the unary fragment of LTL.

Abstract

  We study the satisfiability problem for XPath with data equality tests. XPath is a node selecting language for XML documents whose satisfiability problem is known to be undecidable, even for very simple fragments. However, we show that the satisfiability for XPath with the rightward, leftward and downward reflexive-transitive axes (namely following- sibling-or-self, preceding-sibling-or-self, descendant-or-self) is decidable. Our algorithm yields a complexity of 3ExpSpace, and we also identify an expressive-equivalent normal form for the logic for which the satisfiability problem is in 2ExpSpace. These results are in contrast with the undecidability of the satisfiability problem as soon as we replace the reflexive-transitive axes with just transitive (non-reflexive) ones.

Abstract

  Although mixed extensions of finite games always admit equilibria, this is not the case for countable games, the best-known example being Wald'€™s pick-the-larger-integer game. Several authors have provided conditions for the existence of equilibria in infinite games. These conditions are typically of topological nature and are not applicable to countable games. Here we establish an existence result for the equilibrium of countable games when the strategy sets are a countable group and the payoff€s are functions of the group operation. In order to obtain the existence of equilibria, finitely additive mixed strategies have to be allowed. This creates a problem of selection of a product measure of mixed strategies. We propose a family of such selections and prove existence of an equilibrium that does not depend on the selection. As a byproduct we show that if finitely additive mixed strategies are allowed, then Wald's game admits an equilibrium.

Abstract

  Borel determinacy says that all infinite-tree win-lose two-player games have a Nash equilibrium provided that the winning sets of the players are Borel. This talk generalises it and shows that all infinite-tree multi-outcome multi-player games have a Nash equilibrium provided that the outcome function is "Borel measurable" and that the player preferences have no infinite ascending chains. open access to the article at http://lmcs-online.org/ojs/viewarticle.php?id=985&layout;=abstract&iid;=39

Abstract

  A well-known result states that every strategic game generates a playable effectivity function, and every playable effectivity function can be implemented with a strategic game. We show that the latter does not hold for infinite games. We identify the error in the proof, and present examples of playable effectivity functions for which no equivalent strategic game exists. Then, we characterize the class of *truly playable* functions that do correspond to strategic games. We also show that Coalition Logic cannot distinguish between the two classes, and we extend it to a logic that is expressive enough.

Abstract

  The premise of this talk is that in order to obtain realistic decision plans for Markov Decision Processes (or other decision-theoretic models) it is useful to consider solution concepts that are as discriminating as possible, by exploiting as much as possible the information provided in the model. Hence, we propose novel solution concepts for MDPs, obtained by lexicographically composing different risk attitudes, ranging from absolutely risk-averse, or pessimistic, to risk-seeking, or optimistic, in an order that depends on the application domain.

Abstract

  We consider two-player games with mean-payoff (MP) and total-payoff (TP) objectives. In single dimension, their complexities coincide. In multi dimensions, MP games are coNP-complete. We show that TP games are undecidable. We introduce conservative approximations, considering the payoff over a local finite window sliding along a play. For single dimension, we show that (i) if the window is polynomial, deciding the winner is in P, and (ii) the existence of a bounded window can be decided in NP $\cap$ coNP, and is at least as hard as solving MP games. For multi dimensions, we show that (i) the fixed window size problem is EXP-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window.

Abstract

  We consider two-player games on the configuration graph of pushdown systems with an additional finite set of non-negative integer counters. These counters can be incremented, reset to zero or left unchanged by the transition rules of the pushdown system. We associate the cost of a play with the highest counter value that occurs and look at a combined reachability and cost-limit winning condition. Is there a uniform cost-bound k such that one can win from a set of configurations A with this bound? We provide a solution to this question by an extension of the well-known saturation principle.

Abstract

  When studying games played on finite arenas, the arena is given explicitly, hiding the underlying structure of the arena. We study games where the global arena is a product of several smaller, constituent arenas. We investigate how these "global games" can be solved by playing "component games" on the constituent arenas. To this end, we introduce two kinds of products of arenas. Moreover, we define a suitable notion of strategy composition and show how, for the first notion of product, winning strategies in reachability games can be composed from winning strategies in games on the constituent arenas. For the second kind of product, the complexity of solving the global game shows that a general composition theorem is equivalent to proving Pspace = Exptime.

Abstract

  I will introduce a novel class of two-player games, called "Two-Player Stochastic meta-Parity Games", which are used in my PhD Thesis to give Game Semantics to expressive probabilistic-variants of the Modal mu-Calculus. This new class of games is proven to be "determined". I will discuss some of the technical aspects of the proof.

Abstract

  We prove that the determinacy of Gale-Stewart games whose winning sets are accepted by real-time 1-counter BŁchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. Using some results of set theory we prove that one can effectively construct a 1-counter BŁchi automaton A such that: (1) There exists a model of ZFC in which Player 1 has a winning strategy in the Gale-Stewart game G(L(A)); but the winning strategies cannot be recursive and not even hyperarithmetical. (2) There exists a model of ZFC in which the Gale-Stewart game is not determined.

Abstract

  Recently the present authors have shown that both the non-deterministic and the alternating Rabin-Mostowski index problems are decidable for languages recognisable by so-called game automata, which can be seen as the closure of deterministic ones under complementation and composition. In order to be able to claim decidability of the index problem for a given subclass of regular languages, one should however prove that membership in is decidable too. In this talk we show that membership in the class of languages recognizable by game automata is decidable.

Abstract

  If we take the complexity of a property to mean the difficulty of determining when it holds, 'simple` reductions provide a way to organise properties in terms of their complexity. In a topological space, the notion of Wadge reducibility is obtained by interpreting 'simple` as continuous. While on the Cantor space this gives a nice and useful hierarchy on the Borel sets, on the real line, for example, Wadge reducibility gives no hierarchy at all. We define a notion of reducibility for second countable T0 topological spaces, based on admissible representations, which always semi-wellorders the Borel sets.

Abstract

  M. Bojanczyk and T. Place proved that for a regular language of infinite trees it is decidable if it is a boolean combination of open sets. The class of Delta^0_2 sets consists of sets which are simultaneously F_sigma and G_delta. Every boolean combination of open sets belongs to the class Delta^0_2. I will present a small modification of the result of M. Bojanczyk and T. Place. Namely, provide an algorithm to decide whether a given regular language of infinite trees belongs to the class \Delta^0_2.

Abstract

  Acceptance games and evaluation games provide examples of parity games in which some positions can be singled out as being *basic*, in the sense that (1) matches proceed in *rounds*, moving from one basic position to another, and (2) when determining the winner of an infinite match, only the basic positions matter. We introduce a notion of bisimulation between two such games that combines Pauly's bisimulation between extensive strategic games, with a combinatorial part for the parity condition. Applications include the proof of complementation lemmas in automata theory.

Abstract

  There are well-known connections between word language theory and semigroup theory, mediated by free monoids, with deep link with the theory of finite state automata. By considering free inverse monoids instead of free monoids and premorphisms into ordered monoids instead of morphisms into monoids, we manage to lift these connections to languages of finite trees and, beyond, towards a more general notion of higher dimensional strings. In this talk, we will give a quick overview of the background results with a special emphasis on the main underlying concepts and methods.

Abstract

  One of the surprising developments in the area of program verification in the late part of the 20th Century is the emergence of Linear Temporal Logic (LTL), a logic that emerged in philisophical studies of free will, as the cannonical language for describing temporal behavior of computer systems. LTL, however, is not expressive enough for industrial applications. The first decade of the 21 Century saw the emergence of industrial temporal logics such as ForSpec, PSL, and SVA. These logics, however, are not clean enough to serve as objects of theoretical study. This talk will describe the rise and fall of LTL, and will propose a new cannonical temporal logic: Linear Dynamic Logic (LDL).

Abstract

  In multi-agent games, a recent contribution is given by Strategy Logic (SL), a powerful formalism that allows to reason explicitly about strategies as first order objects. The price to pay for the high expressiveness of SL is that it admits non-behavioral strategies, i.e., a choice of an agent in a play may depend on choices made in another counterfactual play. As the latter moves are unpredictable, these strategies cannot be synthesized in practice. In this talk, we introduce two maximal syntactical fragments of SL admitting behavioral strategies only. As a consequence, we show that the model-checking problem for both fragments is solvable in 2EXPTIME, as it is for the subsumed ATL*.

Abstract

  ATLsc is a powerful formalism for reasoning about multi-agent systems; it is a natural variant of the semantics of the logic ATL, as defined by Alur, Henzinger and Kupferman. Using a translation into QCTL (CTL extended with quantification over atomic propositions), we prove that ATLsc satisfiability is decidable when satisfiability is restricted to turn-based games, or when the set of moves allowed to the players in advance. On the other hand, when strategy quantification is restricted to memoryless strategies, satisfiability is undecidable in all considered cases.

Abstract

  In a global context of formal specification, a theoritecal question is : as for LTL, is it possible to construct an automaton from a tableau-based decision procedure for ATL (Alternating-time Temporal Logic)? To answer that question, we propose a new way of constructing a specific kind of alternating tree automaton, the so called joker automaton, from the construction of the tableau-based decision procedure for ATL [Goranko,Shkatov/2009]. This new automaton recognize all models of a formulae without restrictions on the moves of agents.

Abstract

  We introduce a novel automata-theoretic approach for the verification of multi-agent systems. We present epistemic alternating tree automata, an extension of alternating tree automata, and use them to represent specifications in the temporal epistemic logic CTLK. We show that model check- ing a memory-less interpreted system against a CTLK prop- erty can be reduced to checking the language non-emptiness of the composition of two epistemic tree automata. We report on an experimental implementation and discuss preliminary results. We evaluate the effectiveness of the technique using two real-life scenarios: a gossip protocol and the train gate controller.

Abstract

  We discuss expressivity issues concerning the epistemic mu-calculus with synchronous and perfect recall semantics w.r.t. games with partial observation, alternating temporal logics with incomplete observation, and an extension of the monadic second-order logic on trees.

Abstract

  Modal logic is called "elementary" if it is considered over class of frames definable by a first-order formula. Different formulae lead to different logics, and many of them find their applications in computer science. The aim of the Highlights conference talk is to present a wide picture of the latest research on the satisfiability problem of elementary modal logics. The talk will provide all the necessarily definitions, discuss the motivation, summarise the recent research papers on this topic, and discuss some open problems.

Abstract

  We study the effects of the addition of an equivalence relation to one of the most representative interval temporal logics, namely, the logic ABBbar of Allen's relations "meets", "begun by", and "begins". We first prove that the satisfiability problem for the resulting logic ABBbar-sim remains decidable over finite linear orders, but it becomes nonprimitive recursive, while decidability is lost over $\bbN$. Then, we show that ABBbar-sim is expressive enough to define $\omega{S}$-regular languages.

Abstract

  In this talk, we are interested by expressivity of automaton reading a base b r-tuple of natural numbers. It is well known that those automaton recognize b-recognizable set. We will study how to decide, in polynomial time if the set recognized by an automaton is definable a smaller structure as \FO[+] or \FO[<,\moda], and how to compute a formula in this structure that accepts this set.

Abstract

  From Rabin's tree theorem, one can infer that the monadic second order theory of the lexicographic order on any regular language is decidable. The same holds for deterministic context-free languages since they belong to Caucal's hierarchy. When dropping determinism, not even the first-order theory remains decidable (\'Esik \& Carayol). This talk demonstrates that undecidability occurs already for \begin{itemize} \item small fragments of first-order logic and \item 1-counter automata that are very close to being deterministic. \end{itemize}

Abstract

  Cost monadic logic extends monadic second-order logic with the ability to measure the cardinality of sets and comes with decision procedures for boundedness related questions. We provide new decidability results allowing the systematic investigation of questions involving “relative boundedness”. We first introduce a suitable logic, magnitude monadic logic. We then establish the decidability of this logic over finite words. We finally advocate that developing the proofs in the axiomatic system of “relative internal set theory”, a variant of nonstandard analysis, entails a significant simplification of the proofs.

Abstract

  In this paper, we make a general study of the concept of promptness in parity games that allows to put under a unique theoretical framework several of the cited variants along with new ones. Also, we describe simple polynomial reductions from all these conditions to either Buchi or parity games, which simplify all previous known procedures.

Abstract

  We propose a logical modeling framework, combining a game-theoretic study of the abilities of players to achieve quantitative objectives in multi-player games (optimizing payoffs or preferences on outcomes) with a logical analysis of the abilities of players for achieving qualitative objectives (reaching or maintaining game states with desired properties). We enrich concurrent game models with payoffs for the normal form games associated with each state of the model and propose a quantitative extension of the logic ATL* enabling combination of quantitative and qualitative reasoning.

Abstract

  

Abstract

  11A-2-Sassolas.txt Iterated admissibility is a well-known and important concept in classical game theory, e.g. to determine rational behaviors in multi-player matrix games. As recently shown by Berwanger, this concept can be soundly extended to infinite games played on graphs with omega-regular objectives. In this talk, we study the algorithmic properties of this concept for such games. We settle the exact complexity of natural decision problems on the set of strategies that survive iterated elimination of dominated strategies. As a byproduct of our construction, we obtain automata which recognize all the possible outcomes of such strategies.

Abstract

  We present the first proof system for Coordination Logic (CL). CL provides a logical representation for the distributed realizability problem and extends the game-based temporal logics with quantification over strategies under incomplete information. The proof system is based on a reduction from CL to its decidable fragment. We propose a compositional proof rule which splits a given CL formula into two parts, a decidable CL formula and another, simplified, CL formula. Applying the rule repeatedly transforms the original CL formula into a collection of decidable CL formulas. Our proof system is a complete framework for the synthesis of distributed systems.

Abstract

  Automatic structures are relational structures whose domain can be presented as a regular language and predicates as synchronously regular relations. The main result on automatic structures is an explicit algorithm to build an automaton that accepts any first-order relation, relying on the correspondance between logical connectives and classical operations over automata. In general, building this automaton is non-elementary, but for some automatic structures with elementary first-order theory, we show that this construction has a complexity close to that of the logic.

Abstract

  CTL* formulas can be enriched to express relations between variables whose value can range in a chosen concrete domain. Chosen the appropriate domain one can express quantitative properties that ordinary CTL^* formulas can only approximate through abstraction. We can refer directly to concrete values and describe how they change in time. In this talk we show that satisfiability for CTL* with equality-, order-, and modulo- constraints over the Z is decidable

Abstract

  Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to LTL(F,G) which is the LTL fragment using only modalities F and G. We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae.

Abstract

  We study the problem of generalizing from a finite sample to a language taken from a predefined language class. The two language classes we consider are generated by restricted regular expressions (CHAREs and SOREs) that have significance in the specification of XML documents. For each of the two language classes we give an efficient algorithm returning a minimal generalization from the given finite sample to an element of the fixed language class; such generalizations are called descriptive. In this sense, both our algorithms are optimal.

Abstract

  One challenge in making online education more effective is to develop automatic grading software that can provide meaningful feedback. This paper provides a solution to automatic grading of the standard computation-theory problem that asks a student to construct a deterministic finite automaton from the given description of its language. We focus on how to assign partial grades for incorrect answers. We experimentally show that the tool is able to assign partial grades in a meaningful way, and should be preferred over the human graders for both scalability and consistency.

Abstract

  We introduce streaming tree transducers as an analyzable, executable, and expressive model for transforming unranked ordered trees. Given a linear encoding of the input tree, the transducer makes a single left-to-right pass through the input, and computes the output using a finite-state control, a visibly pushdown stack, and a finite set of variables storing output chunks that can be combined using concatenation and insertion. We prove the model to be equivalent to monadic second-order logic transductions. We show complexity bounds of ExpTime for type-checking and NExpTime for equivalence.

Abstract

   Any two-way finite state automaton is equivalent to some one-way finite state automaton. This well-known result, shown by Rabin and Scott and independently by Shepherdson, states that two-way finite state automata (even non-deterministic) characterize the class of regular languages. It is also known that this result does not extend to finite string transductions: (deterministic) two-way finite state transducers strictly extend the expressive power of (functional) one-way transducers. In particular deterministic two-way transducers capture exactly the class of MSO-transductions of finite strings. In this talk, we address the following definability problem: given a function defined by a two-way finite state transducer, is it definable by a one-way finite state transducer? By extending Rabin and Scott's proof to transductions, we show that this problem is decidable. Our procedure builds a one-way transducer, which is equivalent to the two-way transducer, whenever one exists.

Abstract

  A Mealy automaton is a deterministic, complete, letter-by-letter transducer, with same input and output alphabet. We can consider the semigroup generated by the functions on words induced by its states. We prove that semigroups generated by reversible two-state Mealy automata have remarkable growth properties: they are either finite or free. We give an effective procedure to decide finiteness or freeness of such semigroups when the generating automaton is also invertible.

Abstract

  A nondeterministic automaton is unambiguous if it has at most one accepting run on every input. The class of languages recognisable by unambiguous tree automata is still not well-understood. In this paper we show the following complexity collapse: if A is an unambiguous Buchi tree automaton then L(A) is recognisable by a weak alternating automaton. We present also some extensions of this result. To our best knowledge this is the first parity index collapse that exploits unambiguity of an automaton.

Abstract

   We propose an operation on languages of infinite trees that significantly increases topological complexity but preserves unambiguity. We prove that iterating the operation yields topologically harder and harder sets. As an illustration, we might note that application of the operation to the empty language already produces a non-Borel set, and the next application of the operation produces a set that is outside the sigma-field generated by analytic sets. Moreover, we show how to perform a limit step of the iteration.

Abstract

  In this talk, I will give a game semantics for a paraconsistent logic, and define a paraconsistent "win" - parallel to the paraconsistent understanding of truth.

Abstract

  Expressive completeness, which is one of the themes in this field of research, compares the power of these logics to fragments of first-order logic over some class of frames. If logic is as expressive as first order logic, as logic US (with connectives Until, Since) is shown to be, it is as powerful as possible. It can express the same statements, but in a more concise and readable way. In this presentation I will show a method of proving expressive completeness of a temporal logic by the use of games. This will be demonstrated on example of a temporal logic with connectives Future and Past.

Abstract

  We consider TPTL(Z) and MTL(Z) whose semantics are based on nonmonotonic data words in which every point is assigned a natural number as its weight. We define a weighted version of the EF game on MTL. Using these games, we prove the following: 1. TPTL(Z) is strictly more expressive than MTL(Z). 2. The until hierarchy and the constant hierarchy are strict for MTL(Z). 3. It is undecidable whether a given TPTL(Z) formula can be expressed in MTL(Z).

Abstract

  One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that weak simulation preorder is decidable for OCN. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, and so are weak (and strong) trace inclusion.

Abstract

  A one counter net is a one counter automaton without possibility of testing 0 value. We proved that solving the simulation problem for one counter nets is P-SPACE complete.

Abstract

  

Abstract

  

Abstract

  

Abstract

   In this work, we focus on control of Markov decision processes with non-negative real-valued costs. We develop an algorithm to design a control strategy that guarantees the satisfaction of a correctness specification expressed as a formula of Linear Temporal Logic, while at the same time minimizing the expected average cost between two consecutive satisfactions of a desired property. The existing solutions to this problem in control theory are sub-optimal. By leveraging ideas from automata-based model checking and game theory, we provide an optimal solution.

Abstract

  We provide the first assume-guarantee reasoning for stochastic continuous-time systems. Interactive Markov chains (IMC) are compositional behavioural models similar to continuous-time Markov decision processes. Given a time-bounded property, an IMC component and a specification of the environment, we synthesize a scheduler optimizing the probability that the property is satisfied when the IMC is working in an unknown environment that satisfies the specification. In this talk we focus on a two-player continuous-time stochastic game model that we call controller-environment games that is the crucial step in the solution of the problem above.

Abstract

  Janin and Walukiewicz showed that the modal mu-calculus MC is the bisimulation-invariant fragment of monadic second-order logic MSO. Their proof uses parity automata with a transition map defined in terms of monadic first-order logic. We decompose their proof in three parts: (1) automata-theoretic characterizations of MSO and MC respectively, (2) a simple model-theoretic characterization of the identity-free fragment of monadic first-order logic, and (3) a coalgebraic result, stating that the second result propagates from the `one-step level' to the level of full fixpoint logics.

Abstract

  We offer a coalgebraic perspective on the k-regular sequences. For any k >= 1 and semiring S, the set of sequences with output in S is the carrier of a final coalgebra. This allows us to give a coalgebraic characterization of the k-regular sequences. Using an isomorphism based on a bijective numeration system, we thus obtain a structural correspondence between S-rational series over k nonterminals, and k-regular sequences with output in S. We will furthermore discuss a connection with sequences definable by divide and conquer recurrences.

Abstract

  We discuss complexity theoretic results in the context of Combinatory Logic Synthesis which is a new approach to component-based synthesis using type inhabitation. The complexity theoretic reductions behind these results establish explicit and effective connections between combinatory logic inhabitation and automata theoretic models, in the form of alternating tree automata and alternating space bounded Turing machines. These computational models that are commonly found in automata theoretic approaches are related to synthesis based on logics within the MSO family of logics.

Abstract

  We describe the role epistemic reasoning can play in concurrency theory. The idea of using modalities as programming constructs has been largely unexplored. We add epistemic and spatial modalities as part of the programming language, not just as part of the meta-language to reason about protocols. We introduce spatial and epistemic process calculi to reason about information and knowledge distributed among agents in a system. We give domain-theoretic structures to represent this information, operational and denotational means to reason about possibly infinite behavior, and compact versions of infinite objects to simulate public announcement.