Document Open Access Logo

Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages

Authors Bharat Adsul , Paul Gastin , Saptarshi Sarkar , Pascal Weil

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.28.pdf
  • Filesize: 0.75 MB
  • 19 pages

Document Identifiers

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
Saptarshi Sarkar
  • IIT Bombay, Mumbai, India
Pascal Weil
  • CNRS, ReLaX, IRL 2000, Siruseri, India
  • Univ. Bordeaux, LaBRI, CNRS UMR 5800, F-33400 Talence, France

Cite AsGet BibTex

Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.28

Abstract

One of the main motivations for this work is to obtain a distributed Krohn-Rhodes theorem for Mazurkiewicz traces. Concretely, we focus on the recently introduced operation of local cascade product of asynchronous automata and ask if every regular trace language can be accepted by a local cascade product of "simple" asynchronous automata. Our approach crucially relies on the development of a local and past-oriented propositional dynamic logic (LocPastPDL) over traces which is shown to be expressively complete with respect to all regular trace languages. An event-formula of LocPastPDL allows to reason about the causal past of an event and a path-formula of LocPastPDL, localized at a process, allows to march along the sequence of past-events in which that process participates, checking for local regular patterns interspersed with local tests of other event-formulas. We also use additional constant formulas to compare the leading process events from the causal past. The new logic LocPastPDL is of independent interest, and the proof of its expressive completeness is rather subtle. Finally, we provide a translation of LocPastPDL formulas into local cascade products. More precisely, we show that every LocPastPDL formula can be computed by a restricted local cascade product of the gossip automaton and localized 2-state asynchronous reset automata and localized asynchronous permutation automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Algebraic language theory
Keywords
  • Mazurkiewicz traces
  • propositional dynamic logic
  • regular trace languages
  • asynchronous automata
  • cascade product
  • Krohn Rhodes theorem

Metrics

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

References

  1. 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. Google Scholar
  2. Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Asynchronous wreath product and cascade decompositions for concurrent behaviours. Log. Methods Comput. Sci., 18, 2022. Google Scholar
  3. Bharat Adsul and Milind A. Sohoni. Local normal forms for logics over traces. In Manindra Agrawal and Anil Seth, editors, FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 22nd Conference Kanpur, India, December 12-14, 2002, Proceedings, volume 2556 of Lecture Notes in Computer Science, pages 47-58. Springer, 2002. Google Scholar
  4. Benedikt Bollig, Marie Fortin, and Paul Gastin. Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic. J. Comput. Syst. Sci., 115:22-53, 2021. URL: https://doi.org/10.1016/j.jcss.2020.06.006.
  5. Benedikt Bollig and Paul Gastin. Non-sequential theory of distributed systems. CoRR, abs/1904.06942, 2019. URL: http://arxiv.org/abs/1904.06942.
  6. Benedikt Bollig, Dietrich Kuske, and Ingmar Meinecke. Propositional dynamic logic for message-passing systems. Log. Methods Comput. Sci., 6(3), 2010. URL: http://arxiv.org/abs/1007.4764.
  7. Giuseppe De Giacomo and Moshe Y Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Twenty-Third International Joint Conference on Artificial Intelligence, 2013. Google Scholar
  8. Volker Diekert and Paul Gastin. LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences, 64(2):396-418, March 2002. Google Scholar
  9. 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. Google Scholar
  10. 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, volume 2 of Texts in Logic and Games, pages 261-306. Amsterdam University Press, 2008. Google Scholar
  11. Volker Diekert and Grzegorz Rozenberg, editors. The Book of Traces. World Scientific, 1995. URL: https://doi.org/10.1142/2563.
  12. Werner Ebinger and Anca Muscholl. Logical definability on infinite traces. Theor. Comput. Sci., 154(1):67-84, 1996. Google Scholar
  13. Michael J Fischer and Richard E Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979. Google Scholar
  14. Stefan Göller, Markus Lohrey, and Carsten Lutz. PDL with intersection and converse: satisfiability and infinite-state model checking. J. Symb. Log., 74(1):279-314, 2009. URL: https://doi.org/10.2178/jsl/1231082313.
  15. Giovanna Guaiana, Antonio Restivo, and Sergio Salemi. Star-free trace languages. Theor. Comput. Sci., 97(2):301-311, 1992. Google Scholar
  16. Kenneth Krohn and John Rhodes. Algebraic theory of machines I. Prime decomposition theorem for finite semigroups and machines. Transactions of The American Mathematical Society, 116, April 1965. URL: https://doi.org/10.2307/1994127.
  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. Google Scholar
  18. Roy Mennicke. Propositional dynamic logic with converse and repeat for message-passing systems. Log. Methods Comput. Sci., 9(2), 2013. URL: https://doi.org/10.2168/LMCS-9(2:12)2013.
  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. Howard Straubing. Finite automata, formal logic, and circuit complexity. Birkhaüser Verlag, Basel, Switzerland, 1994. Google Scholar
  21. P.S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for Mazurkiewicz traces. Information and Computation, 179(2):230-249, December 2002. 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. Nicolas Troquard and Philippe Balbiani. Propositional Dynamic Logic. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Spring 2019 edition, 2019. URL: https://plato.stanford.edu/archives/spr2019/entries/logic-dynamic/.
  24. Wieslaw Zielonka. Notes on finite asynchronous automata. RAIRO Theor. Informatics Appl., 21(2):99-135, 1987. URL: https://doi.org/10.1051/ita/1987210200991.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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