Modal Logic over Higher Dimensional Automata – technicalities

Higher dimensional automata (HDA) are a model of concurrency [5, 8] that can express most of the traditional partial order models like Mazurkiewicz traces, pomsets, event structures, or Petri nets. Modal logics, interpreted over Kripke structures, are the logics for reasoning about sequential behavior and interleaved concurrency. Modal logic is a well behaved subset of first-order logic; many vari-ants of modal logic are decidable. However, there are no modal-like logics for the more expressive HDA models. We introduce and develop a modal logic over HDAs which incorporates two modalities for reasoning about “during ” and “af-ter”. This general higher dimensional modal logic (HDML) is shown to be de-cidable and we provide a complete axiomatic system for it. With higher dimensional automata concurrent systems can be modeled at different levels of abstraction, not only as all possible interleavings of their con-current actions. HDAs can model concurrent systems at any granularity level and make no assumptions about the durations of the actions. Moreover, HDAs are not constrained to only before-after modeling, but represent also the “during”