- A-212 (STCS Seminar Room)
The class of Unambiguous Star-free regular languages over words has been variously characterized in the past by logics such as the fragments $\Delta_2[<]$ and $FO^2[<]$ of first-order definable languages, Unary Temporal Logic $TL[F,P]$ as well as the logic $TL[X_a,Y_a]$ of rankers and Unambiguous Interval Temporal Logic (UITL). The class of partially- ordered 2-way DFA (po2DFA) also characterize this class and so do the variety DA of monoids.
The prominent logical characterizations of UL have primarily been non-deterministic, such as the logics $\Delta_2[<] , FO^2[<]$ and $TL[F,P]$. While these logics are expressively equivalent to po2DFA, no explicit reductions from these logics to po2DFA were known. Neither the complexities of the formula automaton construction nor the bounds on the size of equivalent automata were worked out. We bridge this gap and give an effective language preserving translation from the non-deterministic logic $TL[F,P]$ to the deterministic logic $TL[X_a,Y_a]$. This completes the missing link in effective reduction from logics $TL[F,P]$ and $FO^2[<]$ for UL to their language equivalent po2DFA automata. Moreover, the reduction also gives us an alternate proof for NP-complete satisfiability for $TL[F,P]$ formulas.