2026-08-19T09:39:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9545 2024-03-06T10:44:41Z ddc:004 open_access

It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before" Bollig, Benedikt Fortin, Marie Gastin, Paul communicating finite-state machines first-order logic happened-before relation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Benedikt Bollig and Marie Fortin and Paul Gastin 2018 Is Part Of LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2018.7 urn:nbn:de:0030-drops-95455 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.7 eng https://creativecommons.org/licenses/by/3.0/legalcode