Around Dot Depth Two

It is known that the languages definable by formulae of the logics FO2[<,S], 2[<,S], LTL[F,P,X,Y] are exactly the variety DAD. Automata for this class are not known, nor is its precise placement within the dot-depth hierarchy of starfree languages. It is easy to argue that 2[<,S] is included in 3[<]; in this paper we show that it is incomparable with B(2)[<], the boolean combination of 2[<] formulae. Using ideas from Straubing's "delay theorem", we extend our earlier work [LPS08] to propose partially-ordered two-way deterministic finite automata with look-around (po2dla) and a new interval temporal logic called LITL and show that they also characterize the variety DAD. We give effective reductions from LITL to equivalent po2dla and from po2dla to equivalent FO2[<,S]. The po2dla automata admit efficient operations of boolean closure and the language non-emptiness of po2dla is NP-complete. Using this, we show that satisfiability of LITL remains NP-comp...

• Type: Conference
• Year: 2010
• Where: DLT
• Authors: Kamal Lodaya, Paritosh K. Pandya, Simoni S. Shah
• Keywords: Boolean Combination, DLT 2010, Dot-depth Hierarchy, Theoretical Computer Science, Variety Dad