FUNDING

My funding supports research in a number of topics listed under Current Research Topics. Further details can be found in my CV.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

Current Funding

• NSF: Model Exploration for Cyber-Physical Systems
• NSF: Statistical Techniques for Verifying Temporal Properties of Embedded and Mixed-Signal Systems
• CES: Statistical Techniques for Property Exploration of Cyber-Physical Systems
• CES: Robust Testing for Networked Control Systems and Mixed-Signal Systems

SOFTWARE TOOLS

S-TaLiRo Tool Suite [Get tools]

A suit of tools for the analysis of continuous and hybrid dynamical systems using linear time temporal logics. S-TaLiRo (Systems TaLiRo) is a software toolbox for Matlab for the temporal logic falsification of Hybrid Automata and Matlab/Simulink models. TaLiRo is a software toolbox for Matlab for the temporal logic robustness analysis of discrete time signals that take values in metric spaces.

TaLiRo v0.1 [Get tool]

TaLiRo computes the robustness estimate of a temporal logic specification (LTL or MTL) over a finite timed state sequence.

CURRENT RESEARCH TOPICS

Robustness of Temporal Logics

This project studies the robust interpretation of Metric Temporal Logic (MTL) (and, hence, Linear Temporal Logic (LTL)) formulas over signals that take values in metric spaces. For such signals, which are generated by systems whose states are equipped with nontrivial metrics, for example continuous or hybrid, robustness is not only natural, but also a critical measure of system performance. Thus, we propose multi-valued semantics for MTL formulas, which capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance e from unsatisfiability. Any other signal that remains e-close to the initial one also satisfies the same MTL specification under the usual Boolean semantics. The new robust semantics can find several applications on diverse problems such as (i) robust and/or statistical testing of hybrid systems and (ii) computation of satisfiability and estimation of robustness for real-time formulas with continuous time semantics using discrete time reasoning on the sampled signal.

Robust Testing and Verification for Hybrid Systems

Temporal logics have been proven to be an extremely useful formalism for the property based verification or testing of software and hardware systems. Several critical bugs in protocols and designs have been detected using software toolboxes that have resulted from this line of research. Even though there is a dire need for the property based validation and verification of analog and, especially, hybrid systems, similar results in the case of continuous time dynamical systems have not yet been achieved. Toward this direction, this original work utilizes the theory of robustness for real-time temporal logics and the theory of approximate bisimulations to infer the behavior of a neighborhood of system trajectories from a single system trajectory. A major advantage of this work is that the more robust the system is with respect to the logic formula the easier it is to verify its temporal properties. This testing framework can form the basis for a new approach in the verification/testing of analog and mixed signal circuits.

Hybrid System Synthesis from Temporal Logic Specifications

Complex operating regions as well as involved control specifications necessitate the development of hybrid control laws for the regulation of a dynamical system. A very characteristic example of such a system is a mobile robot that has to navigate through a labyrinth-like environment in order to perform a complex task. Such tasks (specifications) can be stated using Temporal Logics. For example, "(!D U A) /\ (!D U B) /\ (!D U C)" could be a formula for the specification "Visit rooms A, B and C while avoiding room D". The design by hand of non-trivial hybrid systems that have to satisfy complicated specifications is a tedious and error-prone procedure. Moreover, the verification of such systems in most of the cases is an undecidable problem. This project investigates certain classes of systems for which the synthesis problem from temporal logic specifications can be efficiently solved in a bottom-up fashion. In a bottom-up approach the controllers are provided and the synthesis procedure attempts to compose the controllers in such a way that the trajectories of the final system satisfy the specification.

From High-Level Specifications to Controller Specifications

The motivation for this project is the same as for the project "Hybrid System Synthesis from Temporal Logic Specifications". This project studies a top-down approach to the problem of hybrid system synthesis. Namely, given a high-level specification, the goal is to derive controller requirements such that the realization and subsequent composition of the controllers with the system will produce a hybrid system whose trajectories satisfy the specification. A top-down approach has the advantage over a bottom-up approach that the method does not have to look for a solution over a restricted set of controllers. The method to design the controllers depends on the respective controller specifications.

Human-Robot Interfaces

Consider a mobile robot that has to navigate through a labyrinth-like environment in order to perform a complex task. Such tasks (specifications) could be stated in natural or structured language by the user of the robot. For example, "Visit rooms A, B and C while avoiding room D" and "Patrol rooms A, B and C. If you detect a fire, call the fireman." could be two such input specifications. The interesting aspect of these types of specifications is that they can be captured by temporal logic formulas. However, writing and reading such specifications in temporal logics is a task that requires mathematical training. Therefore, the methods developed for robot motion and action planning through temporal logics become unapproachable to persons without the appropriate mathematical background. This research addresses the problem of translating structured language into temporal logic specifications in order to devise a completely automatic framework for robot motion and action planning from natural language input.

PAST RESEARCH

Techniques for Embedded System and Software Assurance (NEC Labs America)

For this project, a framework for the robustness analysis of Simulink simulations was developed. The main theoretical machinery that was employed for the analysis was self-validated arithmetics (interval and affine arithmetic). The goal of the project was to study the robustness and correctness of Simulink simulations under system uncertainties, numerical errors and floating point rounding errors. The outcome of the project was the Matlab toolbox RobSim which can analyze continuous-time, discrete-time and mixed-signal systems.

Modeling and Design of UAVs (University of Pennsylvania)

This project concerned the development of a number of autonomous Unmanned Aerial Vehicles (UAV) at the University of Pennsylvania. The following tasks were completed: (i) design of components for the UAVs, (ii) aerodynamic and stractural modeling of the UAVs, and (iii) hybrid system modeling of the UAVs when controlled by the autopilot.

Extended Ant Colony Optimization (National Technical University of Athens)

Ant Colony Optimization (ACO) is an innovative optimization method inspired by ants' behavior during foraging. ACO was introduced by M. Dorigo and applied to discrete optimization problems. In this work, the Extended Ant Colony Optimization (EACO) method was introduced for dealing with continuous optimization problems. EACO has been successfully applied to the problem of Inverse Design of Aerodynamic Shapes (IDS).