Centre Fédéré en Vérification

Recursive Markov Chains (RMCs) are a natural abstract model of procedural probabilistic programs and other systems involving both recursion and probability. RMCs define a class of denumerable Markov chains with a rich theory generalizing that of multi-type Branching (stochastic) Processes and Stochastic Context-Free Grammars, and they are tightly related to probabilistic Pushdown Systems. Recursive Markov Decision Processes (RMDPs) and Recursive Stochastic Games (RSGs) extend RMCs with a controller and two adversarial players, respectively.

In a series of recent papers we have studied central algorithmic analysis and verification questions for RMCs, RMDPs, and RSGs, providing some strong upper and lower bounds on the complexity of key algorithmic problems.

I will provide a broad survey of this work, indicate some of the main techniques involved in our analyses, discuss potential application domains, and indicate some of the many directions for future research.

This talk describes joint work with Mihalis Yannakakis (Columbia U.) contained in a series of recent papers that appear at: STACS'05, TACAS'05, ICALP'05, QEST'05, and STACS'06, and in a submitted paper.

SPIN is a well-known, state-of-the-art model checker for the verification of distributed systems. This talk will show that SPIN can be used for much more than verifying software systems and it is argued that SPIN should be part of every computer science engineer's toolbox. For example, the talk will illustrate how SPIN can be used to solve optimization problems and as a database engine for XML databases. Furthermore, some general patterns to contruct efficient PROMELA models will be discussed and techniques will be presented how to use SPIN in the most effective way. The talk itself will have a tutorial-like presentation style and the objective is to make attendees (even more) enthusiastic about explicit state model checkers.

The planned aim of the talk is to highlight the author's main results and techniques dealing with decidability and complexity questions for bisimilarity. This includes the general result of undecidability of (behavioural) equivalences on (labelled place/transition) Petri nets, and PSPACE-completeness of bisimilarity on Basic Parallel Processes, using the technique of so called DD-functions. Also a fresh result (Jancar, Srba 2005) will be demonstrated, as a new application of so called Defender's choice technique; it shows the undecidability of bisimilarity on Type -1 systems (with prefix rewrite rules R --> w), by which an open question posed by Senizergues and Stirling is answered.

We address the problem of selecting test cases, for testing the conformance of a black box implementation of a reactive system with respect to its specification.. In this talk, we focus on models of infinite state systems represented by automata extended with variables (ioSTS). We first revisit the ioco testing theory of Tretmans, where the conformance relation defining conformant implementations wrt a specification is a partial inclusion of visible behaviors. We then consider test selection using test purposes, which are specified by ioSTS reachability observers, and allow to focus selection on some behaviours to be tested. The goal is to produce an ioSTS test case that checks both non- conformance and acceptance by the test purpose. The problem reduces to co- reachability analysis, which is undecidable for ioSTS. However, we show that an approximated analysis (using e.g. abstract interpretation) still allows to produce sound test cases. An adaptation of the approach can be used to generate test cases that may detect non-conformance and violations of safety properties, on both the implementation and the specification, thus complementing (a potentially partial) verification of safety properties on the specification.

Standard abstract model checking relies on abstract Kripke structures which approximate the concrete model by gluing together indistinguishable states, namely by a partition of the concrete state space. Strong preservation for a specification language L encodes the equivalence of concrete and abstract model checking of formulas in L. We show how abstract interpretation can be used to design abstract models which are more general than abstract Kripke structures. Accordingly, strong preservation can be generalized to this abstract interpretation-based model checking framework. This also provides a generalized abstract interpretation-based view of partition refinement algorithms for reducing the state space of a Kripke structure in order to obtain strong preservation for a specification language L. In particular, the well-known Paige and Tarjan algorithm reduces the state space in order to obtain bisimulation, that is strong preservation for CTL or mu-calculus. We show how our abstract interpretation-based view leads to design a generalized Paige-Tarjan algorithm for computing the minimal refinement of a generic abstract model which is strongly preserving for a generic language.