Logical fragments for infinite and partially commutative objects

点击翻译按钮获取中文摘要

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.