Akshay Rajhans:
Verification of Systems Using Robust Temporal Logic TestingRobustness of Temporal Logic Specifications for Testing of Signals

Abstract: The notion of robustness of the temporal logic testing for signals was developed in part I of this talk series. Trajectories of systems can be thought of as signals. A system satisfies a temporal logic (TL) specification if ALL of its trajectories satisfy it. This means that (in principle) we should be able to run a robust test on EACH trajectory of such a system in order to talk about satisfaction of a specification by the system. However, the number of trajectories for even a small bounded region of initial conditions is infinite in the case of continuous systems.

In this talk we will see how the notion of approximate bisimulation allows us to reason about the behavior of a neighborhood of trajectories (in turn, about a neighborhood of initial conditions) by running just one robust test. What this facilitates is the ability to verify the satisfaction of a specification by a system using only a FINITE number of its (numerically simulated) trajectories. To facilitate this discussion, we will briefly review approximate bisimulation relations and see how bisimulation functions help us do this in practice. Next, we will see the temporal logic verification algorithm proposed by the thesis.

In closing, we will briefly mention other contributions of the thesis and some related research work that are not central to this two-presentation series.

NOTE: This two-part presentation series titled "Robustness of temporal logic specifications" looks at some interesting contributions of the recently defended PhD thesis by Dr. Georgios Fainekos at the University of Pennsylvania. Part I of this talk was presented 20 August 2008.
Akshay Rajhans is a PhD student in the Electrical and Computer Engineering department at Carnegie Mellon University. He received his Bachelor of Engineering degree in Electronics and Telecommunication from the University of Pune in 2003. From 2003 to 2005 he was working with the Research Development and Engineering department of Cummins India Limited, where he most recently served as a Manager of Electronic Controls. In January 2006 he joined the University of Pennsylvania, where he received his Master of Science degree in Electrical Engineering in December 2008. From January 2008 through June 2008, he was a temporary research staff under Prof. George Pappas at the General Robotics Automation Sensing and Perception (GRASP) Laboratory of the University of Pennsylvania. From July 2008 he is a PhD student at the Electrical and Computer Engineering department at Carnegie Mellon University.

Appointments: dcm@cs.cmu.edu

Maintainer Home > Seminar ]
`Last modified: Wed Aug 20 11:09:10 EDT 2008