Title | ||
---|---|---|
It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before". |
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 Lamportu0027s 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. |
Year | DOI | Venue |
---|---|---|
2018 | 10.4230/LIPIcs.CONCUR.2018.7 | international conference on concurrency theory |
DocType | Volume | Citations |
Conference | abs/1804.10076 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Benedikt Bollig | 1 | 427 | 35.02 |
Marie Fortin | 2 | 0 | 0.68 |
Paul Gastin | 3 | 1165 | 75.66 |