Document Open Access Logo

Communicating Finite-State Machines and Two-Variable Logic

Authors Benedikt Bollig, Marie Fortin, Paul Gastin

PDF
Thumbnail PDF

File

LIPIcs.STACS.2018.17.pdf
  • Filesize: 0.62 MB
  • 14 pages

Document Identifiers

Author Details

Benedikt Bollig
Marie Fortin
Paul Gastin

Cite AsGet BibTex

Benedikt Bollig, Marie Fortin, and Paul Gastin. Communicating Finite-State Machines and Two-Variable Logic. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.STACS.2018.17

Abstract

Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they are expressively equivalent to existential MSO logic with two first-order variables and the order relation.
Keywords
  • communicating finite-state machines
  • MSO logic
  • message sequence charts

Metrics

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

References

  1. R. Alur and P. Madhusudan. Adding nesting structure to words. Journal of the ACM, 56(3):1-43, 2009. Google Scholar
  2. N. Bedon. Logic and branching automata. Logical Methods in Computer Science, 11(4), 2015. Google Scholar
  3. H. Björklund and T. Schwentick. On notions of regularity for data languages. Theoretical Computer Science, 411(4-5):702-715, 2010. Google Scholar
  4. M. Bojanczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data words. ACM Transactions on Computational Logic, 12(4):27, 2011. Google Scholar
  5. 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
  6. 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
  7. D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2), 1983. Google Scholar
  8. J. Büchi. Weak second order logic and finite automata. Z. Math. Logik, Grundlag. Math., 5:66-62, 1960. Google Scholar
  9. C. C. Elgot. Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98:21-52, 1961. Google Scholar
  10. 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
  11. 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
  12. B. Genest, D. Kuske, and A. Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae, 80(1-3):147-167, 2007. Google Scholar
  13. E. Grädel and M. Otto. On logics with two variables. Theor. Comput. Sci., 224(1-2):73-113, 1999. Google Scholar
  14. M. Grohe and N. Schweikardt. Comparing the succinctness of monadic query languages over finite trees. In Proceedings of CSL'03, volume 2803 of Lecture Notes in Computer Science, pages 226-240. Springer, 2003. Google Scholar
  15. 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
  16. Lauri Hella, Matti Järvisalo, Antti Kuusisto, Juhana Laurinharju, Tuomo Lempiäinen, Kerkko Luosto, Jukka Suomela, and Jonni Virtema. Weak models of distributed computing, with connections to modal logic. Distributed Computing, 28(1):31-53, 2015. URL: http://dx.doi.org/10.1007/s00446-013-0202-3.
  17. 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
  18. D. Kuske. Infinite series-parallel posets: Logic and languages. In Proceedings of ICALP'00, volume 1853 of LNCS, pages 648-662. Springer, 2000. Google Scholar
  19. D. Kuske. Regular sets of infinite message sequence charts. Information and Computation, 187:80-109, 2003. Google Scholar
  20. Antti Kuusisto. Modal logic and distributed message passing automata. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 452-468. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.452.
  21. Fabian Reiter. Distributed graph automata. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 192-201. IEEE Computer Society, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.27.
  22. Fabian Reiter. Asynchronous distributed automata: A characterization of the modal mu-fragment. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 100:1-100:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2017.100.
  23. J. W. Thatcher and J. B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1):57-81, 1968. Google Scholar
  24. W. Thomas. On logical definability of trace languages. In Proceedings of Algebraic and Syntactic Methods in Computer Science (ASMICS), Report TUM-I9002, Technical University of Munich, pages 172-182, 1990. Google Scholar
  25. W. Thomas. Elements of an automata theory over partial orders. In Proceedings of POMIV'96, volume 29 of DIMACS. AMS, 1996. Google Scholar
  26. 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
  27. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of LICS'86, pages 332-344. IEEE Computer Society, 1986. Google Scholar
  28. P. Weis. Expressiveness and Succinctness of First-order Logic on Finite Words. Ph.D. thesis, University of Massachusetts Amherst, 2011. Google Scholar
  29. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact