WP1 - Quantitative Analysis of Concurrent Program Behaviour
Partners Involved: SAU / RWTH / TUD / TUE / UNC / UBA
It is often the case that random algorithms introduce more efficient solutions or even some solution that are impossible by traditional algorithms, particularly in distributed systems as is the case of leader election protocols, byzantine agreement protocols or security or anonymity protocols. In addition, random behaviour is also present in the environment in which the system is immersed and interacting with. This factors can be quantified like in the case of the probability of losing a message, the average time between fault occurrences, or the availability of a resource. Under this work package, we will focus on understanding and analyzing this type of systems.
- Generating and visualizing counterexample in probabilistic model checkers. The major advantage of a model checker is not checking the validity of a property, but producing counterexamples in the case the property does not hold. This feature, that has been present in traditional model checkers from the beginning, took some time to be understood in probabilistic model checkers. It is only recently that the first approaches appeared for DTMCs and MDPs. Participants in this WP were responsible for most of these techniques. We propose to implement these techniques by integrating them in probabilistic model checkers such as PRISM or MRMC, and extend it also to CTMC and CTMDP model checkers.
- Languages for modelling stochastic timed systems. System models are specified through specification languages. Their semantics should be rigorously understood from a mathematical point of view. Many of us have been involved in the definition of probabilistic or stochastic process calculi as well as complex languages such as MoDeST or a stochastic extension of mCRL2. We propose to proceed further with the study of these languages as well as understanding deeper the foundational aspects of non-deterministic and probabilistic systems with continuous probability.
- Limiting the power of schedulers. Schedulers are the fundamental concept that allows for the understanding of probabilistic behaviour on models that have also non- determinism (i.e. MDPs). It is already known that for the study of distributed systems or security protocols not every scheduler defines a coherent probabilistic behaviour (see WP3.3). Classes of coherent schedulers have been defined by members of this project, but we also know that they may lead to undecidable problems. We propose to further study this topic aiming to obtain classes of schedulers that are related to different classes of computable schedulers such as polynomial classes.
- Parameter synthesis. Whereas the verification of probabilistic models is focused on a single model instance with all quantitative information fixed, a more interesting, though more challenging question is whether it is possible to synthesize the parameter ranges for which a parameterized probabilistic models satisfies a given temporal logic formula. Though some progress has recently been made for discrete-time models, the bridge towards continuous-time models such as CTMCs has not been made. We will study parameter synthesis for timed reachability and long-run objectives.
- Invariant generation in probabilistic models. Loop invariants are crucial to prove properties of programs and its derivation of major complexity. Independently, members participating in this WP extended the idea of predicate abstraction generation in non-deterministic programs to programs containing also probabilistic decisions. Both methods share some fundamental ideas, but differ in the way the computation of the invariant is carried out. We propose to unify both approaches aiming to obtain a stronger tool to automatically verify complex probabilistic and nondeterministic programs.
- Parallel implementations of probabilistic model checkers. Apart from the inherent state explosion problem, the performance of probabilistic model checkers is also heavily dependent on numerical calculations. This kind of computation involve matrix and vector manipulation which are amenable for parallelization. We propose to study the implementation of model checkers on different kinds of High Performance Computing platforms involving both usual multicore-shared memory architecture and GPGPU architectures.
- Partial specification of probabilistic systems. Probabilistic automata (PA)are a widely-recognized framework for the specification and analysis of systems with non- deterministic and stochastic behaviours. Although refinement relations between PA have been studied in the literature, a full-fledged specification and abstraction theory is still missing. We plan to study abstractions of PA (such as interval and constraint-based abstractions), with the aim to define a specification theory. Such theory supports both satisfaction and refinement operators, together with classical stepwise design operators. To that end, we aim to study a mixture of modal transition systems (which define a specification theory for transition systems), and combine this with compositional abstraction techniques.
