It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"
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.
communicating finite-state machines
first-order logic
happened-before relation
Theory of computation~Logic and verification
7:1-7:17
Regular Paper
Partly supported by ANR FREDDA (ANR-17-CE40-0013) and UMI RELAX.
https://arxiv.org/abs/1804.10076
Benedikt
Bollig
Benedikt Bollig
LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, Cachan, France
Marie
Fortin
Marie Fortin
LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, Cachan, France
Paul
Gastin
Paul Gastin
LSV, CNRS & ENS Paris-Saclay, Université Paris-Saclay, Cachan, France
10.4230/LIPIcs.CONCUR.2018.7
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.
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.
http://arxiv.org/abs/1804.10076
B. Bollig, D. Kuske, and I. Meinecke. Propositional dynamic logic for message-passing systems. Logical Methods in Computer Science, 6(3:16), 2010.
B. Bollig and M. Leucker. Message-passing automata are expressively equivalent to EMSO logic. Theoretical Computer Science, 358(2-3):150-172, 2006.
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2), 1983.
J. Büchi. Weak second order logic and finite automata. Z. Math. Logik, Grundlag. Math., 5:66-62, 1960.
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.
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.
V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.
C. C. Elgot. Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98:21-52, 1961.
M. J. Fischer and R. E. Ladner. Propositional Dynamic Logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979.
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.
D. M. Gabbay, I. Hodkinson, and M. A. Reynolds. Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Oxford University Press, 1994.
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.
B. Genest, D. Kuske, and A. Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae, 80(1-3):147-167, 2007.
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.
E. Grädel and M. Otto. On logics with two variables. Theoretical Computer Science, 224(1-2):73-113, 1999.
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.
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.
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.
H. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, 1968.
D. Kuske. Regular sets of infinite message sequence charts. Information and Computation, 187:80-109, 2003.
L. Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, 1978.
M. Lange. Model checking propositional dynamic logic with all extras. Journal of Applied Logic, 4(1):39-49, 2006.
M. Lange and C. Lutz. 2-ExpTime lower bounds for Propositional Dynamic Logics with intersection. Journal of Symbolic Logic, 70(5):1072-1086, 2005.
M. Lohrey and A. Muscholl. Bounded MSC Communication. Information and Computation, 189(2):160-181, 2004.
R. Mennicke. Propositional dynamic logic with converse and repeat for message-passing systems. Logical Methods in Computer Science, 9(2:12):1-35, 2013.
L. J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, MIT, 1974.
R. S. Streett. Propositional dynamic logic of looping and converse. In Proceedings of STOC'81, pages 375-383. ACM, 1981.
P. S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for Mazurkiewicz traces. Inf. Comput., 179(2):230-249, 2002.
W. Thomas. Languages, automata and logic. In A. Salomaa and G. Rozenberg, editors, Handbook of Formal Languages, volume 3, pages 389-455. Springer, 1997.
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.
W. Zielonka. Notes on finite asynchronous automata. R.A.I.R.O. - Informatique Théorique et Applications, 21:99-135, 1987.
Benedikt Bollig, Marie Fortin, and Paul Gastin
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode