Talks and Slides

  • Print

 

Talks


Automata Theoretic Approach for model checking of Open  Probabilistic systems
Prasad A. Sistla
University of Illinois Chicago


Abstract
This talk considers the use of probabilistic automata for model checking open probabilistic systems. In particular,  we present a class of probabilistic automata, called 1-level Hierarchical Probabilistic Automata. We show that these automata are powerful enough to express non-regular languages. We also show that non-emptiness, universality problems,  for these automata are decidable. We also show how failure prone open  systems can be modeled by these automata, and can be verified automatically using the presented decision procedures. Some preliminary experimental illustrating the applications of the approaches will be presented.

Slides in PDF


Parameterized and infinite branching WSTS
Alain Finkel
ENS Cachan


Abstract
Most decidability results concerning well-structured transition systems apply to the finitely branching variant.  Yet some models (inserting automata, omega-Petri nets, ...) are naturally  infinitely branching.  Here we develop tools to handle infinitely branching WSTS by exploiting the crucial property that in the (ideal) completion of a well-quasi-ordered set, downward-closed sets are inite unions of ideals. Then, using these tools, we derive decidability results and we delineate the undecidability frontier in the case of the termination, the control-state maintainability and the coverability problems.  Coverability and boundedness under new effectivity conditions are shown decidable

Slides in PDF


Beyond well structured systems
Ahmed Rezine
Linkoeping University

Abstract
Multi-threaded programs may synchronise in subtle ways. For instance, they can use integer variables to count the number of threads satisfying some property in order to implement dynamic barriers or to organise their interleaved execution. We address the problem of automatically establishing deadlock freedom and safety in general for multi-threaded programs generating an arbitrary number of concurrent processes. For this purpose, we explain how we leverage on simple techniques to derive "counting invariants", i.e., invariants that relate the number or processes in a given location to the values of the program variables. We use these invariants and leverage on predicate abstraction techniques in order to generate non-monotonic counter machine reachability problems that faithfully capture the correctness of the safety property.  Solving the reachability problems: We propose several new lazy heuristics for checking reachability of non monotonic counter machines. The idea is to localise the refinement of well quasi orderings in order to allow for a decidable reachability analysis on possibly infinite abstractions that are well structured wrt. these orderings. The orderings can be refined based on obtained false positives in a CEGAR like fashion. This allows for the verification of systems that are not monotonic and are hence inherently beyond the reach of classical well-structured-systems-based analysis techniques. Unlike classical lazy predicate abstraction, we show the feasibility of the approach even for such systems with infinite control. Our heuristics are applicable both in backward and in forward as shown by our experiments.
 
Slides in PDF

Timed extensions of Petri nets with data
Fernando Rosa Velardo
UCM


Abstract 
In this talk I will present our work about timed extensions of variations of Petri nets in which tokens carry data. In particular, I will focus on the case in which the data carried by tokens is unstructured and unordered, sometimes called pure names, that can be thought as the identifier of an instance. This model has been called nu-Petri nets or Unordered Petri Data Nets in the literature, and can serve as the basis of models in which an arbitrary amount of processes (modelled as Petri nets) interact via sychronous or buffered asynchronous communication. We first consider the typical timed-arc extension of Petri nets, in which tokens (also) carry a real valued clock and arcs are labelled by a guard that restricts the age of consumed tokens. We prove this model to be Turing-complete. Even in the case of two clocks per name (that is, for each name there are only two tokens for which the age is relevant), we prove undecidability of safety properties (namely control-state reachability or coverability). Then we study the case in which each name (each instance) carries only one clock. We prove that in this case safety properties are decidable, by instantiating the framework of WSTS using similar techniques as for the Timed Petri Nets of Abdullah et al. Finally we will discuss some open problems.

Slides in PDF


Liveness in Parameterized Systems
Pierre Ganty
IMDEA Madrid


Abstract
In this talk, we characterize the complexity of liveness verification for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributor processes.  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 case in which processes are modeled by finite-state machines or pushdown machines and the property is given by a Büchi automaton over the alphabet of read and write actions of the leader.  We show that the problem is decidable, and has a surprisingly low complexity: it is NP-complete when all processes are finite-state machines, and is PSPACE-hard and in NEXPTIME when they are pushdown machines. This complexity is lower than for the non-parameterized case: liveness verification of finitely many finite-state machines is PSPACE-complete, and undecidable for two pushdown machines.

