ABSTRACT. Symbolic automata extend classic finite state automata by allowing transitions to carry predicates over rich alphabet theories. The key algorithmic difference to classic automata is the ability to efficiently operate over very large or infinite alphabets. In this talk we give an overview of what is currently known about symbolic automata, what their main applications are, and what challenges arise when reasoning about them. We also discuss some of the open problems and research directions in symbolic automata theory.

ABSTRACT. Graph games with ω-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify ω-regular winning conditions. Graph games with parity conditions are equivalent to μ-calculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finite-state systems, as well as algorithms for the analysis of infinite-state systems with finite quotient. A set-based symbolic algorithm uses the basic set operations and the one-step predecessor operators. We consider graph games with n vertices and parity conditions with c priorities (equivalently, a μ-calculus formula with c alternations of least and greatest fixed points). While many explicit algorithms exist for graph games with parity conditions, for set-based symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires O(n^c) symbolic operations and linear space; and (b) an improved algorithm that requires O(n^{c/2+1}) symbolic operations but also O(n^{c/2+1}) space (i.e., exponential space). In this work we present two set-based symbolic algorithms for parity games: (a) our first algorithm requires O(n^{c/2+1}) symbolic operations and only requires linear space; and (b) developing on our first algorithm, we present an algorithm that requires O(n^{c/3+1}) symbolic operations and only linear space. We also present the first linear space set-based symbolic algorithm for parity games that requires at most a sub-exponential number of symbolic operations.

ABSTRACT. For a regular cardinal κ, a formula of the modal μ-calculus is κ-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of κ-directed sets. We define the fragment C_\aleph1 (x) of the modal μ-calculus and prove that all the formulas in this fragment are \aleph1-continuous. For each formula φ(x) of the modal μ-calculus, we construct a formula ψ(x) ∈ C_\aleph1(x) such that φ(x) is κ-continuous, for some κ, if and only if φ(x) is equivalent to ψ(x). Consequently, we prove that (i) the problem whether a formula is κ-continuous for some κ is decidable, (ii) up to equivalence, there are only two fragments determined by continuity at some regular cardinal: the fragment C_\aleph0 (x) studied by Fontaine and the fragment C_\aleph1(x). We apply our considerations to the problem of characterizing closure ordinals of formulas of the modal μ-calculus. An ordinal α is the closure ordinal of a formula φ(x) if its interpretation on every model converges to its least fixed-point in at most α steps and if there is a model where the convergence occurs exactly in α steps. We prove that \omega_1, the least uncountable ordinal, is such a closure ordinal. Moreover we prove that closure ordinals are closed under ordinal sum. Thus, any formal expression built from 0,1,\omega_0,\omega_1 by using the binary operator symbol + gives rise to a closure ordinal.

ABSTRACT. We introduce an extension of modal mu-calculus to sets with atoms and study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show some limitations to the expressiveness of the calculus and argue that a naive way to remove these limitations results in a logic whose model checking is undecidable.

ABSTRACT. A new family of modal logics with an associative binary modality, called counting logics is proposed. These propositional logics allow to express finite cardinalities of sets and more generally to count the number of subsets satisfying some properties. We show that these logics can be seen both as specializations of the Boolean logic of bunched implications and as generalizations of the propositional dependence logic. Moreover, whereas most logics with an associative binary modality are undecidable, we prove that some counting logics are decidable, in particular the basic counting logic bCL. We conjecture that this interesting result is due to the valuation constraints in counting logics' semantics and prove that the logic corresponding to bCL without these constraints is undecidable. Finally, we give lower and upper bounds for the complexity of bCL's validity problem.

ABSTRACT. We introduce a notion of reduction on resource vectors, i.e. infinite linear combinations of resource λ-terms. The latter form the multilinear fragment of the differential λ-calculus introduced by Ehrhard and Regnier, and resource vectors are the target of the Taylor expansion of λ-terms.

We show that the reduction of resource vectors contains the image, through Taylor expansion, of β-reduction in the algebraic λ-calculus, i.e. λ-calculus extended with weighted sums.

We moreover exhibit a class of algebraic λ-terms, having a normalizable Taylor expansion: this subsumes both arbitrary pure λ-terms, and normalizable algebraic λ-terms. We then show that Taylor expansion and normalization commute.

ABSTRACT. Auditing is an increasingly important operation for computer programming, for example in security (e.g. to enable history-based acce ss control) and to enable reproducibility and accountability (e.g. provenance in scientific programming). Most proposed auditing techniques are ad hoc or treat auditing as a second-class, extralinguistic operation; logical or semantic foundations for auditing are not yet well-established. Justification Logic (JL) offers one such foundation; Bavera and Bonelli introduced a computational interpretation of JL called JLh that supports auditing. However, JLh is technically complex and strong normalization was only established for special cases. In addition, we show that the equational theory of JLh is inconsistent. We introduce a new calculus JLhc that is simpler than JLh, consistent, and strongly normalizing. Our proof of strong normalization is formalized in Nominal Isabelle.

ABSTRACT. The logical foundation of arithmetic generally starts with a quantificational logic over relations. Of course, one often wishes to have a formal treatment of functions within this setting. Both Hilbert and Church added to logic choice operators (such as the epsilon operator) in order to coerce relations that happen to encode functions into actual functions. Others have extended the term language with confluent term rewriting in order to encode functional computation as rewriting to a normal form. We take a different approach that does not extend the underlying logic with either choice principles or with an equality theory. Instead, we use the familiar two-phase construction of focused proofs and capture functional computation entirely within one of these phases. As a result, our logic remains purely relational even when it is computing functions.

ABSTRACT. Ludics is a logical framework in which types/formulas are modelled by sets of terms with the same computational behaviour. This paper investigates the representation of inductive data types and functional types in ludics. We study their structure following a game semantics approach. Inductive types are interpreted as least fixed points, and we prove an internal completeness result giving an explicit construction for such fixed points. The interactive properties of the ludics interpretation of inductive and functional types are then studied. In particular, we identify which higher-order functions types fail to satisfy type safety, and we give a computational explanation.