Higher Dimensional Modal Logic

TL;DR

This paper introduces a decidable higher dimensional modal logic (HDML) for reasoning about concurrent systems modeled by higher dimensional automata, extending modal logic to express complex concurrency behaviors.

Contribution

It develops HDML, a new modal logic for HDAs, proves its decidability, and shows how it generalizes standard modal logic and temporal logics for traces and concurrency.

Findings

HDML is decidable and has an axiomatic system.

HDML generalizes standard modal logic when restricted to Kripke structures.

HDML captures split-bisimulation and relates to temporal logics for Mazurkiewicz traces.

Abstract

Higher dimensional automata (HDA) are a model of concurrency 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 variants of modal logic are decidable. However, there are no modal-like logics for the more expressive HDA models. In this paper we introduce and investigate a modal logic over HDAs which incorporates two modalities for reasoning about "during" and "after". We prove that this general higher dimensional modal logic (HDML) is decidable and we define an axiomatic system for it. We also show how, when the HDA model is restricted to Kripke structures, a syntactic restriction of HDML becomes the standard modal logic. Then we 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. We also study the expressiveness of the basic HDML language wrt. bisimulations and conclude that HDML captures the split-bisimulation.