Slides in PDF


Adding probabilities to Networks with Selective Broadcast
Arnaud Sangnier
Liafa, Paris


Abstract
In this talk, I will present some recent results for the verification of a model of network with the following characteristics: the number of entities is parametric, communication is performed through selective broadcast (i.e. the set of receivers is chosen at each emission of a message), entities can change their internal state probabilistically and reconfiguration of the communication topology can happen at any time. The semantics of such a model is given in term of an infinite state system with both non deterministic and probabilistic choices. The studied problems are qualitative ones like for instance whether there exists an initial  number of entities and a resolution of the non determinism such that a configuration exhibiting an error state is almost surely reached. We show that all the qualitative reachability problems are decidable and some proofs are based on solving a 2 player game played on the graphs of a network with selective broadcast using parity and safety objectives.

Slides in PDF


Büchi's Theorem: From Fixed Architectures to Parameterized Systems
Benedikt Bollig
LSV Cachan


Abstract
We survey extensions of Büchi's Theorem, stating expressive equivalence of finite automata and MSO logic, to various models of concurrent systems: multi-stack automata, communicating automata, data automata, and parameterized communicating automata. While the former two serve as models of systems with a fixed finite set of processes, the latter two represent parameterized systems, where the number of processes is a priori unknown. All logical characterizations rely on restrictions of the logic and/or the automata model. However, these restrictions are non-trivial and provide a theoretical basis for under-approximate verification of concurrent systems.

Slides in PDF


Verification of Dynamic Register Automata
Mohamed Faouzi Atig
Uppsala University

Abstract: 

We consider the verification problem for Dynamic Register Automata (DRA). DRA extend classical register automata by process creation. In this setting, each process is equipped with a finite set of registers in which the process IDs of other processes can be stored. A process can communicate with processes whose IDs are stored in its registers and can send them the content of its registers. The state reachability problem asks whether a DRA reaches a configuration where at least one process is in an error state. We will  first show that this problem is in general undecidable. This result holds even when we restrict the analysis to configurations where the maximal length of the simple paths in their underlying (un)directed communication graphs are bounded by some constant. Then we will introduce the model of degenerative DRA which allows non-deterministic reset of the registers. We will  prove that for every given DRA, its corresponding degenerative one has the same set of reachable states. While the state reachability of a degenerative DRA remains undecidable, we will  show that the problem becomes decidable with nonprimitive recursive complexity when we restrict the analysis to strongly bounded configurations, i.e. configurations whose underlying undirected graphs have bounded simple paths. Finally, we will consider the class of strongly safe DRA, where all the reachable configurations are assumed to be strongly bounded. We show that for strongly safe DRA, the state reachability problem becomes decidable.  

Slides in PDF

Computing with population protocols
Javier Esparza
TUM

Abstract
Population protocols are a formal model of networks consisting of identical mobile devices. Two devices can interact  and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. We introduce a new notion of computation with population protocols, which exploits their similartity to chemical networks. Computing, say, the satisfiability of a formula, amounts to putting together a sufficiently large amount of a number of chemical reactants, adding water, and keep stirring the solution well until it gets a certain color, say blue for satisfiable and red for unsatisfiable. We present some first results and some open questions on the computational power of this model.

Slides in PDF


Parameterized Verification of Fault-Tolerant Distributed Algorithms and Beyond
Helmut Veith
TU Wien


Distributed algorithms in critical applications are often designed to be fault-tolerant, i.e., to tolerate the fault of a certain fraction of components. While fault tolerant distributed algorithms enable a system to handle hardware faults, they are typically quite complex, and thus a source of subtle software errors themselves. Together, the criticality and the complexity of the algorithms motivate systematic verification efforts by parameterized model checking.

In a series of recent papers, our group has demonstrated that the progress of the last two decades in abstract model checking, SMT, and partial order reduction gives leverage for parameterized model checking techniques that are able to verify non-trivial fault tolerant distributed algorithms. In my talk, I will survey our recent results and discuss the methodological challenges we need to solve towards a broader application of model checking to distributed algorithms.

