Date and Time: Thursday, 3 December 2009, 15:45 - 16:45

Location: HG 6.96

Speaker: MohammadReza Mousavi (OAS)

Title: Decompositional Reasoning About Past

Abstract:

State-space explosion is a major obstacle in model checking logical properties. One approach to combat this problem is (de)compositional model checking, where by the global property to be model checked is decomposed (or quotiented) into local properties of (possibly unknown) components. In this talk, we introduce a decomposition technique for Hennessy-Milner logic with past and for its extension with recursively defined formulae. This is particularly interesting in the light of recent developments concerning reversible processes and knowledge representation (epistemic aspects) inside process algebra and also the use of past formulae in program verification.

Joint work with Luca Aceto (Reykjavik), Arnar Birgisson (Chalmers) and Anna Ingolfsdottir (Reykjavik).