ABSTRACT. I will survey a body of work, developed over the past decade or so, on algorithms for, and the computational complexity of, analyzing and model checking some important families of countably infinite-state Markov chains, Markov decision processes (MDPs), and stochastic games. These models arise by adding natural forms of recursion, branching, or a counter, to finite-state models, and they correspond to probabilistic/control/game extensions of classic automata-theoretic models like pushdown automata, context-free grammars, and one-counter automata. They subsume some classic stochastic processes such as multi-type branching processes and quasi-birth-death processes. They also provide a natural model for probabilistic procedural programs with recursion.

Some of the key algorithmic advances for analyzing these models have come from algorithms for computing the least fixed point (and greatest fixed point) solution for corresponding monotone systems of nonlinear (min/max)-polynomial equations. Such equations provide, for example, the Bellman optimality equations for optimal extinction and reachability probabilities for branching MDPs (BMDPs). A key role in these algorithms is played by Newton’s method, and by a generalization of Newton’s method which is applicable to the Bellman equations for BMDPs, and which uses linear programming in each iteration.

By now, polynomial time algorithms have been developed for some of the key problems in this domain, while other problems have been shown to have high complexity, or to even be undecidable. Yet many algorithmic questions about these models remain open. I will highlight some of the open questions.

(This talk partly describes joint work with Alistair Stewart and Mihalis Yannakakis.)

ABSTRACT. Calude et al. have given the first algorithm for solving parity games in quasi-polynomial time, where previously the best algorithms were mildly subexponential. We combine the succinct counting technique of Calude et al. with the small progress measure technique of Jurdzinski. Our contribution is two-fold: we provide an alternative exposition of the ideas behind the groundbreaking quasi-polynomial algorithm of Calude et al., and we use it to reduce the space required from quasi-polynomial to nearly linear.

ABSTRACT. We study countably infinite MDPs with parity objectives, and special cases with a bounded number of colors in the Mostowski hierarchy (including reachability, safety, Buchi and co-Buchi).

In finite MDPs there always exist optimal memoryless deterministic (MD) strategies for parity objectives, but this does not generally hold for countably infinite MDPs. In particular, optimal strategies need not exist.

For countable infinite MDPs, we provide a complete picture of the memory requirements of optimal (resp., ε-optimal) strategies for all objectives in the Mostowski hierarchy.

In particular, there is a strong dichotomy between two different types of objectives. For the first type, optimal strategies, if they exist, can be chosen MD, while for the second type optimal strategies require infinite memory. (I.e., for all objectives in the Mostowski hierarchy, if finite-memory randomized strategies suffice then also MD strategies suffice.) Similarly, some objectives admit ε-optimal MD-strategies, while for others ε-optimal strategies require infinite memory. Such a dichotomy also holds for the subclass of countably infinite MDPs that are finitely branching, though more objectives admit MD-strategies here.

ABSTRACT. We demonstrate the usefulness of adding delay to infinite games with quantitative winning conditions. In a delay game, one of the players may delay her moves to obtain a lookahead on her opponent's moves. We show that determining the winner of delay games with winning conditions given by parity automata with costs is EXPTIME-complete and that exponential bounded lookahead is both sufficient and in general necessary. Thus, although the parity condition with costs is a quantitative extension of the parity condition, our results show that adding costs does not increase the complexity of delay games with parity conditions.

Furthermore, we study a new phenomenon that appears in quantitative delay games: lookahead can be traded for the quality of winning strategies and vice versa. We determine the extent of this tradeoff. In particular, even the smallest lookahead allows to improve the quality of an optimal strategy from the worst possible value to almost the smallest possible one. Thus, the benefit of introducing lookahead is twofold: not only does it allow the delaying player to win games she would lose without, but lookahead also allows her to improve the quality of her winning strategies in games she wins even without lookahead.

ABSTRACT. Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory cannot support higher-order functions, that is, the category of measurable spaces is not cartesian closed.

Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form an extensional category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.

ABSTRACT. We present a categorical construction for modelling both definite and indefinite causal structures within a general class of process theories that include classical probability theory and quantum theory. Unlike prior constructions within categorical quantum mechanics, the objects of this theory encode fine-grained causal relationships between subsystems and give a new method for expressing and deriving consequences for a broad class of causal structures. To illustrate this point, we show that this framework admits processes with definite causal structures, namely one-way signalling processes, non-signalling processes, and quantum n-combs, as well as processes with indefinite causal structure, such as the quantum switch and the process matrices of Oreshkov, Costa, and Brukner. We furthermore give derivations of the operational behaviour of these processes using simple, diagrammatic axioms.

