Talks & Seminars
Title: Fixpoint Logic on Data Words
Dr. Amaldev Manuel, Chennai Mathematical Institute
Date & Time: August 4, 2017 10:00
Venue: Conference Room, C Block, 01st Floor, Department of Computer Science and Engineering, Kanwal Rekhi (KReSIT) Building
Data \omega-words are infinite sequences of pairs from a set (A \times D) where A (called letters) is finite and D (called data values) is infinite. This is an expressive formalism that extends other popular abstractions like timed words, nested words etc. When seen as first-order/Kripke structures, they are \omega-words extended with a binary relation (“next occurrence of the same data value") that a is union of chains. We study the decidability and expressiveness questions of modal mu-calculus on such graphs. I will present two fragments Bounded-Reversal and Bounded-Mode-Alternation that are defined using the composition operator. We prove that BMA as well as Alternation-free BR are decidable (while the decidability of BR is open). The proof is by constructing a nondeterministic automaton for the formula (called Buchi generalised data automata) that has decidable emptiness problem. The second result is a hierarchy theorem for BMA based on composition height using techniques from Ramsey theory. These results are based on joint work with Thomas Colcombet.
Speaker Profile:
Dr. Amaldev Manuel is a Visiting Faulty at Chennai Mathematical Institute and more detail about him is available at http://www.cmi.ac.in/~amal/.
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback