Document Open Access Logo

Kamp Theorem for Pomset Languages of Higher Dimensional Automata

Authors Emily Clement , Enzo Erlich , Jérémy Ledent

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.43.pdf
  • Filesize: 1.29 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Concurrency
Keywords
  • Higher dimensional automata
  • temporal logic
  • Kamp’s theorem

Metrics

Abstract

Temporal logics are a powerful tool to specify properties of computational systems. For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages. In the case of words, Kamp’s theorem states that First Order (FO) logic is as expressive as Linear Temporal Logic (LTL). In this paper, we extend this result to pomsets. To do so, we first investigate the class of pomset languages that are definable in FO. As expected, this is a strict subclass of MSO-definable languages. Then, we define a Linear Temporal Logic for pomsets (LTL_Poms), and show that it is equivalent to FO.

Cite As Get BibTex

Emily Clement, Enzo Erlich, and Jérémy Ledent. Kamp Theorem for Pomset Languages of Higher Dimensional Automata. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 43:1-43:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.43

Author Details

Emily Clement
  • CNRS, LIPN UMR 7030, Université Sorbonne Paris Nord, F-93430 Villetaneuse, France
Enzo Erlich
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
  • EPITA Research Laboratory (LRE), Paris, France
Jérémy Ledent
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France

Funding

This work was partly supported by ANR projects BisoUS (ANR-22-CE48-0012) and PaVeDyS (ANR-23-CE48-0005).

