C Aiswarya (Uppsala University, Sweden)
Communicating Recursive Programs: Control and Split-width (Slides: pdf)
Abstract:
Communicating recursive programs (CRPs) form an important but Turing powerful class of distributed systems. Several under-approximation methods have been proposed towards their automated analysis. However, most of these do not allow to detect, in a distributed and on-the-fly manner, whether a run has exceeded the approximation parameter. This kind of control mechanism is desirable, and often inevitable, when employing under approximation for the verification of safety-critical systems.
We present a new under approximation, which either subsumes or is orthogonal to the existing under approximations, and design a deterministic distributed controller for it. The decidability of the under-approximation is shown by demonstrating a bound on its split-width. Split-width is a measure on the graph behaviours of CRPs which is equivalent to tree/clique-width. At the same time it is conceptually much simpler to understand and easy to prove a bound on. The talk will give a gentle introduction to split-width and illustrate its simplicity by demonstrating a bound on the aforementioned under approximation.
These results and notions have appeared in three papers coauthored with Paul Gastin and K. Narayan Kumar (CONCUR 12, CONCUR 14, and ATVA 14) and also in my PhD thesis.
Mohamed Faouzi Atig (Uppsala University, Sweden)
The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO
Abstract:
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
Benedikt Bollig (LSV, ENS Cachan, France)
Towards a Regular Theory of Parameterized Concurrent Systems (Slides: pdf)
Abstract:
We present parameterized communicating automata (PCAs), where finite-state processes exchange messages via rendez-vous or through bounded FIFO channels. Unlike classical communicating automata, a given PCA can be run on any network topology of bounded degree. We present various Büchi-Elgot-Trakhtenbrot theorems for PCAs, which roughly read as follows: Let F be an existential MSO formula and T be any of the following topology classes: pipelines, ranked trees, grids, or rings. There is a PCA that is equivalent to F on all topologies from T. In the case where each process executes a bounded number of contexts (each context restricting communication in a suitable way), we can even show that PCAs are closed under complementation, are expressively equivalent to full MSO logic, and have a decidable emptiness problem.
The talk contains results from joint works with Paul Gastin, Akshay Kumar, and Jana Schubert.
Christopher Broadbent (TU Munich, Germany)
Model-Checking Untyped Recursion Schemes over the Modal Mu-Calculus
Abstract:
"Higher-Order Model-Checking" concerns itself with the (Böhm) trees generated by higher-order recursion schemes, which are essentially terms of the simply typed lambda calculus with recursion. The full modal mu-calculus is decidable on these models, and safety properties at least can also be checked in practice. Applications in the literature include the manipulation of compressed data, flow analysis, safety verification of higher-order programs (including the inference of refinement types), and more recently termination verification of higher-order programs (via transition invariants).
It is natural to ask about the extent to which we can apply techniques from the simply typed case to arbitrary (untyped) recursion schemes. Since this model is Turing complete we must, of course, limit our ambitions to finding model-checking algorithms that are sound, but complete only relative to some natural (even if undecidable) constraint on the recursion scheme.
Kobayashi's RTReCS tool is an example of work in this vein, which checks safety properties of "mu-HORS", a subclass of untyped recursion schemes that are nonetheless Turing Complete. The RTReCS algorithm is complete relative to typability in a system of recursive intersection types.
Our current work attempts to go further by considering completely unrestricted recursion schemes and all properties expressible in the full modal mu-calculus. We extend the mu-calculus to a kind of recursive intersection type system, which in particular allows for a function-space constructor and alternating fixpoints to be bound to variables occurring negatively as well as positively. There is a sense in which this type system is "optimal" (for a non-dependent type system): the type-system can witness that a term t has Böhm tree satisfying a mu-calculus property P iff there exists a regular over-approximation of the terms reachable from t such that it is "sufficient to consider" the weakest expressible property satisfied by all terms in each respective regular set.
We show further that there exists a model-checking algorithm remiscent of Ramsay et al's recent algorithm and higher-order saturation algorithms (for safety on simply typed HORS) that is complete relative to the aforementioned type system.
Thomas Colcombet (LIAFA, University Paris 7, France)
Characterizing logics over infinite words (Slides: pdf)
Abstract:
In this talk, we consider infinite linear orderings of countable length. It is known that their monadic theory is decidable.
Inspired from ideas of the algebraic theory of monoids as pioneered by Schützenberger, we will show that it is possible to characterize effectively natural fragments of monadic logic over countable linear orderings.
We will be particularly interested in changing the domain of quantifiers: can we characterize first-order? first order with access to cuts? weak monadic logic? weak monadic logic with access to cuts? monadic logic with quantifier over scattered subsets?
The material for this talk is based on works and collaborations with Alexis Bès, Olivier Carton, Gabriele Puppis with Sreejith A.V. It was funded by the ERC grant GALE.
Diego Figueira (LaBRI, University of Bordeaux, France)
On reflexive-transitive navigation in the presence of data values (Slides: pdf)
Abstract:
When working on data words or data trees, it is often important to be able to compare data values from positions far apart. In modal or navigational languages, such as LTL or XPath, this is done using transitive closure modalities (such as Future, or Descendant). As it turns out, this type of modalities very easily makes the satisfiability problem either undecidable or with non-primitive recursive complexity. However, in many of these cases, replacing modalities with their reflexive-transitive counterpart (as opposed to only transitive) entails a series of monotonicity properties useful to gain decidability, even elementarity. The purpose of this talk is to give an idea of why adding reflexivity improves things.
The results I will present are based on my work appeared in LICS'11 and PODS'13.
Pierre Ganty (IMDEA Software Institute, Madrid, Spain)
Parameterized Verification of Asynchronous Shared-Memory Systems
Abstract:
We study systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem. We consider the cases where leader and contributors are in turn modeled by finite-state machines, pushdown machines, and Turing machines. Our proofs use a mix of combinatorial properties of the model and some language-theoretic constructions of independent interest. We will also present preliminary results about the liveness verification problem.
Christoph Haase (LSV, ENS Cachan, France)
Pushing the boundaries of the complexity of the reachability problem in vector addition systems one step at a time (Slides: pdf)
Abstract:
Determining the complexity of the reachability problem for vector addition systems with states is a long-standing open problem. Long known to be decidable, in the general case the problem to this day lacks any complexity upper bound whatsoever.
In this talk, I will survey some recent results on the complexity of reachability in subclasses of vector addition systems. On the one hand, I will draw a comprehensive picture of the progress that has been made and the influence it has had on other areas. On the other hand, I will also discuss on a high level some techniques that have allowed for tightening upper bounds, and in particular elaborate on a recent result which states that reachability in two-dimensional vector addition systems is PSpace-complete. The talk will be concluded by a discussion on open problems and current challenges.
Marcin Jurdziński (University of Warwick, UK)
The perfect half-spaces technique for multi-dimensional energy games (Slides: pdf)
Abstract:
Mean-payoff and energy games are closely related, for example the battery user has a winning strategy in an arbitrary-initial-charge energy game if and only if the value of the corresponding mean-payoff game is non-negative. This relationship breaks down for multi-dimensional mean-payoff and energy games, and hence techniques developed for solving multi-dimensional mean-payoff games cannot be directly applied to energy games. We show how to generalize the hyperplane-separation technique (Chatterjee and Velner, 2013) from multi-dimensional mean-payoff games to multi-dimensional energy games, in order to achieve an algorithm for solving the latter whose running time is exponential only in the dimension, but not in the size of the game graph. This answers an open question whether arbitrary-initial-charge energy games can be solved in pseudo-polynomial time for dimensions 3 or larger (Chaloupka, 2010). It also allows to improve the complexity of solving known-initial-charge multi-dimensional energy games from non-elementary (Brazdil, Jancar and Kucera, 2010) to 2EXPTIME, thus establishing 2EXPTIME-completeness.
This is joint work with Ranko Lazic and Sylvain Schmitz.
Manfred Kufleitner (University of Stuttgart, Germany)
Omega-terms and automata
Abstract:
Many interesting subclasses such as first-order definable languages or piecewise testable languages can algebraically be represented as identities of omega-terms. When the input is given as a DFA, then (for any non-trivial identity) this always leads to an NL-hard problem in PSPACE. In the case of first-order languages, the problem is PSPACE-complete whereas for piecewise testable languages it is in NL. In this talk we first give a brief survey on the known results in this area. Second, we show that, when given a DFA A, for every level of the FO2 quantifier alternation hierarchy it is NL-complete to check whether L(A) is definable in this fragment.
Akash Lal (MSR Bengaluru, India)
A Program Transformation for Faster Goal-Directed Search (Slides: pptx)
Abstract:
A goal-directed search attempts to reveal only relevant information needed to establish reachability (or unreachability) of the goal from the initial state of the program. The further apart the goal is from the initial state, the harder it can get to establish what is relevant. This paper addresses this concern in the context of programs with assertions that may be nested deeply inside its call graph-thus, far away interprocedurally from main. We present a source-to-source transformation on programs that lifts all assertions in the input program to the entry procedure of the output program, thus, revealing more information about the assertions close to the entry of the program. The transformation is easy to implement and applies to sequential as well as concurrent programs. We empirically validate using multiple goal-directed verifiers that applying this transformation before invoking the verifier results in significant speedups, sometimes up to an order of magnitude. This is joint work with Shaz Qadeer and it received the best paper award at FMCAD 2014.
Anthony Widjaja Lin (Yale-NUS College, Singapore)
Parikh's Theorem: Complexity and Applications (Slides: pdf)
Abstract:
Parikh's Theorem is a classic result in automata theory (proven by Rohit Parikh in 1961) that semilinear sets are effectively equivalent with the sets of letter-counts (a.k.a. Parikh images) of regular languages and those of context-free languages. The results have abundant applications in various areas in computer science including databases and verification. In this talk, we are going to take a look at the computational and descriptional complexity aspects of Parikh's Theorem. Surprisingly, despite their equivalence, Parikh images of regular languages and context-free grammars differ in terms of their computational/descriptional complexity. We will sample a few known constructions for Parikh images of regular languages and context-free grammars (e.g. by Chrobak-Martinez, Esparza, Kopczynski-Lin, and Verma et al.). We will also sample a few applications in databases/verification and give a few hints how to derive the best complexity for a specific application. We will close the talk with some challenges.
Jerome Leroux (LaBRI, University of Bordeaux, France)
Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems (Slides: pdf)
Abstract:
This paper studies the boundedness and termination problems for vector addition systems equipped with one stack. We introduce an algorithm, inspired by the Karp & Miller algorithm, that solves both problems for the larger class of well-structured pushdown systems. We show that the worst-case running time of this algorithm is hyper-Ackermannian for pushdown vector addition systems. For the upper bound, we introduce the notion of bad nested words over a well-quasi-ordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyper-Ackermannian upper bound for the length of bad nested words over vectors of natural numbers. For the lower bound, we exhibit a family of pushdown vector addition systems with finite but large reachability sets (hyper-Ackermannian). This is a joint work with M. Praveen and Grégoire Sutre. The full paper is available as a CSL-LICS'14 paper.
Rupak Majumdar (MPI Kaiserslautern, Germany)
What's decidable about asynchronous programs? (Slides: pptx)
Abstract:
Asynchronous event-driven programming has become a central model for building responsive and efficient software systems: from low-level kernel modules, device drivers, and embedded systems, to consumer applications on mobile and web browser platforms. Being fundamentally concurrent, such systems are vulnerable to subtle programming errors which, in principle, could be systematically discovered with automated techniques such as model checking.
We will discuss recent formal models for asynchronous event-driven programs and show that safety verification remains decidable for these, quite expressive, programming models. In particular, the formal models allow dynamic creation of concurrent tasks, events, task buffers, and threads, and precisely capture the interaction between these objects. Along the way, I will show how models of asynchronous programs correspond to other concurrency models such as Petri nets, Petri nets with resets, depth-bounded pi-calculus, and data nets. Our decidability results show reductions from asynchronous programs to these models. We also show undecidability results for simple extensions of these models.
Thomas Place (LaBRI, University of Bordeaux, France)
Climbing Up the Quantifier Alternation Hierarchy of First-Order Logic over Words
Abstract:
It is natural to classify first-order logic formulas by counting the number of alternations between existential and universal quantifiers in their prenex normal form. This defines the quantifier alternation hierarchy of first-order logic. In formal languages theory, a longstanding open problem has been associated to this hierarchy: given as input a level in the hierarchy and a first-order definable language, can we decide whether the language is definable by a formula of the level in question.
For a long time this problem has been open above level 3/2 (formulas having only 1 alternation). Recently, progress were made for higher levels by investigating the decidability of a deeper decision problem called separation. I will discuss these new results and explain why getting a solution for the whole hierarchy remains a challenging problem.
Gabriele Puppis (LaBRI, University of Bordeaux, France)
The Cost of Repairs (Slides: pdf)
Abstract:
What do you do if a computational object (e.g., a document, a program trace) fails a specification? An obvious approach is to perform a "repair": modify the object minimally to get something that satisfies the constraints. This approach has been extensively investigated in the database community for relational integrity constraints, and in the AI community for propositional logics. Different modification operators have been considered on the basis of the application scenarios. For instance, a repair of an XML document usually consists of applying to the underlying tree structure a certain number of editing operations such as relabelings, deletions, and insertions of nodes.
In this talk I will survey a series of results related to the worst-case cost of repairing documents between regular specifications. More precisely, I will focus on the number of edits that are needed to get from a document (e.g. a word or a tree) that satisfies a source specification (e.g. a regular language S) to some document that satisfies a target specification (e.g. a regular language T). As this number may well be unbounded, I will consider the problem of determining those pairs of languages (S,T) such that one can get from any word/tree in S to a word/tree in T using a finite, uniformly bounded number of editing operations. I will give effective characterizations of these pairs when S and T are given by finite state automata (word case) or stepwise tree automata (tree case), and derive some complexity bounds for the corresponding decision problems. Finally, I will briefly mention some variants of these problems where the repair is produced in an online way (streaming setting), or where the cost is calculated as the worst-case ratio between the number of edits and the size of the document (normalized cost).
The presentation is based on joint works with Michael Benedikt, Pierre Bouhris, Cristian Riveros, and Sławek Staworko.
M Praveen (CMI, Chennai, India)
Defining relations on graphs: how hard is it in the presence of node partitions? (Slides: pdf)
Abstract:
Designing query languages for graph structured data is an active field of research. Evaluating a query on a graph results in a relation on the set of its nodes. In other words, a query is a mechanism for defining relations on a graph. Some relations may not be definable by any query in a given language. This leads to the following question: given a query language and a relation, does there exist a query in the given language that defines the given relation? This is called the definability problem. When the given query language is standard regular expressions, the definability problem is known to be Pspace-complete.
The model of graphs can be extended by labeling nodes with values from an infinite domain. These labels induce a partition on the set of nodes: two nodes are equivalent if they are labeled by the same value. Query languages can also be extended to make use of this equivalence. Two such extensions are Regular Expressions with Memory (REM) and Regular Expressions with Equality (REE). We study the complexity of the definability problem in this extended model when the query language is either REM or REE. We show that the definability problem is Expspace-complete when the query language is REM, and it is Pspace-complete when the query language is REE. In addition, when the query language is a union of conjunctive queries based on REM or REE, we show coNP-completeness. This is joint work with B Srivathsan.
Jean-François Raskin (ULB, Brussels, Belgium)
Variations on the stochastic shortest path problem
Abstract:
In this paper,we revisit the stochastic shortest path problem, and show how recent results allow one to improve over the classical solutions: we present algorithms to synthesize strategies with multiple guarantees on the distribution of the length of paths reaching a given target, rather than simply minimizing its expected value. The concepts and algorithms that we propose here are applications of more general results that have been obtained recently for Markov decision processes and that are described in a series of recent papers.
Arnaud Sangnier (LIAFA, University Paris 7, France)
Distributed local strategies in broadcast networks (Slides: pdf)
Abstract:
We study the problem of reaching a specific control state in networks with a parameterized number of identical processes communicating with broadcast. We restrict our attention to the executions where all the processes follow the same local strategy which, given the past performed action and received messages, provides the next action to be performed. We show that the reachability problem under local strategy is NP-complete with the assumption that the communication topology is reconfigurable, i.e. the set of receivers is chosen non deterministically at each step. The same problem is decidable and non-primitive recursive when the communication is performed in a clique topology where all the participants receive the emitted messages. This complexity result still holds when each process performs an action in a round-robin fashion and with reconfigurable topologies. But, when both round-robin executions and clique topology are considered, the reachability problem under local strategy is undecidable.
This is a joint work with Nathalie Bertrand and Paulin Fournier.
Sylvain Schmitz (LSV, ENS Cachan, France)
Towards Complexity Upper Bounds for VASS Reachability
Abstract:
More than 30 years after their inception, the complexity of the algorithms for VASS reachability is still an open issue. By examining the decomposition techniques of Mayr, Kosaraju, and Lambert, and using more recent results on the complexity of termination thanks to well quasi orders and well orders, I will show how to obtain (fast-growing) complexity upper bounds. The talk will be based on ongoing work with Jérôme Leroux.
Simoni Shah (TIFR, Mumbai, India)
Recursive po2DFA: Hierarchical Automata for FO-definable languages. (Slides: pdf)
Abstract:
A recursive generalization of the Partially Ordered 2-Way Deterministic Automata (PO2DFA) of Schwentik, Therien and Vollmer is investigated. The resulting automata, called rPO2DFA, are hierarchically structured with rPO2DF[k] at level k being PO2DFA but having the transitions guarded by boolean combinations of lower level rPO2DFA[k-1] automata: in this sense rPO2DFA are a special kind of 2-way alternating automata.
The expressive power of these recursive rPO2DFA automata is studied and shown to coincide with FO-definable languages with an interesting hierarchical structure which we call the recursion hierarchy. Pinning down the exact expressive power of our automata, we show that rPO2DFA[k] are expressively equivalent to the k-th level of the recursive deterministic temporal logic TL[X_\phi,Y_\phi][k] of Kroger ([Kr84]). This logic was shown by Borchert ([B004]) to exactly characterize the k-fold weakly iterated block product of the variety DA. Thus, rPO2DFA provide an automaton characterization of the hierarchy of FO definable languages formed by the weakly iterated block product of variety DA.
We compare our recursion hierarchy with the alternation hierarchy of FO as well as the until-since hierarchy of LTL. On one hand, all of the STAIR languages (used to separate levels of the Until-Since hierarchy) can be expressed within level two of the recursion hierarchy. We show that rPO2DFA[k] can express Until-Since formulas of modal depth k with arbitrary nesting of unary operators F and P. Thus the recursion hierarchy grows faster than the Until-Since hierarchy. On the other hand, the level \Sigma_2 of the alternation hierarchy intersects with all levels of the recursion hierarchy. A novel and interesting characterization of the bounded-buffer languages using the rPO2DFA gives us some insight into the kind of languages that are equally "hard" for levels of the recursive as well as alternation hierarchy.
B Srivathsan (CMI, Chennai, India)
Fast detection of cycles in timed automata (Slides: pdf)
Abstract:
We will present an algorithm to detect if a cycle in a timed automaton can be iterated infinitely often. Existing solutions in tools have a complexity which is exponential in the number of clocks. Our method is polynomial. This method can be incorporated in algorithms for verifying Büchi properties on timed automata. Experiments show a significant reduction in search space. This is joint work with A. Deshpande, F. Herbreteau, T.T. Tran and I. Walukiewicz.
Ashutosh Trivedi (IIT Bombay, Mumbai, India)
Bounded-Rate Multi-Mode Systems Based Motion Planning
Abstract:
Hybrid automata are a natural and expressive formalism to model systems that exhibit both discrete and continuous behavior. However, the applications of hybrid automata in analyzing cyber-physical systems have been rather limited due to undecidability of simple verification problems such as reachability. This drawback of hybrid automata has fueled the investigation of the so-called compositional methodology to design complex system by sequentially composing well-understood lower-level components. This methodology has, for example, been used in the context of the motion planning problem for mobile robots, where the task is to move a robot along a pre-specified trajectory with arbitrary precision by sequentially composing a set of well-studied simple motion primitives, such as "move left", "move right" and "go straight". In this talk, we summarize some of our recent results related to efficient solution of motion planning problem for systems whose motion primitives are given as constant-rate vectors with uncertainties.
References
Marc Zeitoun (LaBRI, University of Bordeaux, France)
The separation problem: an introduction and a transfer theorem. (Slides: pdf)
Abstract:
The separation problem is a generalization of the membership problem, which is itself used as the standard mean to capture the expressiveness of high-level descriptive formalisms. I will first present this problem for languages of finite words, then explain why it is a promising track to obtain new expressiveness results, and finally illustrate this on an example: the enrichment of a first-order fragment with the successor relation admits a decidable separation problem if so does the original fragment. This result was already known in an algebraic setting (B. Steinberg, 2001). I will sketch an alternative simple proof and present some consequences.
Martin Zimmermann (Saarland University, Saarbrücken, Germany)
How Much Lookahead is Needed to Win Infinite Games (Slides: pdf)
Abstract:
Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. For regular winning conditions, it is known that such games can be solved in doubly-exponential time and that doubly-exponential lookahead is sufficient.
We improve upon both results by giving an exponential-time algorithm and an exponential upper bound on the lookahead. This is complemented by exponential lower bounds on lookahead and by showing PSPACE-hardness of the solution problem for restricted fragments of regular winning conditions, namely reachability and safety conditions.
Joint work with Felix Klein (Saarland University).