The Parikh theorem (1961) states that the commutative image of every context-free language is a semi-linear set (an ultimately periodic set in Nd). Put differently, every context-free language can be represented by a finite-state automaton---if two words are considered the same whenever they agree on the number of occurrences of each letter.
This theorem has become a standard tool in the theory of infinite-state systems, with many different proofs of the original statement and many extensions. In this talk, we will look into complexity aspects of the theorem: how efficiently can the commutative image of a context-free language be represented? We will survey constructions and ideas behind several proofs, from Parikh's original construction to recent developments.
Formalisms and models of computations for languages over infinite alphabets have found applications in many areas of research in computer science. Originally, though, the idea came from a well known problem in database: the membership problem for datalog program, which gave birth to some models of register automata introduced in the late 1980's and early 1990's. The emergence of XML databases in the early 2000's further spurred researchers to in-depth study of various models such as pebble automata, two-variable logic and freeze register automata, to name a few. Since then, it has been realized that abstraction by languages over infinite alphabets can be useful, not only in database, but also in areas such as verification, specification, distributed computing and many others. In this talk we will provide a survey of literatures on data languages and languages over infinite alphabets from 1980's till now.
#SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tasks as counting the number of satisfying assignments to a Boolean formula and computing the volume of a polytope. In the realm of satisfiability modulo theories (SMT) there is a growing need for model counting solvers, coming from several application domains (quantitative information flow, static analysis of probabilistic programs). In this talk, we describe a reduction from an approximate version of #SMT to SMT with a focus on the theories of integer arithmetic and linear real arithmetic. We show an application of #SMT to the value problem for probabilistic programs.
In a recent work, we introduced four variants of diagnosability in (finite) probabilistic systems (pLTS) depending whether one considers (1) finite or infinite runs and (2) faulty or all runs. We studied their relationship and established that the corresponding decision problems are PSPACE-complete. A key ingredient of the decision procedures was a characterisation of diagnosability by the fact that a random run almost surely lies in an open set whose specification only depends on the qualitative behaviour of the pLTS. Here we investigate similar issues for infinite pLTS. We first show that this characterisation still holds for some diagnosability notion but with a Gδ set instead of an open set and also for two other diagnosability notions when pLTS are finitely branching. We also prove that surprisingly the remaining diagnosability notion cannot be characterised in this way even in the finitely branching case. Then we apply our characterisations to a partially observable probabilistic extension of visibly pushdown automata (POpVPA), yielding EXPSPACE procedures for solving diagnosability problems. In addition, we establish some computational lower bounds and show that slight extensions of POpVPA lead to undecidability.
Deductive proof systems enable the verification of infinite-state systems against temporal specifications. Notable examples of such proof systems are the ones developed by Kesten and Pnueli for the logic CTL* and by Slanina, Sipma and Manna for ATL*. One of the key advantages of this approach is its compositionality in the structure of the specification: the proof rules reduce the task of verifying a complex temporal formula to the tasks of verifying simpler (sub)formulas.
In this talk I will present two recent extensions of this approach. The first is a proof system for alternating-time temporal properties on continuous dynamical systems. It enables the application of existing constraint-based techniques for finding barrier certificates and Lyapunov functions to the design of controllers for complex temporal properties, while sidestepping the exponential cost of computing finite-state abstractions. Second, I will describe a deductive proof system for the verification of infinite-state probabilistic systems against specifications in probabilistic CTL*. It lifts the deductive approach to the probabilistic world by providing proof rules for establishing quantitative properties, as well as rules for relating quantitative and qualitative reasoning. The soundness arguments for these rules are completely distinct from the ones in the non-probabilistic setting and rely on martingale theory.
The talk is based on joint work with Rupak Majumdar, Luis Maria Ferrer Fioriti and Holger Hermanns.
Probabilistic programs whose runs accumulate quantities such as energy or cost are naturally modelled by cost chains, which are Markov chains whose transitions are labelled with a vector of integer costs. Computing information on the probability distribution of the total cost accumulated along a run is a fundamental problem in this model. Central to the analysis and verification of certain probabilistic programs is the so-called cost problem, which is to compute quantiles of the total cost, such as the median cost or the probability of large costs. While it is an open problem whether such probabilities are always computable or even rational, in this talk I will present an algorithm that allows to approximate the probabilities with arbitrary precision. The algorithm is simple to state and implement, and exploits strong results from graph theory such as the so-called BEST theorem for efficiently computing the number of Eulerian circuits in a directed graph. Moreover, the algorithm allows for showing that the decision version of the cost problem lies in the counting hierarchy, a counting analogue to the polynomial-time hierarchy that contains the latter and is included in PSPACE. Finally, I will demonstrate the effectiveness of the algorithm by evaluating it on case studies of probabilistic programs that have appeared in the literature.
Asynchronous programming has become ubiquitous in smartphone and web application development, as well as in the development of server-side and system applications. Many of the uses of asynchrony can be modeled by extending programming languages with asynchronous procedure calls - procedures not executed immediately, but stored and selected for execution at a later point by a non-deterministic scheduler. Asynchronous calls induce a flow of control that is difficult to reason about, which in turn makes formal verification of asynchronous programs challenging. In response, we take a rely/guarantee approach: Each asynchronous procedure is verified separately with respect to its rely and guarantee predicates; the correctness of the whole program then follows from the natural conditions the rely/guarantee predicates have to satisfy. In this way, the verification of asynchronous programs is modularly decomposed into the more usual verification of sequential programs with synchronous calls. For the sequential program verification we use Hoare-style deductive reasoning, which we demonstrate on several simplified examples. These examples were inspired from programs written in C using the popular Libevent library; they are manually annotated and verified within the state-of-the-art Frama-C platform.