Logics and Automata for Classical and Real Time Unambiguous Languages

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 investigate 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). In this thesis, we introduce a notion of Deterministic Logics for UL with “Unique Parsability” as its key property. We show that UL is robustly 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.