# Engineering Commons™

CPS Theory

2017

Real-Time and Embedded Systems Lab (mLAB)

Articles 1 - 3 of 3

## Full-Text Articles in Engineering

Smooth Operator: Control Using The Smooth Robustness Of Temporal Logic, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam Aug 2017

#### Smooth Operator: Control Using The Smooth Robustness Of Temporal Logic, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

##### Real-Time and Embedded Systems Lab (mLAB)

Modern control systems, like controllers for swarms of quadrotors, must satisfy complex control objectives while withstanding a wide range of disturbances, from bugs in their software to attacks on their sensors and changes in their environments. These requirements go beyond stability and tracking, and involve temporal and sequencing constraints on system response to various events. This work formalizes the requirements as formulas in Metric Temporal Logic (MTL), and designs a controller that maximizes the robustness of the MTL formula. Formally, if the system satisfies the formula with robustness r, then any disturbance of size less than r cannot cause it ...

Technical Report: Control Using The Smooth Robustness Of Temporal Logic, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam Mar 2017

#### Technical Report: Control Using The Smooth Robustness Of Temporal Logic, Yash Vardhan Pant, Houssam Abbas, Rahul Mangharam

##### Real-Time and Embedded Systems Lab (mLAB)

Cyber-Physical Systems must withstand a wide range of errors, from bugs in their software to attacks on their physical sensors. Given a formal specification of their desired behavior in Metric Temporal Logic (MTL), the robust semantics of the specification provides a notion of system robustness that can be calculated directly on the output behavior of the system, without explicit reference to the various sources or models of the errors. The robustness of the MTL specification has been used both to verify the system offline (via robustness minimization) and to control the system online (to maximize its robustness over some horizon ...

Relaxed Decidability And The Robust Semantics Of Metric Temporal Logic, Houssam Abbas, Matthew O'Kelly, Rahul Mangharam Feb 2017

#### Relaxed Decidability And The Robust Semantics Of Metric Temporal Logic, Houssam Abbas, Matthew O'Kelly, Rahul Mangharam

##### Real-Time and Embedded Systems Lab (mLAB)

Relaxed notions of decidability widen the scope of automatic verification of hybrid systems. In quasi-decidability and $\delta$-decidability, the fundamental compromise is that if we are willing to accept a slight error in the algorithm's answer, or a slight restriction on the class of problems we verify, then it is possible to obtain practically useful answers. This paper explores the connections between relaxed decidability and the robust semantics of Metric Temporal Logic formulas. It establishes a formal equivalence between the robustness degree of MTL specifications, and the imprecision parameter $\delta$ used in $\delta$-decidability when it is used to ...