C Aiswarya (CMI, Chennai, India )
Recency-bounded verification of dynamic database-driven systems Slides
Abstract:
We propose a formalism to model database-driven systems, called database manipulating systems (DMS). The actions of a DMS modify the current instance of a relational database by adding new elements into the database, deleting tuples from the relations and adding tuples to the relations. The elements which are modified by an action are chosen by (full) first-order queries. We propose monadic second order logic (MSO-FO) to reason about sequences of database instances appearing along a run of a DMS. Unsurprisingly, the linear-time model checking problem of DMS against MSO-FO is undecidable. Towards decidability, we propose under- approximate model checking of DMS, where the under-approximation parameter is the bound on recency. In a k-recency-bounded run, only the most recent k elements in the current active domain may be modified by an action. More runs can be verified by increasing the bound on recency. Our main result shows that recency-bounded model checking of DMS against MSO-FO is decidable, by a reduction to the satisfiability problem of MSO over nested words.
Based on a joint work with Parosh Abdulla, Mohammed Faouzi Atig, Marco Montali and Othmane Rezine, which appeared in PODS 2016.
Mikołaj Bojańczyk (University of Warsaw, Poland)
A probabilistic variant of MSO on infinite trees
Abstract:
I will talk about a variant of MSO on infinite trees which can talk about probabilities. When adding probability to MSO, one has to be very careful to avoid undecidability, e.g. one has to avoid encoding the undecidable emptiness problem for probabilistic automata on ω-words. Michalewski and Mio managed to find a logic which is not immediately seen to be undecidable, and this is the logic I will talk about. The logic is the extension of MSO with a quantifier that says "there is zero probability of choosing a path π in the tree so that property φ(π) is satisfied". The talk is based on an ICALP 2016 paper , which shows that a variant of the logic can be captured by an automaton model, and followup unpublished work (joint with Hugo Gimbert and Edon Kelmendi), which shows that the automaton has decidable emptiness.
Ahmed Bouajjani (IRIF, University of Paris Diderot, France)
The Benefits of Duality in Verifying Concurrent Programs under TSO.
Abstract:
We address the problem of verifying safety properties of concurrent programs running over the TSO memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes. In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO model that is more amenable for efficient algorithmic verification and for extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows to obtain a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.
Joint work with: Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Tuan Phong Ngo. (published at CONCUR 2016 Link to Paper.)
Dmitry Chistikov (University of Oxford, UK)
Minimal probabilistic automata and nonnegative matrix factorizations require irrational numbers
Abstract:
Consider probabilistic automata that for each n induce a probability distribution on words of length n. Let the semantics of an automaton be defined as this sequence of distributions, and consider the state minimization problem for these automata. Is it true that, whenever the transition probabilities in an automaton are rational numbers, there is a state-minimal equivalent automaton whose transition probabilities are also rational?
We shall see that the answer to this question is negative, by constructing a matrix M with nonnegative rational entries and with the following properties. The matrix has a factorization M = W H into matrices W and H with nonnegative entries such that the shared dimension of W and H is 5, but every such factorization needs to have irrational entries in W and H. This resolves an open problem by Cohen and Rothblum (1993), showing that nonnegative ranks of matrices over the reals and over the rationals are different functions.
Joint work with Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell.
Constantin Enea (IRIF, University of Paris Diderot, France)
On Verifying Causal Consistency
Abstract:
Causal consistency is one of the most adopted consistency criteria in distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence.
We address the problem of verifying whether the executions of an implementation of a data structure are causally consistent. We consider two problems: (1) checking whether one single (finite) execution is causally consistent, which is relevant for developing testing and bug finding algorithms, and (2) verifying whether all the executions of an implementation are causally consistent.
We show that the first problem is NP-complete. This holds even for the read-write memory abstraction, which is a building block of many today's implementations. In particular, key-value stores, that are omnipresent in distributed implementations, are instances of the read-write memory abstraction. Moreover, we prove that the second problem is undecidable, and again this holds even for the read-write memory abstraction.
We prove however that for the read-write memory abstraction, these negative results can be circumvented if we assume data independence, i.e., that the behaviors of implementations do not depend on the data values that are written or read at each moment, which is a realistic assumption. We prove that in this case, checking the correctness of a single execution w.r.t. the read-write memory abstraction is polynomial time. Furthermore, we show that the set of non-causally consistent executions can be represented by means of a finite number of state machines (register automata). Using these machines as observers (in parallel with the implementation) allows to reduce polynomially the problem of checking causal consistency to a state reachability problem. This reduction holds regardless of the class of programs used for the implementation, the number of read-write variables, and the used data domain. For a significant class of implementations, we derive from this reduction the decidability of verifying causal consistency w.r.t. the read-write memory abstraction.
This is joint work with Ahmed Bouajjani, Rachid Guerraoui, and Jad Hamza.
Javier Esparza (TU Munich, Germany)
From LTL to Limit-Deterministic Automata Slides
Abstract
Limit-deterministic Büchi automata can replace deterministic Rabin automata in probabilistic model checking algorithms, and can be significantly smaller. We present a direct construction from an LTL formula to a limit-deterministic Büchi automaton. The automaton is the combination of a non-deterministic component, guessing the set of eventually true G-subformulas of the formula, and a deterministic component verifying this guess and using this information to decide on acceptance. Contrary to the indirect approach of constructing a non-deterministic automaton for the formula and then applying a semi-determinisation algorithm, our translation is compositional and has a clear logical structure. Moreover, due to its special structure, the resulting automaton can be used not only for qualitative, but also for quantitative verification of MDPs, using the same model checking algorithm as for deterministic automata. This allows one to reuse existing efficient implementations of this algorithm without any modification. Our construction yields much smaller automata for formulas with deep nesting of modal operators and performs at least as well as the existing approaches on general formulas.
Joint work with Salomon Sickert, Stefan Jaax, and Jan Kretinsky.
Emmanuel Filiot (Université Libre de Bruxelles, Belgium)
Automata, Logic and Algebra for Word Transductions Slides
Abstract
This talk will survey old and recent results about word transductions, i.e. functions mapping (finite) words to words. Connections between automata models (transducers), logic and algebra will be presented. Starting with rational functions, defined by (one-way) finite transducers, and the canonical model of bimachines introduced by Reutenauer and Schützenberger, the talk will also target the more expressive class of functions defined by two-way transducers and its equivalent MSO-based formalism.
Blaise Genest (IRISA Rennes, France)
Controlling a Population
Abstract
We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. In this talk, we will describe a sure synchronization problem for such populations: no matter how individual agents react to the actions of the controller, the controller aims at driving all agents synchronously to a goal set of states. The agents are naturally represented by a non-deterministic finite state automaton, the same for every agent, and the whole system is encoded as a 2-player game. The first player chooses actions, and the second player resolves non-determinism for each agent. The game with m agents is called the m-population game. A natural parametrized control problem, given the automaton representing the agents, is whether player one wins the m-population game for any population size m. We show that if the answer is negative, there exists a cut-off, that is, a population size m0 such that for populations of size m < m0 there exists a winning controller, and there is none for populations of size m >m0. Surprisingly, we show that this cut-off can be doubly exponential in the number of states of the NFA. While this suggests a high complexity for the parameterized control problem, we actually show that it can be solved in EXPTIME and is PSPACE-hard.
Joint work with Nathalie Bertrand, Miheer Dewaskar et Hugo Gimbert.
Hugo Gimbert (LaBRI, University of Bordeaux, France)
On the controller synthesis problem for distributed systems with causal memory
Abstract
Synthesizing distributed controllers of distributed systems is a challenging task. There are several ways to formalize this problem, here we assume that 1) both the plant and the controllers are modelled as Zielonka automata. 2) when two or more components of the distributed system perform a synchronization the local controllers are allowed to exchange as much information as they want, i.e. they share their entire causal memory and make their decisions based on this memory.
There exists three classes of plants for which controller synthesis has been shown decidable in this distributed setting: when the dependency graph of actions is series-parallel, when the processes are connectedly communicating and when the dependency graph of processes is a tree.
We provide a unified proof of these results and give new examples of plants for which controller synthesis is decidable.
Stefan Göller (LSV, ENS Cachan, France)
On long words avoiding Zimin patterns
Abstract
A word w encounters a pattern p if some infix of w can be obtained from p by replacing each of its variables by some non-empty word. A pattern p is called unavoidable if for every finite alphabet A every sufficiently long word over A encounters p. A result due to Zimin and Bean, McNulty & Ehrenfeucht states that a pattern over n distinct variables is unavoidable if, and only if, is is encountered in the n-th Zimin pattern Z_n, where Z_1=x_1 and Z_n+1=Z_n x_n+1 Z_n. In this talk we will concern ourselves with the asymptotic growth rate of f(n,k), which is the minimal word length that guarantees that every word of this length over a k-letter alphabet encounters Z_n.
This talk is based on a collaboration with Arnaud Carayol.
Bartek Klin (University of Warsaw, Poland)
Functional programming over sets with atoms
Abstract
Sets with atoms, or nominal sets, offer a way to finitely present certain infinite data structures that exhibit enough symmetry. Essentially, such structures can be presented as their model-theoretic interpretations in a fixed infinite structure with a decidable first-order theory. Well-chosen programming language idioms can hide the interpretations from the programmer and let them work, most of the time, under the convenient intuition of looping and searching through infinite structures. I will say how, and give examples of when it does or does not work.
Martin Lange (University of Kassel, Germany)
Buffered Simulation Games
Abstract
This talk is about games played between two players on two Büchi automata, based on the ordinary simulation game. Starting in the respective initial states, Spoiler advances along a transition in his automaton thus choosing a letter, followed by Duplicator who makes a move with the same letter. It is known that this does not capture language inclusion between Büchi automata but only approxi- mates it from below. However, simulation can be decided in polynomial time while language inclusion is PSPACE-hard.
In order to refine the approximation we consider such games equipped with a buffer which allows Duplicator to delay her moves. For buffers of fixed capacity, this kind of simulation is still decidable in polynomial time, and the buffer sizes induce a hierarchy of approximations below language inclusion. This is as far as buffered simulation is useful for Büchi inclusion: on buffers of unbounded capacity the problem already becomes EXPTIME-hard but still does not capture language inclusion.
We then consider an extension in which the letters are stored in several buffers and show that these multi-buffer games approximate the inclusion problem for trace languages. Again, for finite buffer capacities, multi-buffer simulation is decidable (in polynomial time when these capacities are fixed). Interestingly, adding a single buffer of capacity 0 to one unbounded buffer increases the complexity from EXPTIME to the Boolean closure of Sigma^1_1.
This is joint work with Milka Hutagalung, Dietrich Kuske, Etienne Lozes and Norbert Hundeshagen.
Amaldev Manuel (CMI, Chennai, India )
Cost functions defined by min automata and max automata
Abstract
Min automata (or distance automata) and Max automata (or (max, +)-automata) are two well known classes of weighted automata. We address their decidability problem in the context of regular cost functions: when is it that a regular cost function recognisable by one of these?, and show that it is decidable.
Roland Meyer (TU Kaiserslautern, Germany)
Liveness Verification and Synthesis: New Algorithms for Recursive Programs
Abstract
We consider the problems of liveness verification and liveness synthesis for recursive programs. The liveness verification problem (LVP) is to decide whether a given omega-context-free language is contained in a given omega-regular language. The liveness synthesis problem (LSP) is to compute a strategy so that a given omega-context-free game, when played along the strategy, is guaranteed to derive a word in a given omega-regular language. The problems are known to be EXPTIME-complete and 2EXPTIME-complete, respectively. Our contributions are new algorithms with optimal time complexity. For LVP, we generalize recent lasso-finding algorithms (also known as Ramsey-based algorithms) from finite to recursive programs. For LSP, we generalize a recent summary-based algorithm from finite to infinite words. Lasso finding and summaries have proven to be efficient in a number of implementations for the finite state and finite word setting.
Based on joint work with Sebastian Muskalla and Elisabeth Neumann
Madhavan Mukund (CMI, Chennai, India)
Distributed Probabilistic Systems Slides
Abstract
One way to address the challenge of formal verification of large probabilistic models is to exploit concurrency and define a network of probabilistic agents that interact through communication. However, constructing a sensible global probabilistic measure over the runs of a system with both concurrency and nondeterminism is nontrivial.
We begin by defining Distributed Markov Chains (DMC), a class of communicating agents in which probability distributions are attached to synchronized moves between groups of agents. The key restriction is that any two simultaneously enabled synchronizations involve disjoint sets of agents. This allows us to view such a network as a succinct and distributed presentation of a large global Markov chain.
We use partial-order notions to define an interleaved semantics that can be used to efficiently verify properties of the global Markov chain represented by the network, using statistical model checking.
We then extend the DMC model to Distributed Probabilistic Systems (DPS) that allow nondeterministic choices between synchronizations. In a DPS, schedulers are used to resolve nondeterminism, like Markov Decision Processes. We illustrate the DPS model through an example from business process modelling (BPM) involving stochastic resource-constrained business processes.
This is joint work with R P Jagadish Chandra Bose, Javier Esparza, Sumit Kumar Jha, Ratul Saha and P S Thiagarajan.
Anca Muscholl (LaBRI, University of Bordeaux, France)
Sound negotiations and static analysis
Abstract
Negotiations are a graphical formalism for describing multiparty distributed cooperation, proposed by Desel and Esparza. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In a former paper, Esparza and Desel have shown that deciding soundness of arbitrary negotiations is PSPACE-complete, and in PTIME for deterministic negotiations. First we review the soundness problem and consider it beyond deterministic negotiations: we show that soundness of acyclic, weakly non-deterministic negotiations is in PTIME, and that checking soundness is already NP-complete for slightly more general classes. Next, for sound deterministic negotiations, fundamental questions like computing summaries or the expected cost can be solved in PTIME too, while they are PSPACE-complete in the general case. We extend these results by showing how to solve Mazurkiewicz-invariant analysis problems in PTIME.
Joint work with J. Esparza, D. Kuperberg and I. Walukiewicz
M Praveen (CMI, Chennai, India )
Nesting Depth of Operators in Graph Database Queries: Expressiveness vs. Evaluation Complexity
Abstract
Designing query languages for graph structured data is an active field of research, where expressiveness and efficient algorithms for query evaluation are conflicting goals. To better handle dynamically changing data, recent work has been done on designing query languages that can compare values stored in the graph database, without hard coding the values in the query. The main idea is to allow variables in the query and bind the variables to values when evaluating the query. For query languages that bind variables only once, query evaluation is usually NP-complete. There are query languages that allow binding inside the scope of Kleene star operators, which can themselves be in the scope of bindings and so on. Uncontrolled nesting of binding and iteration within one another results in query evaluation being PSPACE-complete.
We define a way to syntactically control the nesting depth of iterated bindings, and study how this affects expressiveness and efficiency of query evaluation. The result is an infinite, syntactically defined hierarchy of expressions. We prove that the corresponding language hierarchy is strict. Given an expression in the hierarchy, we prove that it is undecidable to check if there is a language equivalent expression at lower levels. We prove that evaluating a query based on an expression at level i can be done in level i of the polynomial time hierarchy. Satisfiability of quantified Boolean formulas can be reduced to query evaluation; we study the relationship between alternations in Boolean quantifiers and the depth of nesting of iterated bindings.
Prakash Saivasan (TU Kaiserslautern, Germany)
The complexity of regular abstractions of one-counter languages
Abstract
One counter automaton is a finite state automaton equipped with a counter and an ability to perform increments, decrements and test for zero on it. The class of languages recognized by such automata falls between the class of context free and regular languages. From the verification perspective, such automata can model programs with ability to count. In this talk, I will discuss about the complexity of the regular representations for downward closure, upward closure and parikh image abstraction of a given one counter language.
Philippe Schnoebelen (LSV, ENS Cachan, France)
Decidable fragments of the logic of subwords
Abstract
While subwords appear prominently in many works in language theory, program verification, combinatorics on words, etc., not much is known about the decidability of logics for subwords and subsequences.
In this talk we present several recently identified fragments of the first-order logic of subwords that have been shown decidable. We also describe some new techniques from the descriptive complexity of piecewise-testable languages that have been used in the complexity analysis of our decidable logic fragments.
AV Sreejith (CMI, India - currently visiting University of Warsaw, Poland )
Extending monadic second order logic with bounded predicate.
Abstract
In this talk, we introduce two monadic second order predicates, (1) the periodic predicate which recognises periodic sets and (2) the bounded predicate which recognises bounded sets. We then look at the monadic second order logic (MSO) extended with these predicates over omega words. First, we see that MSO with periodic predicates can define bounded sets. Next we show that MSO with bounded predicate can effectively simulate the U quantifier (this monadic second order quantifier says there are unbounded number of sets). This surprising result shows that the satisfiability problem is undecidable for both logics. In short, even the addition of a very weak predicate like ultimately periodic is enough to make MSO undecidable.
This is a joint work with Bruno Guillon, Laure Daviaud, Mikołaj Bojańczyk and Vincent Penelle.
B Srivathsan (CMI, Chennai, India )
Abstractions for timed automata Slides
Abstract
Timed automata are finite automata equipped with real-valued variables called clocks, that are used to constrain transitions. We consider the reachability problem for timed automata. As the space of configurations of a timed automaton is infinite (due to clocks), reachability algorithms compute a finite abstraction of the automaton's behaviour.
In this talk, we present some recent results that enable computing smaller (and hence better) abstractions for the reachability problem.
Joint work with F. Herbreteau and I. Walukiewicz.
S P Suresh (CMI, Chennai, India )
Existential Assertions in Dolev-Yao
Abstract
The Dolev-Yao model is a mainstay of formal modeling and analysis of security protocols. It is used to study logical flaws in protocols, under the assumption of perfect cryptography. Over the years, many extensions have been proposed to the Dolev-Yao model, to help model more sophisticated protocols and security properties. In this talk, we present a particular extension wherein agents can communicate assertions to each other, in addition to cryptographic terms. These assertions typically specify properties of the accompanying terms, and could involve conjunction, disjunction and existential quantification. These capture the ability to convey partial information about terms and witness hiding that are common in applications like e-voting protocols.
We introduce the model, describe how to define interesting security properties like anonymity and unlinkability, and briefly touch upon the verification question and its complexity.
This is joint work with R Ramanujam (IMSc) and Vaishnavi Sundararajan (CMI).
Grégoire Sutre (LaBRI, University of Bordeaux, France)
Boundedness and Coverability for Pushdown Vector Addition Systems Slides
Abstract
Pushdown automata and vector addition systems (or, equivalently, Petri nets) are among the most fundamental models of computation. The former can model recursion while the latter can model concurrency. Despite being infinite-state, both models admit many decidable verification questions. In particular, boundedness (is the reachability set finite?) and coverability (is a given control state reachable?) are decidable for these two models. A natural question is whether these problems remain decidable when we combine pushdown automata and vector addition systems. The combination that I will consider in this talk is called pushdown vector addition systems (PVAS). These are finite-state automata equipped with one pushdown stack and several Petri net counters. I will briefly show how to decide boundedness for PVAS. Then, I will focus on PVAS in dimension one (i.e., one Petri net counter), and show that coverability is decidable for this model.
The talk is based on joint works with J. Leroux, M. Praveen and P. Totzke.