ABSTRACT. Multi-agents games are extensively used for modelling settings in which different entities share resources. For example, the setting in which entities need to route messages in a network is modelled by network-formation games: the network is modelled by a graph, and each agent has to select a path satisfying his reachability objective. In practice, the objectives of the entities are often more involved than reachability. The need to specify and reason about rich specifications has been extensively studied in the context of verification and synthesis of reactive systems. The talk describes a lifting of ideas from formal methods to multi-agent games. For example, in network-formation games with regular objectives, the edges of the graph are labeled by alphabet letters and the objective of each player is a regular language over the alphabet of labels. Thus, beyond reachability, a player may restrict attention to paths that satisfy certain properties, referring, for example, to the providers of the traversed edges, the actions associated with them, their quality of service, security, etc.

The talk assumes no previous knowledge in game theory. We will introduce the basic concepts and problems, describe how their extension to games with more expressive specification of objectives poses new challenges, and study the resulting games.

Joint work with Guy Avni and Tami Tamir.

ABSTRACT. We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zero-reachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error eps > 0 in time which is polynomial in log(eps), exponential in the size of a given pMC, and doubly exponential in the number of counters. In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter. Here we show that the qualitative zero-reachability is decidable and SquareRootSum-hard, and the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error eps > 0 (these result applies to pMC satisfying a suitable technical condition that can be verified in polynomial time). The proof techniques invented in the second case allow to construct counterexamples for some classical results about ergodicity in stochastic Petri nets.

ABSTRACT. Ground Tree Rewrite Systems with State are known to have an undecidable control state reachability problem. Taking inspiration from the recent introduction of scope-bounded multi-stack pushdown systems, we define Senescent Ground Tree Rewrite Systems. These are a restriction of ground tree rewrite systems with state such that nodes of the tree may no longer be rewritten after having witnessed an a priori fixed number of control state changes. As well as generalising scope-bounded multi-stack pushdown systems, we show --- via reductions to and from reset Petri-nets --- that these systems have an Ackermann-complete control state reachability problem. However, reachability of a regular set of trees remains undecidable.

ABSTRACT. We describe the construction of an abstract lattice from a given Buchi automata. The abstract lattice is finite and has the following key properties. (i) There is a Galois connection between the (infinite) lattice of languages of finite and infinite words over a given alphabet. (ii) The abstraction is faithful with respect to acceptance by the automaton. (iii) Least fixpoints and w-iterations (but not in general greatest fixpoints) can be computed on the level of the abstract lattice.

This allows one to develop an abstract interpretation capable of checking whether finite and infinite traces of a (recursive) program are accepted by a policy automaton. It is also possible to cast this analysis in the form of a type and effect system with the effects being elements of the abstract lattice.

While the resulting decidability and complexity results are known (regular model checking for pushdown systems) the abstract lattice provides a new point of view and enables smooth integration with data types, objects, higher-order functions which are best handled with abstract interpretation or type systems.

We demonstrate this by generalising our type-and-effect systems to object-oriented programs and higher-order functions.

ABSTRACT. Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking first-order separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words.

ABSTRACT. Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for equivalences of different kinds of systems. Even before Milner introduced and applied such methods in his work on CCS, Hopcroft and Karp used up-to techniques to check equivalence of deterministic automata.

In this work, we prove the soundness of such techniques in an abstract fibrational setting building on the seminal work of Hermida and Jacobs. To do this in a modular way we generalise Pous and Sangiorgi's notion of \emph{compatibility}. This allows us to systematically prove the soundness of up-to techniques, not only for bisimilarity but for a large class of coinductive predicates modeled as coalgebras. By tuning the parameters of our framework, we obtain novel proof techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity.

ABSTRACT. We study two refinements of the linear π-calculus that ensure deadlock freedom (the absence of stable states with pending linear communications) and lock freedom (the eventual completion of pending linear communications). The main feature of both type systems is a new form of channel polymorphism that affects their accuracy in a significant way: they are the first of their kind that can deal with recursive processes communicating in cyclic network topologies.

ABSTRACT. We consider two-player non zero-sum infinite duration games played on weighted graphs. We extend the notion of secure equilibrium introduced by Chatterjee et al., from the Boolean setting to this quantitative setting. As for the Boolean setting, our notion of secure equilibrium refines the classical notion of Nash equilibrium. We prove that secure equilibria always exist in a large class of weighted games which includes common measures like sup, inf, lim sup, lim inf, mean-payoff, and discounted sum. Moreover we show that it is possible to synthesize such strategy profiles that are finite-memory and use few memory. Finally, we prove that the constrained existence problem for secure equilibria is decidable for sup, inf, lim sup, lim inf and mean-payoff measures. Our solutions rely on new results for zero-sum quantitative games with lexicographic objectives that are interesting on their own right.

ABSTRACT. We investigate the existence of certain types of equilibria (Nash, epsilon-Nash, subgame perfect, epsilon-subgame perfect) in infinite sequential games with real-valued payoff functions depending on the class of payoff functions (continuous, upper semi-continuous, Borel) and whether the game is zero-sum. Our results hold for games with two or up to countably many players.

Several of these results are corollaries of stronger results that we establish about equilibria in infinite sequential games with some weak conditions on the occurring preference relations. We also formulate an abstract equilibrium transfer result about games with compact strategy spaces and open preferences. Finally, we consider a dynamical improvement rule for infinite sequential games with continuous payoff functions.

ABSTRACT. Regular cost functions provide a quantitative extension of regular languages that retains most of their important properties, such as expressive power and decidability, at least over finite and infinite words and over finite trees. Much less is known over infinite trees.

