Robust Linear Temporal Logic (rLTL) was crafted to incorporate the notion of robustness into Linear-time Temporal Logic specifications. Robustness is ubiquitous in control systems and translates the intuitive notion that “small” violations of environment assumptions should only lead to “small” violations of system guarantees. This notion was formalized in the logic rLTL via 5 different truth values and it led to an increase in the time complexity of the associated model checking problem.

Abstract: The PIs are developing their novel modeling paradigm, Generalized Synchronization Trees (GSTs), into a rich framework for both describing cyber-physical systems (CPSs) and studying their behavior under interconnection. GSTs were inspired by Milner’s use of Synchronization Trees (STs) to model interconnected computing processes, but GSTs generalize the mathematical structure of their forebears in such a way as to encompass many classes of CPSs.

This project develops a theoretical framework as well as software tools to support testing and verification of a Cyber-Physical System (CPS) within a Model-Based Design (MBD) process. The theoretical bases of the framework are stochastic optimization methods, and robustness notions of formal specification languages.