Document Open Access Logo

It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"

Authors Benedikt Bollig, Marie Fortin, Paul Gastin

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2018.7.pdf
  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • communicating finite-state machines
  • first-order logic
  • happened-before relation

Metrics

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

Abstract

Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. We introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.

Cite As Get BibTex

Benedikt Bollig, Marie Fortin, and Paul Gastin. It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before". In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.7

Author Details

Benedikt Bollig
  • LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, Cachan, France
Marie Fortin
  • LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, Cachan, France
Paul Gastin
  • LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, Cachan, France

Funding

Partly supported by ANR FREDDA (ANR-17-CE40-0013) and UMI RELAX.

References

  1. B. Bollig, M. Fortin, and P. Gastin. Communicating finite-state machines and two-variable logic. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018), volume 96 of Leibniz International Proceedings in Informatics, pages 17:1-17:14. Leibniz-Zentrum für Informatik, 2018. Google Scholar
  2. B. Bollig, M. Fortin, and P. Gastin. It is easy to be wise after the event: Communicating finite-state machines capture first-order logic with "happened before". CoRR, abs/1804.10076, 2018. URL: http://arxiv.org/abs/1804.10076.
  3. B. Bollig, D. Kuske, and I. Meinecke. Propositional dynamic logic for message-passing systems. Logical Methods in Computer Science, 6(3:16), 2010. Google Scholar
  4. B. Bollig and M. Leucker. Message-passing automata are expressively equivalent to EMSO logic. Theoretical Computer Science, 358(2-3):150-172, 2006. Google Scholar
  5. D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2), 1983. Google Scholar
  6. J. Büchi. Weak second order logic and finite automata. Z. Math. Logik, Grundlag. Math., 5:66-62, 1960. Google Scholar
  7. G. De Giacomo and M. Lenzerini. Boosting the correspondence between description logics and propositional dynamic logics. In Proceedings of the 12th National Conference on Artificial Intelligence, Seattle, WA, USA, July 31 - August 4, 1994, Volume 1., pages 205-212. AAAI Press / The MIT Press, 1994. Google Scholar
  8. V. Diekert and P. 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
  9. V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995. Google Scholar
  10. C. C. Elgot. Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98:21-52, 1961. Google Scholar
  11. M. J. Fischer and R. E. Ladner. Propositional Dynamic Logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979. Google Scholar
  12. D. M. Gabbay. Expressive functional completeness in tense logic. In Uwe Mönnich, editor, Aspects of Philosophical Logic: Some Logical Forays into Central Notions of Linguistics and Philosophy, pages 91-117. Springer Netherlands, Dordrecht, 1981. Google Scholar
  13. D. M. Gabbay, I. Hodkinson, and M. A. Reynolds. Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Oxford University Press, 1994. Google Scholar
  14. B. Genest, D. Kuske, and A. Muscholl. A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Information and Computation, 204(6):920-956, 2006. Google Scholar
  15. B. Genest, D. Kuske, and A. Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae, 80(1-3):147-167, 2007. Google Scholar
  16. S. Göller, M. Lohrey, and C. Lutz. PDL with intersection and converse: satisfiability and infinite-state model checking. Journal of Symbolic Logic, 74(1):279-314, 2009. Google Scholar
  17. E. Grädel and M. Otto. On logics with two variables. Theoretical Computer Science, 224(1-2):73-113, 1999. Google Scholar
  18. J. Y. Halpern and Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. Artif. Intell., 54(2):319-379, 1992. Google Scholar
  19. W. Hanf. Model-theoretic methods in the study of elementary logic. In J. W. Addison, L. Henkin, and A. Tarski, editors, The Theory of Models. North-Holland, Amsterdam, 1965. Google Scholar
  20. J. G. Henriksen, M. Mukund, K. Narayan Kumar, M. Sohoni, and P. S. Thiagarajan. A theory of regular MSC languages. Information and Computation, 202(1):1-38, 2005. Google Scholar
  21. H. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, 1968. Google Scholar
  22. D. Kuske. Regular sets of infinite message sequence charts. Information and Computation, 187:80-109, 2003. Google Scholar
  23. L. Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, 1978. Google Scholar
  24. M. Lange. Model checking propositional dynamic logic with all extras. Journal of Applied Logic, 4(1):39-49, 2006. Google Scholar
  25. M. Lange and C. Lutz. 2-ExpTime lower bounds for Propositional Dynamic Logics with intersection. Journal of Symbolic Logic, 70(5):1072-1086, 2005. Google Scholar
  26. M. Lohrey and A. Muscholl. Bounded MSC Communication. Information and Computation, 189(2):160-181, 2004. Google Scholar
  27. R. Mennicke. Propositional dynamic logic with converse and repeat for message-passing systems. Logical Methods in Computer Science, 9(2:12):1-35, 2013. Google Scholar
  28. L. J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, MIT, 1974. Google Scholar
  29. R. S. Streett. Propositional dynamic logic of looping and converse. In Proceedings of STOC'81, pages 375-383. ACM, 1981. Google Scholar
  30. P. S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for Mazurkiewicz traces. Inf. Comput., 179(2):230-249, 2002. Google Scholar
  31. W. Thomas. Languages, automata and logic. In A. Salomaa and G. Rozenberg, editors, Handbook of Formal Languages, volume 3, pages 389-455. Springer, 1997. Google Scholar
  32. B. A. Trakhtenbrot. Finite automata and monadic second order logic. Siberian Math. J, 3:103-131, 1962. In Russian; English translation in Amer. Math. Soc. Transl. 59, 1966, 23-55. Google Scholar
  33. W. Zielonka. Notes on finite asynchronous automata. R.A.I.R.O. - Informatique Théorique et Applications, 21:99-135, 1987. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact