Modular Markovian Logics for Analysis of Stochastic Concurrent Systems

Individual Research Grant (Project 10-085054) awarded in May 2010 by The Danish Council for Independent Research.
Starting date - October 2010
Budget - DKK 1,728,000
Collaborators - Prof. Kim Larsen, Prof. Arne Skou (Aalborg University) and Prof. Luca Cardelli (Microsoft Research Cambridge, UK).

Sapere Aude: DFF-Young Researchers Grant awarded in December 2010 by The Danish Council for Independent Research.
Budget - DKK 950,000
Post Doctoral collaborator - ongoing recruiting process

Abstract in English:
Many man-made and natural systems such as computational, social, financial, biological, and ecological are modelled as stochastic processes, to encapsulate both a lack of knowledge and inherent randomness. Such systems are frequently modular in nature, consisting of parts which are systems in their own right: the global behaviour depends on both the behaviour of the parts and on the links ruling their interactions. To say something global, it is necessary to integrate local information in a logical way.
The result of the project will be a logical framework with efficient reasoning techniques to support proving global properties of stochastic systems from properties of their subsystems, addressing a key problem in complex systems. The development will combine the expertise of the applicant in logics for stochastic, probabilistic and concurrent-distributed systems with that of the sponsor in probabilistic systems and their logics. The framework will be tested using challenging examples from embedded systems, provided by Center for Embedded Software Systems (CISS) at Aalborg University.

Abstract in Danish:
Mange menneskeskabte og naturlige systemer - såsom IT, sociale, finansielle, biologiske og økologiske - bliver ofte modelleret som stokastiske processer, da man herved får indkapslet både mangel på præcis viden og systemernes grad af tilfældighed. Sådanne systemer er ofte modulære i deres natur og består af komponenter, der i sig selv er systemer: Den totale adfærd afhænger både af delsystemernes adfærd og af de forbindelser, der styrer deres interaktion. For at kunne udtale sig om den totale adfærd, er det derfor nødvendigt at integrere lokal information på systematisk vis.
Resultatet af projektet vil være et logisk system med effektive ræsonneringsteknikker, der understøtter beviser for globale egenskaber ved stokastiske processer ud fra egenskaber om deres delsystemer. Herved adresseres et nøgleproblem vedrørende komplekse systemer, og projektet vil kombinere ansøgerens ekspertise i logikker til stokastiske, probabilistiske, samtidige -og distribuerede systemer med værtsinstitutionens ekspertise i probabilistiske systemer og deres logikker. Det resulterende logiske system vil blive afprøvet ved brug af udfordrende eksempler indenfor indlejrede systemer, som vil blive leveret af Center for Indlejrede Software Systemer (CISS), Aalborg Universitet.