2015 -- Approximate Reasoning for Stochastic Markovian Systems

Project 4181-00360 awarded in June 2015 by The Danish Council for Independent Research.
Starting date - August 2015
Budget - DKK 5,574,000
Prof. Kim Larsen (AAU)
Prof. Prakash Panangaden (McGill, Canada)
Prof. Dexter Kozen (Cornell, USA)
Prof. James Worrell (Oxford, UK)
Prof. Luca Cardelli (Microsoft Research Cambridge, UK).

Complex systems that combine artificial (software-based) components and natural components are the new challenges today in Engineering and Technology. They can be found in areas as diverse as aerospace, automotive engineering, chemical processes, civil infrastructures, energy, healthcare, manufacturing, transportation, and consumer appliances. When we analyse these systems, we often represent them as stochastic processes to model ignorance, uncertainty or inherent randomness. The stochastic processes are mathematical models that use probabilistic reasoning to abstract the missing information. In this Monograph we present a series of research results that we obtained while aiming to develop a logical framework that will help us understanding the knowledge transfer between models and the systems being modelled. The goal is to be able to understand when the properties observed on models can be true about the modelled system. To do this, we have studied the logical and mathematical foundations of an approximation theory for stochastic systems that formalizes this knowledge transfer and supports the process of modelling and simulation of complex systems. This research is multidisciplinary, combining knowledge from Logic, Topology, Measure Theory, Metric Spaces, Transition Systems as well as applied Computer Science and Engineering; the results are expected to have a significant impact in all these fields.



2010 -- 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

Elite Research Conference 2011 (EliteForsk Konference) ############################################# My link on Sapere Aude EliteForsk website

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.

Related Tools:
On-the-fly Exact Computation of Bisimilarity Distances.