Laboratoire d'informatique de l'École polytechnique

Talk by Christian Johansen: «Sculptures for Higher Dimensional Automata»

Speaker: Christian Johansen
Location: Room Philippe Flajolet
Date: Thu, 12 Jan 2017, 15:00-16:00

Abstract: This talk will explain Higher Dimensional Automata (HDA) model of concurrency emphasising the fact that events/activities have duration. My view of HDAs is more from a CS point of view, than geometrical, and thus I explain how transitions are now first class citizens, the same as nodes are in standard FSM. Finite state machines are the models on which standard modal logics are interpreted, i.e., in states, which contain propositional formulas, whereas the modalities move on transitions from state to state. In comparison, I will present how Higher Dimensional Modal Logic (HDML) is a natural extension of modal logic to consider the transitions as first class citizens and also to consider the concurrency. I will try to explain the attempt at proving the completeness of HDML over HDAs. Difficulty of obtaining the completeness of HDML may be because HDML is close to the ST structures, which are the natural extension of the configuration structures of van Glabbeek and Plotkin by considering the transitions as first class citizens, i.e., the notion of “during” is made explicit. My results suggest that ST structures do not capture all HDAs, but capture only Sculptures. Sculptures are strange, elusive, since they want to capture the intuition given by Pratt about how to build HDAs, but do not capture full HDAs. This brings now the discussion that maybe this is why the completeness of HDML fails. Thus, if we pin point where the sculptures sit wrt. HDAs, we may be able to understand where the completeness fails for HDML. Note that this talk will be given in a manner understandable also for non-experts in HDA or in HDML. Though some familiarity with modal logics or with event-based models of concurrency would help.