Logical fragments for infinite and partially commutative objects

• Applicant: Professor Dr. Volker Diekert
• Subject Area: Theoretical Computer Science
• Term: from 2010 to 2020
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 166222852

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.

• DFG Programme: Research Grants