In quest of efficiently decidable fragments of metric temporal logic
MTL is a well known and highly expressive real time logic. Its satisfiability is undecidable in general. We will survey the long line of work seeking satisfiable fragments of MTL and present our recent results giving efficiently satisfiable fragments of MTL. These results are proved using a novel class of timed automata called partially ordered two-way deterministic timed automata (po2dfa). A refined picture of the fragments of MTL classifying these by their decision complexities and expressiveness will be presented.
Paritosh Pandya did his B.Tech in Electronics at M. S. University, Baroda, M.Tech in Computer Science at IIT Kanpur and PhD in Computer Science at TIFR. He has worked as a research officer in Oxford University Computing Laboratory under Prof C.A.R. Hoare and also as a visiting scientist at the United Nation University's International Institute of Software Technology.
Paritosh Pandya is a professor at the Tata Institute of Fundamental Research (TIFR) where he is currently the Dean of the School of Technology and Computer Science. He is also an adjunct professor in the computer science department at IIT Bombay. His research interests are in logic, formal techniques for design and analysis of programs, concurrency and embedded systems. He enjoys Indian classical music and is trying to teach the same to his computer.