ABSTRACT. We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-L\"{o}f type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates for identity types. As an application, we show a relational parametricity result on homotopy type theory. As a corollary, it follows that every polymorphic endofunction on a loop space is homotopic to some iterated concatenation of a loop.

ABSTRACT. In previous work we have described the construction of an abstract lattice from a given Buchi automaton. The abstract lattice is finite and has the following key properties. (i) There is a Galois insertion between it and the 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 $\omega$-iterations (but not in general greatest fixpoints) can be computed on the level of the abstract lattice.

This allows one to decide whether finite and infinite traces of first-order recursive boolean programs are accepted by the automaton and can further be used to derive a type-and-effect system for infinitary properties.

In this paper, we show how to derive from the abstract lattice a cartesian-closed category with fixpoint operator in such a way that the interpretation of a *higher-order* recursive program yields precisely the abstraction of its set of finite and infinite traces and thus provides a new algorithm for the higher-order model checking problem for trace properties.

All previous algorithms for higher-order model checking work inherently on arbitrary tree properties and no apparent simplification appears when instantiating them with trace properties. The algorithm presented here, while necessarily having the same asymptotic complexity, is considerably simpler since it merely involves the interpretation of the program in a cartesian-closed category.

The construction of the cartesian closed category from a lattice is new as well and may be of independent interest.

ABSTRACT. This paper studies sets of rational numbers definable by continuous Petri nets and extensions thereof. First, we identify a polynomial-time decidable fragment of existential FO(Q, +, <) and show that the sets of rationals definable in this fragment coincide with reachability sets of continuous Petri nets. Next, we introduce and study continuous vector addition systems with states (CVASS), which are vector addition systems with states in which counters may hold non-negative rational values, and in which the effect of a transition can be scaled by a positive rational number smaller or equal to one. This class strictly generalizes continuous Petri nets by additionally allowing for discrete control-state information. We prove that reachability sets of CVASS are equivalent to the sets of rational numbers definable in existential FO(Q, +, <) from which we can conclude that reachability in CVASS is NP-complete. Finally, our results explain and yield as corollaries a number of polynomial-time algorithms for decision problems that have recently been studied in the literature.

ABSTRACT. The regular separability problem asks, for two given languages, if there exists a regular language including one of them but disjoint from the other. Our main result is decidability, and pspace-completeness, of the regular separability problem for languages of one counter automata without zero tests (also known as one counter nets). This contrasts with undecidability of the regularity problem for one counter nets, and with undecidability of the regular separability problem for one counter automata, which is our second result.

ABSTRACT. The dot-depth hierarchy of Brzozowski and Cohen is a classification of all first-order definable languages. It rose to prominence following the work of Thomas, who established an exact correspondence with the quantifier alternation hierarchy of first-order logic: each level contains all languages that can be defined with a maximal number of quantifier blocks. One of the most famous open problems in automata theory is to obtain membership algorithms for all levels in this hierarchy.

For a fixed level, the membership problem asks whether an input regular language belongs to this level. Despite a significant research effort, membership by itself has only been solved for the lower levels. Recently, a breakthrough has been made by replacing membership with a more general problem: separation. Separation asks whether, for two input languages, there exists a third one in the investigated level containing the first language and disjoint from the second. The motivation for looking at separation is threefold: (1) while more difficult, it is more rewarding; (2) being more general, it provides a more convenient framework, and (3) all recent membership algorithms are actually reductions to separation for lower levels.

This paper presents a separation algorithm for dot-depth 2. A~crucial point is that while dot-depth 2 is our main application, we prove a much more general theorem. Indeed, dot-depth belongs to a family of hierarchies which all share the same generic construction process: starting from an initial class of languages called the basis, one applies generic operations to build new levels. We prove that for any concatenation hierarchy whose basis is a finite class, level 1 has decidable separation. In the special case of dot-depth, this generic result can easily be lifted to level 2.

