ACTS 2023

We show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasoning tools.

Theoretically, interactive protocols exist for all PSPACE problems. The verifier of a protocol checks the prover's answer to a problem instance in polynomial time, with polynomially many bits of communication, and with exponentially small probability of error. (The prover may need exponential time.) Existing interactive protocols are not used in practice because their provers use naive algorithms, inefficient even for small instances, that are incompatible with practical implementations of automated reasoning.

We bridge the gap between theory and practice by means of a novel interactive protocol whose prover uses BDDs. We consider the problem of counting the number of assignments to a QBF instance (#CP), which has a natural BDD-based algorithm. We give an interactive protocol for #CP whose prover is implemented on top of an extended BDD library. The prover has only a linear overhead in computation time over the natural algorithm.

Video

Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. Two of the most studied such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e., while model-checking is (non-elementarily) decidable, satisfiability is undecidable for both logics. We settle the exact complexity of these problems, showing that both are in fact highly undecidable: HyperLTL satisfiability is {$\Sigma^1_1$}-complete and HyperCTL* satisfiability is {$\Sigma^2_1$}-complete. To prove {$\Sigma^2_1$} membership for HyperCTL*, we prove that every satisfiable HyperCTL* formula has a model that is equinumerous to the continuum, and that this bound is tight. On the other hand, both countable and finitely-branching satisfiability for HyperCTL* are as hard as truth in second-order arithmetic, i.e. still highly undecidable.

This is joint work with Louwe B. Kuijer, Patrick Totzke and Martin Zimmermann.

Video

Since the 1970s with the work of McNaughton, Papert and Schützenberger, a regular language is known to be definable in the first-order logic if and only if its syntactic monoid is aperiodic. This algebraic characterisation of a fundamental logical fragment has been extended in the quantitative case by Droste and Gastin in 2019, dealing with polynomially ambiguous weighted automata and a restricted fragment of weighted first-order logic. In the quantitative setting, the full weighted first-order logic (without the restriction that Droste and Gastin use, about the quantifier alternation) is more powerful than weighted automata, and extensions of the automata with two-way navigation, and pebbles or nested capabilities have been introduced to deal with it. In this talk, we will review these models and characterise the fragment of the two-way nested weighted automata that recognise exactly the full weighted first-order logic, under the condition that automata are polynomially ambiguous.

This is a joint work with Dhruv Nevatia.

Video

Video

This is an overview of some recent work on the verification of concurrent programs. Traditionally concurrent programs are interpreted under sequential consistency (SC). Eventhough SC is very intuitive and easy to use, modern multiprocessors do not employ SC for performance reasons, and instead use so called "weak memory models". Some of the well known weak memory models in vogue among modern multiprcessor architectures are Intel x-86, IBM POWER and ARM. The use of weak memory is also prevelant in the C11 model, leading to the release acquire fragment of C11. This talk is on the verification of concurrent programs under the release acquire (RA) semantics. The main focus of the talk will be on non parameterized programs under RA, and I will briefly discuss results in the parameterized setting.

In the non parameterized setting, we show that the reachability problem for RA is undecidable even in the case where the input program is finite-state, closing a long standing open problem. What works well for this class is under approximate reachability, in the form of bounded view switching, an analogue of bounded context switching, relevant to RA. In the parameterized setting, the first observation is that the semantics of RA can be simplified, lending to a better complexity for verification. Further, safety verification is PSPACE-complete for the case where the distinguished threads are loop-free, and jumps to NEXPTIME-complete for the setting where an unrestricted distinguished ego thread interacts with the environment threads. I will conclude by summarizing the rich complexity landscape of C11 memory models.

This talk is based on papers that appeared in PLDI'19 (joint with Parosh Abdulla, Mohamed Faouzi Atig and Jatin Arora), PODC'22 (joint with Roland Meyer, Adwait Godbole and Soham Chakraborty) and PLDI'23 (joint with Parosh Abdulla, Soham Chakraborty, Umang Mathur, Andreas Pavlogiannis and Hunkar Can Tunc).

Video

In this talk, we present the framework of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1 responds rationally with a strategy that is an optimal response. While it is usually assumed that Player 1 has a single objective, we consider here the new setting where he has several. In this context, after responding with his strategy, Player 1 gets a payoff in the form of a vector of Booleans corresponding to his satisfied objectives. Rationality of Player 1 is encoded by the fact that his response must produce a Pareto-optimal payoff given the strategy of Player 0. We study the Stackelberg-Pareto Synthesis problem which asks whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1. We solve this problem for several types of omega-regular objectives. In particular, for games with parity objectives, we show that this problem is fixed-parameter tractable and NEXPTIME-complete. We also discuss the related Stackelberg-Pareto Verification problem which asks whether a given finite-memory strategy announced by Player 0 satisfies his objective, whatever the rational response of Player 1.

Video

The basic algorithm to analyze timed automata involves a symbolic enumeration of its reachable configurations. Over the last thirty years, different strategies have been studied to speed up this enumeration and have been successfully implemented in tools. In this talk, we will see some recent techniques for improving this enumeration and for extending it to richer models.

More specifically, we will look at:

• how a local-time semantics for networks of timed automata can be incorporated into the enumeration procedure. This allows for the use of partial-order reduction techniques. Joint work with Frédéric Herbreteau, R Govind, Igor Walukiewicz.
• a new simulation relation that has helped in seamlessly extending the enumeration algorithm to timed automata containing difference-constraints in guards and richer clock updates. Joint work with Paul Gastin and Sayan Mukherjee.
• an extension of the reachability algorithm to a generalized timed automaton model containing two kinds of clocks: history and future. This model succinctly captures timing constraints that can be expressed by clocks, event-clocks and timers. 
Joint work with S Akshay, Paul Gastin, R Govind and Anirudhha Joshi.

Video

Given a sentence {$\forall X \exists Y \varphi(X, Y)$} in a first-order theory, it is well-known that there exists a function {$F(X)$} for {$Y$} in {$\varphi$} such that {$\exists Y \varphi(X, Y) \leftrightarrow \varphi(X, F(X))$} holds for all values of the universal variables {$X$}. Such a function is also called a Skolem function, in honour of Thoralf Skolem who first made us of this in proving what are now known as the Lowenheim-Skolem theorems. The existence of a Skolem function for a given formula is technically analogous to the Axiom of Choice -- it doesn't give us any any hint about how to compute the function, although we know such a function exists. Nevertheless, since Skolem functions are often very useful in practical applications (like finding a strategy for a reactive controller), we investigate when is it possible to algorithmically construct a Turing machine that computes a Skolem function for a given first-order formula. We show that under fairly relaxed conditions, this cannot be done. Does this mean the end of the road for automatic synthesis of Skolem functions? Fortunately, no. We show model-theoretic necessary and sufficient condition for the existence and algorithmic synthesizability of Turing machines implementing Skolem functions. We show that several useful first-order theories satisfy these conditions, and hence admit algorithms that can synthesize Turing machines implementing Skolem functions. We conclude by presenting several open problems in this area.

This is joint work with Akshay S. and a preliminary version of the work was presented in MFCS 2022.

Video

Video

Distributed algorithms are central to many domains such as scientific computing, telecommunications and the blockchain. Even when they aim at performing simple tasks, their behaviour is hard to analyze, due to the presence of faults (crashes, message losses, etc.) and to the asynchrony between the processes. Parameterized verification techniques have been developed to prove correctness of distributed algorithms independently of the actual setup, i.e. the number of processes and the potential failures.

In this talk, we present a CEGAR approach to checking safety and liveness properties for fault-tolerant distributed algorithms that use threshold conditions, typically on the number of received messages of a given type.

This is based on joint work with Bastien Thomas, Ocan Sankur and Josef Widder.

Video

Joint work with Mrudula Balachander, Emmanuel Filiot, and Jean-François Raskin.

We study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against a hostile environment. In the variant studied here, the user provides the high level LTL specification {$\varphi$} of the system to design, and a set {$E$}of examples of executions that the solution must produce. Our synthesis algorithm works in two phases. First, it generalizes the decisions taken along the examples {$E$} using tailored extensions of automata learning algorithms. This phase generalizes the user-provided examples in {$E$} while preserving realizability of {$\varphi$}. Second, the algorithm turns the (usually) incomplete Mealy machine obtained by the learning phase into a complete Mealy machine that realizes {$\varphi$}. The examples are used to guide the synthesis procedure. We provide a completness result that shows that our procedure can learn any Mealy machine {$M$} that realizes {$\varphi$} with a small (polynomial) set of examples. We also show that our problem, that generalizes the classical LTL synthesis problem (i.e. when {$E=\emptyset$}), matches its worst-case complexity. The additional cost of learning from {$E$} is even polynomial in the size of {$E$} and in the size of a symbolic representation of solutions that realize {$\varphi$}. This symbolic representation is computed by the synthesis algorithm implemented in Acacia-Bonzai when solving the plain LTL synthesis problem. We illustrate the practical interest of our approach on a set of examples.

Video

The starting point is the question whether there is a graph satisfying a graph property {$\Phi$} in a family of graphs given by a set of words under the assumption each word represents a finite graph? We approach this question by using formal languages for specifying families of graphs, in particular by regular sets of words. We show that certain graph properties can be decided for regular languages by studying the syntactic monoid of the specification language. More specifically, we use a natural binary encoding of finite graphs over a binary alphabet {$\Sigma$}, and we define a regular set {$\mathbb{G}\subseteq \Sigma^*$} such that every nonempty word {$w\in \mathbb{G}$} defines a finite and nonempty graph. Also, graph properties can then be syntactically defined as languages over {$\Sigma$}. Then, we ask whether a given automaton specifies some graph satisfying a certain property {$\Phi$}. Our structural results show that we can answer this question for all "typical"' graph properties. For example, the following problems are decidable.

• Is there some {$G$} with a Hamiltonian cycle?
• Is there some {$G$} with a perfect matching?
• Is there some {$G$} with a dominating set of size at most {$\log_2 |V_G|$}?
• Is there some {$G$} with a defensive alliance of size at most {$\log_2 |V_G|$}?

The talk is based on a joint work with Henning Fernau (Trier) and Petra Wolf (Bergen, Norway).

The Skolem Problem asks to determine whether a given integer linear recurrence sequence (such as the Fibonacci numbers) has a zero term. This problem, whose decidability has been open for many decades, arises across a wide range of topics in computer science, including loop termination, probabilistic model checking, weighted automata theory, and dynamical systems, amongst many others. Recently, a new approach to the Skolem Problem was initiated via the notion of a Universal Skolem Set: a set S of positive integers such that it is decidable whether a given linear recurrence sequence has a zero in S. I will present a survey and overview of the Skolem Problem, including lines of attack based on Universal Skolem Sets.

This is joint work with Florian Luca, James Maynard, Armand Noubissie, and James Worrell.

Video

The problem of distributed synthesis is to automatically generate a distributed algorithm, given a target communication network and a specification of the algorithm’s correct behavior.

Previous work has focused on static networks with an a priori fixed message size. This approach has two shortcomings: Recent work in distributed computing is shifting towards dynamically changing communication networks rather than static ones, and an important class of distributed algorithms are so-called full-information protocols, where nodes piggy-pack previously received messages onto current messages.

In this work, we consider the synthesis problem for a system of two nodes communicating in rounds over a dynamic link whose message size is not bounded. Given a network model, i.e., a set of link directions, in each round of the execution, the adversary choses a link from the network model, restricted only by the specification, and delivers messages according to the current link’s directions. Motivated by communication buses with direct acknowledge mechanisms, we further assume that nodes are aware of which messages have been delivered.

We show that the synthesis problem is decidable for a network model if and only if it does not contain the empty link that dismisses both nodes’ messages.

Video

We consider the problem of verifying the safe trajectory of a camera-based autonomous vehicle in a given 3D-scene. We give a couple of effective procedures to verify that all trajectories starting from a given initial region reach a specified target region safely without colliding with obstacles on the way. Our first procedure is based on the key notion of image-invariant regions, which are regions within which the captured images are identical. The second technique is an abstraction-refinement approach that uses the notion of an interval image abstraction. We evaluate our methods on a model of an autonomous road-following drone with simplified dynamics, in a variety of 3D-scenes; our experimental results demonstrate the feasibility and benefits of our approach for both safety analysis and falsification.

This is joint work with P. Habeeb, Kamal Lodaya, and Pavithra Prabhakar.