A Science of CPS Robustness

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. In this poster we highlight our most recent results that consist of a fragment of rLTL for which the model checking problem can be solved using generalized Buchi automata with at most 3^|phi| states where |phi| denotes the length of an rLTL formula phi. This is a substantial improvement over the previously known bound of 5^|phi| and close to the tight upper bound 2^|phi| for LTL.