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.
翻译:电文序列图(MSCs)自然是作为执行通信有限状态机器(CFMs)而出现的,在这种系统中,有限状态处理通过无约束的FIFO频道交换信息。我们研究了MSCs的第一阶逻辑,以Lamport以前发生的关系为特征。我们引入了一个无星版的命题动态逻辑(PDL),以循环和反调为特征。我们的主要结果显示:(一) 每一个一阶句都可以转换成等同的无星PDL句(和反之 ), (二) 每个无星PDL 句可以转换成等同的CFM。这回答了一个开放的问题,并解决了CFMs与月经第二阶逻辑碎片之间的确切关系。作为副产品,我们展示了MSCs的第一阶逻辑具有三种可变属性。