Document Open Access Logo

Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces

Authors Bharat Adsul , Paul Gastin , Shantanu Kulkarni

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.5.pdf
  • Filesize: 1.07 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.CONCUR.2025.5.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Distributed computing models
  • Theory of computation → Algebraic language theory
  • Security and privacy → Logic and verification
Keywords
  • Mazurkiewicz traces
  • temporal logics
  • asynchronous automata
  • cascade product
  • Green’s relations
  • algebraic automata theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We study fragments of temporal logics over Mazurkiewicz traces which are well known and established partial-order models of concurrent behaviours. We focus on concurrent versions of "strict past" and "strict future" modalities. Over words, the corresponding fragments have been shown to coincide with natural algebraic conditions on the recognizing monoids. We provide non-trivial generalizations of these classical results to traces. We exploit the local nature of the temporal modalities and obtain modular translations of specifications into asynchronous automata. More specifically, we provide novel characterizations of these fragments via local cascade products of a very simple two-state asynchronous automaton operating on a single process.

Cite As Get BibTex

Bharat Adsul, Paul Gastin, and Shantanu Kulkarni. Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.5

Author Details

Bharat Adsul
  • IIT Bombay, Mumbai, India
Paul Gastin
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, 91190, Gif-sur-Yvette, France
  • CNRS, ReLaX, IRL 2000, Siruseri, India
Shantanu Kulkarni
  • IIT Bombay, Mumbai, India

References

  1. Bharat Adsul, Paul Gastin, Shantanu Kulkarni, and Pascal Weil. An expressively complete local past propositional dynamic logic over Mazurkiewicz traces and its applications. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'24, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3661814.3662110.
  2. Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Wreath/cascade products and related decomposition results for the concurrent setting of Mazurkiewicz traces. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 19:1-19:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPICS.CONCUR.2020.19.
  3. Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Asynchronous wreath product and cascade decompositions for concurrent behaviours. Log. Methods Comput. Sci., 18, 2022. URL: https://doi.org/10.46298/LMCS-18(2:22)2022.
  4. Bharat Adsul and Milind A. Sohoni. Asynchronous automata-theoretic characterization of aperiodic trace languages. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 84-96. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_8.
  5. Mikołaj Bojańczyk. Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic, 2020. URL: https://arxiv.org/abs/2008.11635.
  6. J.A. Brzozowski and Faith E. Fich. Languages of R-trivial monoids. Journal of Computer and System Sciences, 20(1):32-49, 1980. URL: https://doi.org/10.1016/0022-0000(80)90003-3.
  7. Joëlle Cohen, Dominique Perrin, and Jean-Eric Pin. On the expressive power of temporal logic. Journal of Computer and System Sciences, 46(3):271-294, 1993. URL: https://doi.org/10.1016/0022-0000(93)90005-H.
  8. Volker Diekert and Paul Gastin. Pure future local temporal logics are expressively complete for Mazurkiewicz traces. Information and Computation, 204(11):1597-1619, November 2006. URL: https://doi.org/10.1016/J.IC.2006.07.002.
  9. Volker Diekert, Paul Gastin, and Manfred Kufleitner. A survey on small fragments of first-order logic over finite words. Int. J. Found. Comput. Sci., 19(3):513-548, 2008. URL: https://doi.org/10.1142/S0129054108005802.
  10. Volker Diekert, Martin Horsch, and Manfred Kufleitner. On first-order fragments for Mazurkiewicz traces. Fundamenta Informaticae, 80(1-3):1-29, 2007. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-02.
  11. Volker Diekert and Manfred Kufleitner. On first-order fragments for words and Mazurkiewicz traces: a survey. In Proceedings of the 11th international conference on Developments in language theory, pages 1-19, 2007. Google Scholar
  12. Volker Diekert and Grzegorz Rozenberg, editors. The Book of Traces. World Scientific, 1995. URL: https://doi.org/10.1142/2563.
  13. Werner Ebinger and Anca Muscholl. Logical definability on infinite traces. Theor. Comput. Sci., 154(1):67-84, 1996. URL: https://doi.org/10.1016/0304-3975(95)00130-1.
  14. Kousha Etessami and Thomas Wilke. An until hierarchy and other applications of an Ehrenfeucht-Fraïsse game for temporal logic. Information and Computation, 160(1):88-108, 2000. URL: https://doi.org/10.1006/inco.1999.2846.
  15. Giovanna Guaiana, Antonio Restivo, and Sergio Salemi. On aperiodic trace languages. In Christian Choffrut and Matthias Jantzen, editors, STACS 91, 8th Annual Symposium on Theoretical Aspects of Computer Science, Hamburg, Germany, February 14-16, 1991, Proceedings, volume 480 of Lecture Notes in Computer Science, pages 76-88. Springer, 1991. URL: https://doi.org/10.1007/BFB0020789.
  16. Johan Anthony Willem Kamp. Tense Logic and the Theory of Linear Order. University of California, Los Angeles, CA, USA, 1968. Google Scholar
  17. Manfred Kufleitner. Polynomials, fragments of temporal logic and the variety DA over traces. Theoretical Computer Science, 376:89-100, 2007. Special issue DLT 2006. URL: https://doi.org/10.1016/J.TCS.2007.01.014.
  18. Robert McNaughton and Seymour A Papert. Counter-Free Automata (MIT research monograph no. 65). The MIT Press, 1971. Google Scholar
  19. Madhavan Mukund and Milind A. Sohoni. Keeping track of the latest gossip in a distributed system. Distributed Comput., 10(3):137-148, 1997. URL: https://doi.org/10.1007/s004460050031.
  20. M.P. 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.
  21. Howard Straubing. Finite automata, formal logic, and circuit complexity. Birkhaüser Verlag, Basel, Switzerland, 1994. Google Scholar
  22. Wolfgang Thomas. On logical definability of trace languages. In V. Diekert, editor, Proceedings of a workshop of the ESPRIT Basic Research Action No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS), Kochel am See, Bavaria, FRG (1989), Report TUM-I9002, Technical University of Munich, pages 172-182, 1990. Google Scholar
  23. Wieslaw Zielonka. Notes on finite asynchronous automata. RAIRO Theor. Informatics Appl., 21(2):99-135, 1987. URL: https://doi.org/10.1051/ita/1987210200991.
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