## Talks and Slides

- Details
- Category: General Information
- Published: Saturday, 21 February 2015 14:38
- Written by Super User
- Hits: 1810

**Automata Theoretic Approach for model checking of Open Probabilistic systems****Prasad A. SistlaUniversity 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.

**Parameterized and infinite branching WSTSAlain FinkelENS 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

**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.

**Timed extensions of Petri nets with data****Fernando Rosa VelardoUCM**

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.

**Liveness in Parameterized Systems****Pierre GantyIMDEA 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.

**Adding probabilities to Networks with Selective Broadcast****Arnaud SangnierLiafa, 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.

**Büchi's Theorem: From Fixed Architectures to Parameterized SystemsBenedikt BolligLSV 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.

**Verification of Dynamic Register Automata****Mohamed Faouzi AtigUppsala University**

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.

**Computing with population protocolsJavier EsparzaTUM**

AbstractPopulation 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 BeyondHelmut VeithTU 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.

**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

**On Refinement Checking between Libraries of Concurrent Data StructuresAhmed 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.

**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.

**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

** September 4 **

9:30-10:15 Sistla10:15-11:00 Finkel11-11:30 Coffe Break11:30-12:15 Bollig12:15-13:00 Veith13:00-14:30 Lunch break14:30-15:15 Rezine15:15-16:00 Sanchez16:00-16:30 Coffee break16:30-17:15 EsparzaSeptember 59:30-10:15 Bouajjani10:15-11:00 Rosa Velardo11-11:30 Coffe Break11:30-12:15 Delzanno12:15-13:00 Sangnier13:00-14:30 Lunch break14:30-15:15 Ganty15:15-16:00 Atig16:00-16:30 Coffee break16:30-17:15 von Gleissenthall