ABSTRACT. We introduce a notion of higher-order parity automaton which extends to the infinitary simply-typed lambda-calculus the traditional notion of parity tree automaton on infinitary ranked trees. Our main result is that the acceptance of an infinitary lambda-term by a higher-order parity automaton is decidable, whenever the infinitary lambda-term is generated by a finite and simply-typed lambda-Y-term. The decidability theorem is established by combining ideas coming from denotational semantics and from infinitary rewriting theory.

ABSTRACT. Quantitative algebras (QAs) are algebras over metric spaces defined by quantitative equational theories as introduced by us in 2016. They provide the mathematical foundation for metric semantics of probabilistic, stochastic and other quantitative systems. This paper considers the issue of axiomatizability of QAs. We investigate the entire spectrum of types of quantitative inferences that can be used to axiomatize theories: (i) simple quantitative equations; (ii) Horn clauses with no more than c equations between variables as hypotheses, where c is a cardinal and (iii) the most general case of Horn clauses. In each case we characterize the class of QAs and prove variety/quasivariety theorems that extend and generalize classical results from model theory for algebras and first-order structures.

ABSTRACT. In many instances in first order logic or computable algebra, classical theorems show that many problems are undecidable for general structures, but become decidable if some rigidity is imposed on the structure. For example, the set of theorems in many finitely axiomatisable theories is nonrecursive, but the set of theorems for any finitely axiomatisable complete theory is recursive. Finitely presented groups might have an nonrecursive word problem, but finitely presented simple groups have a recursive word problem.

In this article we introduce a topological framework based on closure spaces to show that many of these proofs can be obtained in a unified setting. We will show in particular that these statements can be generalized to cover arbitrary structures, with no finite or recursive presentation/axiomatization. This generalizes in particular work by Kuznetsov and others.

Examples from first order logic and symbolic dynamics will be discussed at length.

ABSTRACT. \emph{Final coalgebras} as ``categorical greatest fixed points'' play a central role in the theory of coalgebras. Somewhat analogously, most proof methods studied therein have focused on \emph{greatest} fixed-point properties like safety and bisimilarity. Here we make a step towards categorical proof methods for \emph{least} fixed-point properties over dynamical systems modeled as coalgebras. Concretely, we seek a categorical unification of typical (conventional) proof methods for termination and liveness, namely \emph{ranking functions} (in nondeterministic settings) and \emph{ranking supermartingales} (in probabilistic ones). We find an answer in a suitable combination of: coalgebraic simulation (studied previously by the authors); and \emph{corecursive algebra} as a classifier for (non-)well-foundedness.

ABSTRACT. Brunet and Pous showed at LICS 2015 that the equational theory of identity-free relational Kleene lattices (a fragment of Kleene allegories) is decidable in EXPSPACE. In this paper, we show that the equational theory of Kleene allegories is decidable, and is EXPSPACE-complete, answering the first open question posed by their work. The proof proceeds by designing partial derivatives on graphs, which are generalization of partial derivatives on strings for regular expressions called Antimirov's partial derivatives. The partial derivatives on graphs give a finite automata construction algorithm as with the partial derivatives on strings.

ABSTRACT. We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation, as embodied by process algebras like the pi-calculus. The introduced model is formulated as a token machine, in which not one but multiple tokens are allowed to traverse the underlying net at the same time. We prove soundness and adequacy of the introduced model. The former is proved as a simulation result between the token machines one obtains along reduction. The latter is obtained by a fine analysis of termination both in nets and in token machines.

ABSTRACT. Compute the coarsest simulation preorder included in an initial preorder is used to reduce the resources needed to analyze a given transition system. This technique is applied on many models like Kripke structures, labeled graphs, labeled transition systems or even word and tree automata. Let $(Q,\rightarrow)$ be a given transition system and $\mathscr{R}_{\mathrm{init}}$ be an initial preorder over $Q$. Until now, algorithms to compute $\mathscr{R}_{\mathrm{sim}}$, the coarsest simulation included in $\mathscr{R}_{\mathrm{init}}$, are either memory efficient either time efficient but not both. In this paper we propose the foundation for a series of efficient simulation algorithms with the introduction of the notion of maximal transitions and the notion of stability of a preorder with respect to a coarser one. As an illustration we solve an open problem by providing the first algorithm with the best published time complexity, $O(|P_{\mathrm{sim}}|.|{\rightarrow}|)$, and a bit space complexity in $O(|P_{\mathrm{sim}}|^2.\log(|P_{\mathrm{sim}}|) +|Q|.\log(|Q|))$, with $P_{\mathrm{sim}}$ the partition induced by $\mathscr{R}_{\mathrm{sim}}$.

