Logical fragments for infinite and partially commutative objects

在这个项目中，我们想要得到一阶逻辑的新的可判决性结果。我们考虑的模型有有限词、无限词和Marzurkiewicz轨迹。后者很有趣，因为这些部分交换的结构可以建模并发系统。该项目涉及基金会。这些结果的动机来自于实际的考虑，比如电路和软件的验证。在这种情况下，逻辑片段之所以有趣，有两个原因。首先，它们允许对某些给定属性的难度进行估计，其次，更容易的片段允许更有效的算法（例如用于模型检查问题）。直观地说，如果某些属性只能在一些更具表现力的片段中表达，那么它就会变得更加困难。我们使用的方法结合了代数、拓扑和组合思想。

In this project we want to obtain new decidability results for first-order logic. The models we consider are finite words, infinite words, and Marzurkiewicz traces. The latter are interesting since these partially commutative structures can model concurrent systems. The project concerns foundations. The motivation for such results comes from practical considerations such as the validations of circuits and software. In this context, logical fragments are interesting for two reasons. First, they admit the estimation of the difficulty of some given property, and second easier fragments allow for more efficient algorithms (e.g. for the model checking problem). Intuitively, some property is more difficult if it can only be expressed in some more expressive fragment. The methods we use combine algebraic, topological and combinatorial ideas.