Slides in PDF


Parameterized Verification of Distributed Broadcast Protocols
Giorgio Delzanno
DIBRIS, University of Genova

Abstract
We report on recent research lines related to a graph-based approach to parameterized verification of formal models of distributed algorithms and protocols. Verification algorithms for restricted classes of models exploit finite-state abstractions, symbolic representations based on graph orderings, the theory of well-structured transition systems, and reachability algorithms based on labeling procedures.

Joint work with P. Abdulla, A. Sangnier, G. Zavattaro, R. Traverso, O. Rezine

Slides in PDF


On Refinement Checking between Libraries of Concurrent Data Structures
Ahmed Bouajjani

LIAFA Paris

Abstract:
We address the problem of checking observational refinement between libraries of concurrent data structures. While this problem is decidable for a fixed number of client threads (when data are also over a bounded domain), it is undecidable when the number of threads is arbitrarily large (even for bounded data structures). We show however that:
- there is a bounding concept definable on the program behaviours under which this problem becomes decidable, and for which it is possible to define an efficient procedure for bug detections (i.e., refinement violations) that allows to achieve both good coverage and scalability.
- for a class of abstract library specifications, including most of the popular data structures such as queues, stacks, etc., refinement checking (of a library against these specifications) can be reduced efficiently to the state reachability problem, and becomes decidable.

This is a joint work with Michael Emmi, Constantin Enea, and Jad Hamza. 

Slides in PDF


Temporal Deductive Verification of Parametrized Systems
Cesar Sanchez
IMDEA Madrid

Abstract
I will present our work aimed at the verification of concurrent datatypes. Concurrent datatypes are variations of classical datatypes aimed to be efficiently executed by several threads simultaneously. We model these systems as parametrized systems executed by an unbounded number of threads. The main difficulty of this verification problems is that typically these parametrized concurrent systems manipulate shared mutable memory in the heap. Our work is based on an extension of deductive temporal methods, which allow to reason about temporal properties of reactive systems by separating two main concerns: (1) the reasoning about the temporal aspects of the executions, and (2) the data being manipulated. For safety properties we propose the use of proof rules (parametrized versions of the invariance rule); for liveness properties we propose the use of parametrized verification diagrams. These methods automatically generate a finite collection of verification conditions from the system description and the intended property. The validity of these verification conditions guarantee that the systems adheres to temporal specification. For automically proving these verification conditions we have designed decision procedures for specific memory shapes. Finally, I will report the results of an empirical evaluation using our prototype tool Leap.

Joint work with Alejandro Sanchez.

Slides in PDF


Synthesizing Cardinality Invariants for Parameterized Systems
Klaus von Gleissenthall
TUM

Abstract 
The cardinality operator is indispensable when specifying and rea- soning about parameterized concurrent/distributed systems. It provides a level of abstraction and conciseness that makes (manual) proofs go through smoothly. Unfortunately, the automation support for such proofs remains elusive due to challenges in counting sets of unbounded program states.  In this talk, I will present #Π a tool that can automatically synthesize cardinality-based proofs of parameterized systems. #Π crucially relies on a sound and precise axiomatization of cardinality for the combined theory of linear arithmetic and arrays. This axiomatization is the key technical contribution of this work.  We show that various parameterized systems, including mutual exclusion and consensus protocols, can be efficiently verified using #Π. Many of them were automatically verified for the first time.

Joint work with Andrey Rybalchenko

Slides in PDF


 Program


          September 4 

9:30-10:15 Sistla 
10:15-11:00 Finkel
11-11:30 Coffe  Break
11:30-12:15 Bollig
12:15-13:00  Veith
13:00-14:30 Lunch break
14:30-15:15 Rezine
15:15-16:00 Sanchez
16:00-16:30 Coffee break 
16:30-17:15 Esparza
 
September 5
 
9:30-10:15   Bouajjani 
10:15-11:00 Rosa Velardo
11-11:30 Coffe  Break
11:30-12:15 Delzanno
12:15-13:00 Sangnier
13:00-14:30 Lunch break
14:30-15:15 Ganty
15:15-16:00 Atig
16:00-16:30 Coffee break 
16:30-17:15 von Gleissenthall