Reachability and regularity problems for Markov chains

The dynamic behavior of a Markov chain can be described using sequences of probability distributions starting from an initial (convex) set of distributions. We consider a symbolic representation for these trajectories over a finite alphabet, where the $n^{th}$ letter represents the probability range (instead of an exact value) after n steps of the Markov chain. Our goal is to study reachability and regularity for this symbolic language, which would allow us to perform quantitative verification for Markov chains.

We start by considering a basic reachability problem which lies at the heart of many of these questions: does there exist an integer n such that the probability to reach in n steps from a given state to another in a Markov chain is exactly some pre-specified value r. Surprisingly, it turns out that this problem is already as hard as the Skolem Problem: a number-theoretic decision problem whose decidability has been open for decades. We then provide some nearly-tight restrictions to the structure (in particular, the eigenvalues) of the Markov chain, under which we show regularity of the symbolic language.

The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO

We present a method for automatic fence insertion in concurrent programs running under weak memory models that provides the best known trade-off between efficiency and optimality. On the one hand, the method can efficiently handle complex aspects of program behaviors such as unbounded buffers and large numbers of processes. On the other hand, it is able to find small sets of fences needed for ensuring correctness of the program. To this end, we propose a novel notion of correctness, called persistence, that compares the behavior of the program under the weak memory semantics with that under the classical interleaving (SC) semantics. We instantiate our framework for the Total Store Ordering (TSO) memory model, and give an algorithm that reduces the fence insertion problem under TSO to the reachability problem for programs running under SC. Furthermore, we provide an abstraction scheme that substantially increases scalability to large numbers of processes. Based on our method, we have implemented a tool and run it successfully on a wide range benchmarks. The experimental results confirm the superiority of our tool compared to existing tools for analysis of programs running under TSO.

Joint work with Parosh Aziz Abdulla and Tuan Phong Ngo.

Formal methods for the verification of distributed algorithms

We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. Since the verification of distributed algorithms is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. We provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete.

Based on a joint work with C. Aiswarya and Benedikt Bollig, extended abstract at CONCUR 2015.

Model-Checking Higher-Order Recursion

Model-checking problems over first-order recursive programs have been well-studied for both static (inter-procedural) analysis and program verification. Although the foundations for analysing recursion in the presence of higher-order functions has been studied since the 1970s, it is only in the past 10 years that theoretical results have turned into algorithms that can be applied in practice.

In this talk I will survey the modelling of higher-order functions in terms of recursion schemes or the λY-calculus, as well as through automata models such as collapsible pushdown systems and Krivine machines. I will also briefly describe the growing selection of implementations available for higher-order analysis.

Automata with timed atoms

We advocate first-order definable sets (a materialization of sets with timed atoms) as a framework suitable for defining timed models of computation. Roughly speaking, the idea is to reinterpret classical definitions where state spaces, input alphabets, etc, are infinite but orbit-finite; and where transition relation is first-order definable. In particular, such a reinterpretation of nondeterministic finite automata is a slight extension of timed automata; and the reinterpretation of pushdown automata is an extension of dense-timed PDA of Abdulla et al.

Except a unifying view, the framework offers good algorithmic and closure properties. For instance, NFA with timed atoms are closed under minimization, contrarily to the classical timed automata; and non-emptiness problem for PDA is decidable in NEXPTIME. One can also naturally extend the setting to capture various extensions of timed automata.

Logics for Weighted Automata and Transducers

This talk will present some of the recent results obtained in the community on the relationship between weighted automata and weighted logics. The story started 10 years ago with the introduction of a quantitative semantics for MSO logic over words and an equivalence theorem between weighted automata and a restricted weighted MSO logic. Since then, many extensions have been studied: from words to trees, infinite words, pictures, etc; from semirings to more general weight computations. Also, the proof techniques have matured, from low level, carefully mimicking the classical proofs in the boolean setting, to higher level, using various abstract semantics. We illustrate this evolution by introducing a core weighted logic and its abstract semantics as multisets of weight structures. The equivalence between weighted automata and core weighted logic holds at the level of the abstract semantics. We will also demonstrate the versatility of the weighted automata approach by instantiating it into the transducer setting, showing a possible lead towards the design of an alternative logic for transductions.