ABSTRACT. Negotiation diagrams are a model of concurrent computation akin to van der Aalst's workflow Petri nets. Deterministic negotiation diagrams, a class equivalent to the much studied and used free-choice workflow Petri nets, is surprisingly amenable to verification. First, deciding soundness (a property close to deadlock-freedom) can be solved in PTIME. Next, for sound deterministic negotiations, such fundamental questions like computing summaries or the expected cost, can be solved in PTIME too, while they are PSPACE-complete in the general case. In this paper we generalize and explain these results. We extend the classical ``meet-over-all-paths'' (MOP) formulation of static analysis problems to our concurrent setting, and introduce Mazurkiewicz-invariant analysis problems, a class encompassing the questions above and new ones.

We show that the complexity of an arbitrary Mazurkiewicz-invariant analysis problem is in PTIME for sound deterministic negotiations whenever it is in PTIME for sequential flow-graphs; even though the flow-graph of a deterministic negotiation can be exponentially larger than the negotiation itself. This gives a common explanation to the low-complexity of all the analysis questions studied so far. We show that classical gen/kill analyses are also an instance of our framework. As a special case we obtain a PTIME algorithm for detecting anti-patterns in free-choice workflow Petri nets.

Our result is based on a novel decomposition theorem, of independent interest, showing that sound deterministic negotiations can be hierarchically decomposed into, possibly overlapping, sound deterministic negotiations of particularly simple shapes.

ABSTRACT. Stable event structures, and their duality with prime algebraic domains (arising as partial orders of configurations), are a landmark of concurrency theory, providing a clear characterisation of causality in computations. They have been used for defining a concurrent semantics of several formalisms, from Petri nets to linear graph rewriting systems, which in turn lay at the basis of many visual frameworks. Stability however is restrictive for dealing with formalisms where a computational step can merge parts of the state, like graph rewriting systems with non-linear rules, which are needed to cover some relevant applications (such as the graphical encoding of calculi with name passing). We characterise, as a natural generalisation of prime algebraic domains, a class of domains that is well-suited to model the semantics of formalisms with fusions. We then identify a corresponding class of event structures, that we call connected event structures, via a duality result formalised as an equivalence of categories. We show that connected event structures are exactly the class of event structures the arise as the semantics of non-linear graph rewriting systems. Interestingly, the category of general unstable event structures coreflects into our category of domains, so that our result provides a characterisation of the partial orders of configurations of such event structures.

ABSTRACT. In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recursion construct. A lean congruence preserves equivalence when replacing closed subexpressions of a process by equivalent alternatives. A full congruence moreover allows replacement within a recursive specification of subexpressions that may contain recursion variables bound outside of these subexpressions.

I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Additionally, it is a full congruence for the tyft/tyxt format.

ABSTRACT. Descriptive Complexity has been very successful in characterizing complexity classes of decision problems in terms of the properties definable in some logics. However, descriptive complexity for counting complexity classes, such as FP and #P, has not been systematically studied, and it is not as developed as its decision counterpart. In this paper, we propose a framework based on Weighted Logics to address this issue. Specifically, by focusing on the natural numbers we obtained a logic called Quantitative Second Order Logics (QSO), and show how some of its fragments can be used to capture fundamental counting complexity classes such as FP, #P and FPSPACE, among others. We also use QSO to define a hierarchy inside #P, identifying counting complexity classes with good closure and approximation properties, and which admit natural complete problems. Finally, we add recursion to QSO, and show how this extension naturally captures lower counting complexity classes such as #L.

ABSTRACT. We prove that the solvability of systems of linear equations and related linear algebraic properties are definable in a fragment of fixed-point logic with counting that only allows polylogarithmically many iterations of the fixed-point operators. This allows us to separate the descriptive complexity of solving linear equations from full fixed-point logic with counting by logical means. As an application of these results, we separate an extension of first order logic with a rank operator from fixed-point logic with counting, solving an open problem due to Holm [PhD thesis, Cambridge University, 2010].

