A Kleene Theorem for Higher-Dimensional Automata

Authors

Uli Fahrenberg, Christian Johansen, Georg Struth, Krzysztof Ziemiański

Where

33rd International Conference on Concurrency Theory (CONCUR 2022)

Place

Dagstuhl, Germany

Type

inproceedings

Publisher

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Projects

AA"AA" is not in the list (Vaucanson, Spot, URBI, Olena, APMC, Tiger, Climb, Speaker ID, Transformers, Bison, ...) of allowed values for the "Related project" property.

Date

2022-09-06

Abstract

We prove a Kleene theorem for higher-dimensional automata (HDAs). It states that the languages they recognise are precisely the rational subsumption-closed sets of interval pomsets. The rational operations include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce HDAs with interfaces as presheaves over labelled precube categories and use tools inspired by algebraic topology, such as cylinders and (co)fibrations. HDAs are a general model of non-interleaving concurrency, which subsumes many other models in this field. Interval orders are used as models for concurrent or distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  fahrenberg.22.concur,
  author	= {Fahrenberg, Uli and Johansen, Christian and Struth, Georg
		  and Ziemia\'{n}ski, Krzysztof},
  title		= {A {Kleene} Theorem for Higher-Dimensional Automata},
  booktitle	= {33rd International Conference on Concurrency Theory
		  (CONCUR 2022)},
  pages		= {29:1--29:18},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  isbn		= {978-3-95977-246-4},
  issn		= {1868-8969},
  year		= 2022,
  month		= sep,
  volume	= 243,
  editor	= {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher	= {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address	= {Dagstuhl, Germany},
  url		= {https://drops.dagstuhl.de/opus/volltexte/2022/17092},
  urn		= {urn:nbn:de:0030-drops-170925},
  doi		= {10.4230/LIPIcs.CONCUR.2022.29},
  abstract	= {We prove a Kleene theorem for higher-dimensional automata
		  (HDAs). It states that the languages they recognise are
		  precisely the rational subsumption-closed sets of interval
		  pomsets. The rational operations include a gluing
		  composition, for which we equip pomsets with interfaces.
		  For our proof, we introduce HDAs with interfaces as
		  presheaves over labelled precube categories and use tools
		  inspired by algebraic topology, such as cylinders and
		  (co)fibrations. HDAs are a general model of
		  non-interleaving concurrency, which subsumes many other
		  models in this field. Interval orders are used as models
		  for concurrent or distributed systems where events extend
		  in time. Our tools and techniques may therefore yield
		  templates for Kleene theorems in various models and
		  applications.}
}