We consider cost functions over infinite trees defined by an extension of weak monadic second-order logic with a new fixed-point-like operator. We show this logic to be decidable, improving previously known decidability results for cost logics over infinite trees. The proof relies on an equivalence with a form of automata with counters called quasi-weak cost automata, as well as results about converting two-way alternating cost automata to one-way alternating cost automata.

ABSTRACT. Weighted automata are a conservative quantitative extension of finite automata that enjoys applications, e.g., in language processing and speech recognition. Their expressive power, however, appears to be limited when they are applied to more general structures than words, such as graphs. To address this drawback, weighted automata have recently been generalized to weighted pebble walking automata, which proved useful as a tool for the specification and evaluation of quantitative properties over words and nested words. In this paper, we establish the expressive power of weighted pebble walking automata in terms of transitive closure logic, lifting a similar result by Engelfriet and Hoogeboom from the boolean case to a quantitative setting. This result applies to a general class of graphs that subsumes all the aforementioned classes.

ABSTRACT. The hypergraph duality problem DUAL is defined as follows: given two simple hypergraphs G and H, decide whether H consists precisely of all minimal transversals of G (in which case we say that G is the dual of H). This problem is equivalent to decide whether two given non-redundant monotone DNFs are dual. It is known that non-DUAL, the complementary problem to DUAL, is in GC(log² n,PTIME), where GC(f(n),C) denotes the complexity class of all problems that after a nondeterministic guess of O(f(n)) bits can be decided (checked) within complexity class C. It was conjectured that non-DUAL is in GC(log² n,LOGSPACE).

In this paper we prove this conjecture and actually place the non-DUAL problem into the complexity class GC(log² n,TC⁰) which is a subclass of GC(log² n,LOGSPACE). We here refer to the logtime-uniform version of TC⁰, which corresponds to FO(COUNT), i.e., first order logic augmented by counting quantifiers. We achieve the latter bound in two steps. First, based on existing problem decomposition methods, we develop a new nondeterministic algorithm for non-DUAL that requires to guess O(log² n) bits. We then proceed by a logical analysis of this algorithm, allowing us to formulate its deterministic part in FO(COUNT).

ABSTRACT. The modal $\mu$-calculus, introduced by Dexter Kozen in 1981, is among the best known temporal logics studied in the theory of verification. Despite 30 years of continuous efforts, the exact complexity of its model checking problem remains elusive, and the question whether the problem can be solved in polynomial time is still unsolved.

Most work in the literature uses a game- or automata theoretic approach by reducing the model checking problem to the problem of solving parity games, a two-player game in which the formula and the transition system is combined into a single game arena.

In this paper we take a different route and study the model checking problem directly, keeping the formula and the transition system separate. This allows us to develop logical tools which manipulate the formula only and thereby studying the problem within the framework of parameterized complexity. This approach has been very successful for first- or monadic second-order logic, for instance in the work on algorithmic meta theorems.

As the main logical result of this paper we develop decomposition- or splitter-theorems for the modal $\mu$-calculus in the style of Feferman-Vaught theorems for FO and MSO. In particular, we show that if a transition system $M$ is composed of the union of two systems $M_1 \cup M_2$, then the truth of $L_\mu$-formulas at a node in $M$ essentially only depends on the truth of suitable formulas in the two systems $M_1$ and $M_2$. This result even applies to the much more general case where we allow additional edges in $M$ which start in $M_1$ and end in $M_2$.

As an algorithmic consequence we get that $L_\mu$ model-checking is fixed-parameter tractable on various classes of transition systems such as transition systems of bounded directed path width and bounded Kelly-width. To the best of our knowledge, these are among the first FPT-results for $L_\mu$ that do not follow immediately from tractability of monadic second-order logic.

ABSTRACT. We consider the two-variable fragment of first-order logic with counting quantifiers, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NExpTime-complete.

ABSTRACT. We present the first method for reasoning about temporal logic properties of higher-order, infinite-data programs. By distinguishing between the finite traces and infinite traces in the specification, we obtain rules that permit us to reason about the temporal behavior of program parts via a type-and-effect system, which is then able to compose these facts together to prove the overall target property of the program. The type system alone is strong enough to derive many temporal safety properties, for example when using refinement types and temporal effects. We also show how existing techniques can be used as oracles to provide liveness information (e.g. termination) about program parts and that the type-and-effect system can combine this information with temporal safety information to derive nontrivial temporal properties. Our work has application toward verification of higher-order software, as well as modular strategies for procedural programs.

ABSTRACT. Abstract interpretation is a theory of abstraction and constructive approximation of the mathematical structures used in the formal description of complex or infinite systems and the inference or verification of their combinatorial or undecidable properties.  Developed in the late seventies, it has been since then used, implicitly or explicitly, to many aspects of computer science (such as static analysis and verification, contract inference, type inference, termination inference, model-checking, abstraction/refinement, program transformation (including watermarking, obfuscation, etc), combination of decision procedures, security, malware detection, database queries, etc) and more recently, to system biology and SAT/SMT solvers.  Production-quality verification tools based on abstract interpretation are available and used in the advanced software, hardware, transportation, communication, and medical industries.

The talk will consist in an introduction to the basic notions of abstract interpretation and the induced methodology for the systematic development of sound abstract interpretation-based tools. Examples of abstractions will be provided, from semantics to typing, grammars to safety, reachability to potential/definite termination, numerical to protein-protein abstractions, as well as applications (including those in industrial use) to software, hardware and system biology.

This paper is a general discussion of abstract interpretation, with selected publications, which unfortunately are far from exhaustive both in the considered themes and the corresponding references.