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. Our main result states that every first-order sentence can be transformed 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 obtain self-contained normal-form constructions for first-order logic over MSCs (and, therefore, over words). In particular, we show that first-order logic has the three-variable property.
翻译:电文序列图(MSCs)自然是作为执行通信有限状态机器(CFMs)而生成的,在这种机器中,有限状态处理通过无约束的FIFO渠道交换信息。我们研究了MSCs的第一阶逻辑,以Lamport以前发生的关系为特征。我们的主要结果表明,每一阶次的句子都可以转换为等效的CFM。这回答了一个未决问题,解决了CFMs和Monadic第二阶次逻辑的碎片之间的确切关系。作为一个副产品,我们获得了自成一体的正常形式结构结构,以适应MSCs的第一阶次的逻辑(因此也超越了文字 ) 。 特别是,我们显示了一阶逻辑具有三种可变财产。