Hybrid automata are a natural and expressive formalism to model systems that exhibit both discrete and continuous behavior. However, the applications of hybrid automata in analyzing cyber-physical systems have been rather limited due to undecidability of simple verification problems such as reachability. This drawback of hybrid automata has fueled the investigation of the so-called compositional methodology to design complex system by sequentially composing well-understood lower-level components. This methodology has, for example, been used in the context of the motion planning problem for mobile robots, where the task is to move a robot along a pre-specified trajectory with arbitrary precision by sequentially composing a set of well-studied simple motion primitives, such as "move left," "move right" and "go straight." In this talk, Trivedi will summarize some of his recent results related to efficient solution of motion planning problem for systems whose motion p!
rimitives are given as constant-rate vectors with uncertainties.
Ashutosh Trivedi received his PhD from the University of Warwick for studying competitive optimization on Timed Automata in 2009. After this he worked on verification and synthesis of stochastic real-time systems at the University of Oxford in the group of Marta Kwiatkowska. In 2010 he joined the University of Pennsylvania as a postdoctoral researcher with Rajeev Alur to study formal methods for verification of cyber-physical systems. For the last three years he has been working as an assistant professor in the CSE department at IIT Bombay. His research focuses on developing theory, techniques, and tools for formal analysis, verification, and synthesis for hybrid systems.