For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Christian Johansen (Norwegian University of Science and Technology), invited by the Cosynus team.

Link to the online conference

Abstract: This talk presents a modal logic over HDAs which incorporates two modalities for reasoning about “during” and “after”. This higher dimensional modal logic (HDML) is decidable and an “almost” complete axiomatic system exists for it. When the HDA model is restricted to Kripke structures, a syntactic restriction of HDML becomes the standard modal logic. One can isolate the class of HDAs that encode Mazurkiewicz traces and show how HDML, with natural definitions of corresponding Until operators, can be restricted to LTrL (the linear time temporal logic over Mazurkiewicz traces) or the branching time ISTL. A preliminary study of the expressiveness of the basic HDML language wrt. bisimulations has concluded that HDML captures the split-bisimulation. One can also add backward-looking modalities (i.e., past modalities) so to increase the expressiveness so to be able to capture the hereditary history-preserving bisimulation. Classical examples from the literature that are used to distinguish one-or-another bisimulation can be distinguished in this hHDML using a specially crafted formula. I will show these interesting examples and talk about the respective literature, if time permits.

The list of next seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/calendar.ics