A Modular Logic for Reasoning on Concurrent Markovian Systems
Complex networks are often modeled as stochastic processes, to encapsulate a lack of knowledge or inherent non-determinism. Such systems are frequently modular in nature, consisting of parts which are systems in their own right. Their global behaviour depends on the behaviour of their parts and on the links which connect them.
This talk focuses on identifying the mathematical ingredients that support such structures and investigates the possibility of defining a general qualitative and quantitative logical framework appropriate for modular analysis of concurrent Markovian systems. By modular analysis we mean a scale-up approach that proves properties of an upper level system from the properties of its subsystems. Our models are continuous (-space and –time) Markov processes defined for analytic sets with an inbuilt modular structure. We introduce a completely axiomatized polyadic modal logic able to specify both algebraic and coalgebraic properties of the models.
This is a joint work with Luca Cardelli (Microsoft Research Cambridge) and Kim G. Larsen (Aalborg University).