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