Unambiguity and Timed Languages : Automata, Logics, Expressiveness

Regular languages exhibit considerable structure. The characterization of various classes of regular languages using classical and temporal logics, automata and varieties of monoids, as an attempt towards unification of diverse frameworks, has been an important theme and area of research for many decades. In this thesis, we have investigated logic-automata connections for unambiguous languages over finite words and also timed words.

Unambiguous star-free regular languages (UL) originally introduced by Schutzenberger, have various characterizations within classical logics (FO2[<], Delta2[<]), temporal logics (TL[F,P]), using monoids (variety DA), as well as  partially ordered 2-way DFA (po2dfa). We introduce a notion of Deterministic Logics for UL with “Unique Parsability” as its key property. We show that UL is characterized by several deterministic logics with diverse modalities. 

The notion of unambiguity is extended to time to give Timed Unambiguous Languages (TUL). We give  automata as well the exact fragments of  the well known timed logics TPTL and MTL, which characterize TUL. We also study the decidability and expressiveness properties of unary fragments of MITL. 

In order to systematically study expressiveness properties of timed logics, we introduce EF games for MTL and show how these are  a useful tool in comparing expressiveness of timed logics. As a principal result, we show that, MTL[U,S] is strictly less expressive than TPTL[U,S], hence proving Alur and Henzinger's conjecture since 1990.