| Description |
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.
|