Abstract:

Many autonomous (or highly automated) systems are also safety critical. Due to their safety critical nature, they must adhere to well defined requirements typically in pairs of assumptions and guarantees. An ongoing research challenge is to develop a specification formalism to rule them all. That is, the formalism has to be expressive enough to capture all requirements of interest while at the same time it has to be computationally efficient in order to be used in automated analysis and design. Temporal logics have proven to be an excellent choice when considering their expressive power and computational efficiency. In this talk, we will review the theory of robustness of temporal logics as applied to Cyber-Physical Systems (CPS). We will highlight the connections between synthesis and analysis methods with respect to temporal logic requirements and their robust interpretation. In addition, we will show how some verification and specification mining problems can be translated into optimization problems using the notion of robustness. In terms of applications, we will demonstrate how temporal logic requirements can help us in automated testing of autonomous vehicles and perception systems, and in the planning and coordination of groups of vehicles under different access right levels.

Bio:

Georgios Fainekos is an Associate Professor at the School of Computing, Informatics and Decision Systems Engineering (SCIDSE) at Arizona State University (ASU). He is director of the Cyber-Physical Systems (CPS) Lab and he is currently affiliated with the NSF I/UCR Center for Embedded Systems (CES) and the Robotics Faculty Group at ASU. He received his Ph.D. in Computer and Information Science from the University of Pennsylvania in 2008 where he was affiliated with the GRASP laboratory. He holds a Diploma degree (B.Sc. & M.Sc.) in Mechanical Engineering from the National Technical University of Athens (NTUA). Before joining ASU, he held a Postdoctoral Researcher position at NEC Laboratories America in the System Analysis & Verification Group. His technical expertise is on applied logic, formal verification, testing, control theory, artificial intelligence, and optimization. His research has applications to automotive systems, medical devices, autonomous (ground and aerial) vehicles, and human-robot interaction (HRI). In 2013, Dr. Fainekos received the NSF CAREER award and the ASU SCIDSE Best Researcher Junior Faculty Award. He is also recipient of the 2008 Frank Anger Memorial ACM SIGBED/SIGSOFT Student Award. His software toolbox, S-TaLiRo, for testing and monitoring of CPS has been nominated twice as a technological breakthrough by the industry. In 2016, Dr. Fainekos was the program co-Chair for the ACM International Conference on Hybrid Systems: Computation and Control (HSCC).