A data word is a finite word in which each position carries a label from a finite alphabet and a data value from an infinite domain. It is well-known that satisfiability of two-variable first-order logic with the data value equality test on data words is decidable while three variables leads to undecidability. In this talk, we present a decidable extension of the two-variable logic by adding guarded regular binary predicates of the form L(x,y) that is satisfied by positions x and y if they carry the same data value and the factor strictly between x and y is in the regular language L. We characterise the class of monoids recognising the regular predicates for which the resulting extension of the two-variable logic is decidable. Our proof is automata-theoretic – we translate formulas to a new automaton formalism called ordered quasi-normal set automaton that has a decidable emptiness problem by reduction to ordered multicounter automata. We obtain decidability for the logic with guarded regular predicates recognised by a monoid if and only if the monoid is idempotent and its two-sided ideals are linearly ordered. 

Bio: Rishal S P is a researcher at Sarva Labs. He is interested in theoretical computer science, especially in automata theory, logic, and verification. He completed his undergraduate studies in mathematics at Shiv Nadar University, Delhi-NCR in 2024 and has been an intern at IIT Goa under Amaldev Manuel where he was working on automata and logics on data words.