2010 | OriginalPaper | Chapter
Modal Logic over Higher Dimensional Automata
Author : Cristian Prisacariu
Published in: CONCUR 2010 - Concurrency Theory
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Higher dimensional automata (
$\mathit{HDAs}$
) 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
$\mathit{HDA}$
models. In this paper we introduce and investigate a modal logic over
$\mathit{HDAs}$
which incorporates two modalities for reasoning about “during” and “after”. We prove that this general higher dimensional modal logic (
$\mathit{HDML}$
) is decidable and we define a complete axiomatic system for it. We also show how, when the
$\mathit{HDA}$
model is restricted to Kripke structures, a syntactic restriction of
$\mathit{HDML}$
becomes the standard modal logic. Then we isolate the class of
$\mathit{HDAs}$
that encode Mazurkiewicz traces and show how
$\mathit{HDML}$
can be restricted to LTrL (the linear time temporal logic over Mazurkiewicz traces).