We then draw a connection between this work in descriptive complexity theory to graph isomorphism testing and propositional proof complexity. Answering an open question from [Berkholz and Grohe, ICALP 2015], we separate the strength of certain algebraic graph-isomorphism tests. This result can also be phrased as a separation of the algebraic propositional proof systems "Nullstellensatz" and "monomial PC".

ABSTRACT. We study the descriptive complexity of summation problems in Abelian groups and semigroups. In general, an input to the summation problem consists of an Abelian semigroup G, explicitly represented by its multiplication table, and a subset X of G, and the task is to determine the sum over all elements of X.

Algorithmically this is a very simple problem. If the elements of X come in some order, then we can process these elements along that order and calculate the sum in a trivial way. However, what makes this fundamental problem so interesting for us is that from the viewpoint of logical definability its tractability is much more delicate. If we consider the semigroup as an abstract structure and X as an abstract set, without a linear order and hence without a canonical way to process the elements of X one by one, then it is unclear how to define the sum in any logic that does not have the power to quantify over a linear order. Indeed the trivial summation algorithm cannot be expressed in any polynomial-time logic or, in fact, in any computational model which works on abstract mathematical structures in an isomorphism-invariant way without violating polynomial resource bounds.

The surprising difficulty, in terms of logical definability, of this basic mathematical problem is the reason why Ben Rossman asked, more than ten years ago, whether it can be expressed in the logic Choiceless Polynomial Time (CPT). Note that, to date, CPT is one of the most powerful known candidates for a logic that might be capable of defining every polynomial-time property of finite structures.

In this paper we clarify the status of the definability for the summation problem for Abelian groups and semigroups in important polynomial-time logics. In our first main result we show that the problem can be defined in fixed-point logic with counting (FPC). Since FPC is contained in CPT this settles Rossman's question. Our proof is based on a dynamic programming approach and heavily uses the counting mechanism of FPC. In our second main result we give a matching lower bound and show that the use of counting operators cannot be avoided: the summation problem, even over Abelian groups, cannot be defined in pure fixed-point logic without counting. Our proof here is based on a probabilistic argument.

ABSTRACT. The question of whether there is a logic that captures polynomial time is one of the main open problems in descriptive complexity theory and database theory. In 2010 Grohe showed that fixed point logic with counting captures polynomial time on all classes of graphs with excluded minors. We now consider classes of graphs with excluded induced subgraphs. For such graph classes, an effective graph decomposition, called modular decomposition, was introduced by Gallai in 1976. The graphs that are non-decomposable with respect to modular decomposition are called prime. We present a tool, the Modular Decomposition Theorem, that reduces (definable) canonization of a graph class C to (definable) canonization of the class of prime graphs of C that are colored with binary relations on a linearly ordered set. By an application of the Modular Decomposition Theorem, we show that fixed point logic with counting also captures polynomial time on the class of permutation graphs. As a side effect of the Modular Decomposition Theorem, we further obtain that the modular decomposition tree is computable in logarithmic space. It follows that cograph recognition and cograph canonization is computable in logarithmic space.

ABSTRACT. We show that the ellipsoid method for solving semi-definite programs (SDPs) can be expressed in fixed-point logic with counting (FPC). This generalizes an earlier result that the optimal value of a linear program can be expressed in this logic.

As an application, we establish Lasserre lower bounds for a large class of optimization problems, namely those that can be expressed as finite-valued constraint satisfaction problems (VCSPs). In particular, we establish a dichotomy on the number of levels of the Lasserre hierarchy that are required to solve the problem exactly. We show that if a finite-valued constraint problem is not solved exactly by its basic linear programming relaxation, it is also not solved exactly by any sub-linear number of levels of the Lasserre hierarchy.

The lower bounds are established through logical undefinability results. We show that the SDP corresponding to any fixed level of the Lasserre hierarchy is interpretable in a VCSP instance by means of FPC formulas. Our definability result of the ellipsoid method then implies that the solution of this SDP can be expressed in this logic. Together, these results give a way of translating lower bounds on the number of variables required in counting logic to express a VCSP into lower bounds on the number of levels required in the Lasserre hierarchy to eliminate the integrality gap.

As a special case, we obtain the same dichotomy for the class of $\MAXCSP$ problems, generalizing some earlier Lasserre lower bound results by Schoenebeck. Recently, a similar linear lower bound in the Lasserre hierarchy for general-valued VCSPs has also been announced by Thapper and \v{Z}ivn\'y, using different techniques.