1 Goal of the Project
ProNobis is an
ARC (Action
de Recherche Concertée) supported by
INRIA.
The goal of the ProNobis project is to explore mixing probability and
non-determinism in the semantics of transition systems, and also of
programming languages. Finding good models mixing both aspects is
still an art in its infancy.
Rather surprisingly, good ideas have been around for a long time, from
various “theories of evidence” invented by statisticians in the
1960-80's (Dempster, Shafer, Walley) to theories of “games” promoted
by economists in the same period (Shapley, Scarf, Rosenmuller, Gilboa,
Schmeidler). These ideas seem to have been largely ignored in
computer science. One might legitimately say this is the starting
point of the ProNobis proposal. We still have to understand how these
theories adapt to computer science, and how they compare together, and
with other proposals stemming from computer science.
In ProNobis, we plan to keep on eye on applications of these to
typically computer related problems, in particular to problems
stemming from security. Several interesting verification problems
related to security involve proving that two processes are
contextually equivalent. This usally uses notions such as
bisimulation, which need to be better understood in a setting where
probabilities, external non-determinism (choosing which action to fire
in Markov decision processes), and internal non-determinism (where no
visible action distinguishes between the various alternatives).
The project started January 2006, and has a duration of two years.
More details can be found in the
ProNobis proposal (slightly edited).