References

  1. Amazigh Amrane, Hugo Bazille, Emily Clement, Uli Fahrenberg, and Krzysztof Ziemianski. Presenting interval pomsets with interfaces. In Uli Fahrenberg, Wesley Fussner, and Roland Glück, editors, Relational and Algebraic Methods in Computer Science - 21st International Conference, RAMiCS 2024, Prague, Czech Republic, August 19-22, 2024, Proceedings, volume 14787 of Lecture Notes in Computer Science, pages 28-45. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-68279-7_3.
  2. Amazigh Amrane, Hugo Bazille, Uli Fahrenberg, and Marie Fortin. Logic and languages of higher-dimensional automata. In Joel D. Day and Florin Manea, editors, Developments in Language Theory - 28th International Conference, DLT 2024, Göttingen, Germany, August 12-16, 2024, Proceedings, volume 14791 of Lecture Notes in Computer Science, pages 51-67. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-66159-4_5.
  3. Amazigh Amrane, Hugo Bazille, Uli Fahrenberg, and Krzysztof Ziemianski. Closure and decision properties for higher-dimensional automata. In Erika Ábrahám, Clemens Dubslaff, and Silvia Lizeth Tapia Tarifa, editors, Theoretical Aspects of Computing - ICTAC 2023 - 20th International Colloquium, Lima, Peru, December 4-8, 2023, Proceedings, volume 14446 of Lecture Notes in Computer Science, pages 295-312. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-47963-2_18.
  4. Emily Clement, Enzo Erlich, and Jérémy Ledent. Expressivity of linear temporal logic for pomset languages of higher dimensional automata. CoRR, abs/2410.12493, 2024. URL: https://doi.org/10.48550/arXiv.2410.12493.
  5. Volker Diekert and Paul Gastin. LTL is expressively complete for mazurkiewicz traces. J. Comput. Syst. Sci., 64(2):396-418, 2002. URL: https://doi.org/10.1006/jcss.2001.1817.
  6. Volker Diekert and Paul Gastin. From local to global temporal logics over mazurkiewicz traces. Theoretical Computer Science, 356(1):126-135, 2006. In honour of Professor Christian Choffrut on the occasion of his 60th birthday. URL: https://doi.org/10.1016/j.tcs.2006.01.035.
  7. Volker Diekert and Paul Gastin. Pure future local temporal logics are expressively complete for mazurkiewicz traces. Inf. Comput., 204(11):1597-1619, 2006. URL: https://doi.org/10.1016/j.ic.2006.07.002.
  8. Volker Diekert and Paul Gastin. First-order definable languages. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 261-306. Amsterdam University Press, 2008. Google Scholar
  9. Edsger W. Dijkstra. The structure of "the"-multiprogramming system. Commun. ACM, 11(5):341-346, 1968. URL: https://doi.org/10.1145/363095.363143.
  10. Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemianski. Languages of higher-dimensional automata. Math. Struct. Comput. Sci., 31(5):575-613, 2021. URL: https://doi.org/10.1017/S0960129521000293.
  11. Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemianski. A kleene theorem for higher-dimensional automata. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 29:1-29:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.29.
  12. Uli Fahrenberg and Krzysztof Ziemianski. A myhill-nerode theorem for higher-dimensional automata. In Luís Gomes and Robert Lorenz, editors, Application and Theory of Petri Nets and Concurrency - 44th International Conference, PETRI NETS 2023, Lisbon, Portugal, June 25-30, 2023, Proceedings, volume 13929 of Lecture Notes in Computer Science, pages 167-188. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-33620-1_9.
  13. Paul Gastin and Dietrich Kuske. Uniform satisfiability in PSPACE for local temporal logics over mazurkiewicz traces. Fundam. Informaticae, 80(1-3):169-197, 2007. URL: https://doi.org/10.3233/FUN-2007-801-310.
  14. Eric Goubault and Samuel Mimram. Formal relationships between geometrical and classical models for concurrency. In Lisbeth Fajstrup, Eric Goubault, and Martin Raussen, editors, Proceedings of the workshop on Geometric and Topological Methods in Computer Science, GETCO 2010, Aalborg, Denmark, January 11-15, 2010, volume 283 of Electronic Notes in Theoretical Computer Science, pages 77-109. Elsevier, 2010. URL: https://doi.org/10.1016/j.entcs.2012.05.007.
  15. André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Inf. Comput., 127(2):164-185, 1996. URL: https://doi.org/10.1006/inco.1996.0057.
  16. Johan Anthony Willem Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Computer Science Department, University of California at Los Angeles, USA, 1968. Google Scholar
  17. Leslie Lamport. On interprocess communication. part I: basic formalism. Distributed Comput., 1(2):77-85, 1986. URL: https://doi.org/10.1007/BF01786227.
  18. Antoni W. Mazurkiewicz. Trace theory. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986, volume 255 of Lecture Notes in Computer Science, pages 279-324. Springer, 1986. URL: https://doi.org/10.1007/3-540-17906-2_30.
  19. Robert McNaughton and Seymour Papert. Counter-Free Automata, volume Research Monograph, 65. The M.I.T. Press, Cambridge, Mass., 1971. Google Scholar
  20. Vaughan R. Pratt. Modeling concurrency with geometry. In David S. Wise, editor, Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, USA, January 21-23, 1991, pages 311-322. ACM Press, 1991. URL: https://doi.org/10.1145/99583.99625.
  21. Cristian Prisacariu. Modal logic over higher dimensional automata. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 494-508. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_34.
  22. Alexander Rabinovich. A proof of kamp’s theorem. Logical Methods in Computer Science, Volume 10, Issue 1:730, 2014. URL: https://doi.org/10.2168/LMCS-10(1:14)2014.
  23. Marcel Paul Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190-194, 1965. URL: https://doi.org/10.1016/S0019-9958(65)90108-7.
  24. P. S. Thiagarajan. A trace based extension of linear time temporal logic. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), Paris, France, July 4-7, 1994, pages 438-447. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/LICS.1994.316047.
  25. P.S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for mazurkiewicz traces. Information and Computation, 179(2):230-249, 2002. URL: https://doi.org/10.1006/inco.2001.2956.
  26. Rob J. van Glabbeek. On the expressiveness of higher dimensional automata. Theor. Comput. Sci., 356(3):265-290, 2006. URL: https://doi.org/10.1016/j.tcs.2006.02.012.
  27. Safa Zouari, Krzysztof Ziemianski, and Uli Fahrenberg. Bisimulations and logics for higher-dimensional automata. CoRR, abs/2402.01589, 2024. URL: https://doi.org/10.48550/arXiv.2402.01589.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact