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
|