We propose an automatic synthesis technique to generate provably correct controllers of stochastic linear dynamical systems for Signal Temporal Logic (STL) specifications. While formal synthesis problems can be directly formulated as exists-forall constraints, the quantifier alternation restricts the scalability of such an approach. We use the duality between a system and its proof of correctness to partially alleviate this challenge. We decompose the controller synthesis into two subproblems, each addressing orthogonal concerns - stabilization with respect to the noise, and meeting the STL specification. The overall controller is a nested controller comprising of the feedback controller for noise cancellation and an open loop controller for STL satisfaction. The correct-by-construction compositional synthesis of this nested controller relies on using the guarantees of the feedback controller instead of the controller itself. We use a linear feedback controller as the stabilizing controller for linear systems with bounded additive noise and over-approximate its ellipsoid stability guarantee with a polytope. We then use this over-approximation to formulate a mixed-integer linear programming problem (MILP) to synthesize an open-loop controller that satisfies STL specifications. We demonstrate the effectiveness of the proposed technique on a set of case studies.
The paper presents a new defense against adversarial attacks for deep neural networks. We demonstrate the effectiveness of our approach against the popular adversarial image generation method DeepFool. Our approach uses Wald's Sequential Probability Ratio Test to sufficiently sample a carefully chosen neighborhood around an input image to determine the correct label of the image. On a benchmark of 50,000 randomly chosen adversarial images generated by DeepFool we demonstrate that our method SATYA is able to recover the correct labels for 95.76% of the images for CaffeNet and 97.43% of the correct label for GoogLeNet.
Autonomous cyber-physical systems rely on modern machine learning methods such as deep neural networks to control their interactions with the physical world. Testing of such intelligent cyber-physical systems is a challenge due to the huge state space associated with high-resolution visual sensory inputs. In this paper, we demonstrate how fuzzing the input using patterns obtained from the convolutional lters of an unrelated convolutional neural network can be used to test the correctness of vision algorithms implemented in intelligent cyber-physical systems. Our method discovers interesting counterexamples to the pedestrian detection algorithm implemented in the popular OpenCV library. Our approach also unearths counterexamples to the correct behavior of an autonomous car similar to NVIDIA’s end-to-end self-driving deep neural net running on the Udacity open-source simulator.
Verifying the correctness of intelligent embedded systems is notoriously difficult due to the use of machine learning algorithms that cannot provide guarantees of deterministic correctness. In this paper, we investigate the histogram of oriented gradients (HOG) based human detection algorithm implemented in the popular OpenCV computer vision framework. Our validation efforts demonstrate that the OpenCV imple- mentation is susceptible to errors due to both malicious perturbations and naturally occurring fog phenomena. To the best of our knowledge, we are the first to explicitly employ a natural perturbation (like fog) as an adversarial attack using methods from computer graphics and demonstrate that computer vision algorithms are also susceptible to errors under such naturally occurring minor perturbations. Our methods and results may be of interest to the designers, developers and validation teams of intelligent cyber-physical systems such as autonomous cars.
Validating the correctness of human detection vision systems is crucial for safety applications such as pedestrian collision avoidance in autonomous vehicles. The enormous space of possible inputs to such an intelligent system makes it difficult to design test cases for such systems. In this paper, we present our tool MAYA that uses an error model derived from a convolutional neural network (CNN) to explore the space of images similar to a given input image, and then tests the correctness of a given human or object detection system on such perturbed images. We demonstrate the capability of our tool on the pre-trained Histogram-of- Oriented-Gradients (HOG) human detection algorithm implemented in the popular OpenCV toolset and the Caffe object detection system pre-trained on the ImageNet benchmark. Our tool may serve as a testing resource for the designers of intelligent human and object detection systems.
R. Saha, J. Esparza, S. K. Jha, M. Mukund, and P. S. Thiagarajan, “
Distributed Markov Chains
,” in Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, 2015, pp. 117–134. Publisher's Version
Our goal is to find the set of parameters for which a given linear hybrid automaton does not reach a given set of bad states. The problem is known to be semi-solvable (if the algorithm terminates the result is correct) by introducing the parameters as state variables and computing the set of reachable states. This is usually too expensive, how- ever, and in our experiments only possible for very simple systems with few parameters. We propose an adaptation of counterexample-guided abstraction refinement (CEGAR) with which one can obtain an under- approximation of the set of good parameters using linear programming. The adaptation is generic and can be applied on top of any CEGAR method where the counterexamples correspond to paths in the concrete system. For each counterexample, the cost incurred by underapproximat- ing the parameters is polynomial in the number of variables, parameters, and the length of counterexample. We identify a syntactic condition for which the approach is complete in the sense that the underapproxima- tion is empty only if the problem has no solution. Experimental results are provided for two CEGAR methods, a simple discrete version and iterative relaxation abstraction (IRA), both of which show a drastic im- provement in performance compared to standard reachability.
This paper presents the design of a novel distributed algo- rithm d-IRA for the reachability analysis of linear hybrid automata. Re- cent work on iterative relaxation abstraction (IRA) is leveraged to dis- tribute the reachability problem among multiple computational nodes in a non-redundant manner by performing careful infeasibility analysis of linear programs corresponding to spurious counterexamples. The d-IRA algorithm is resistant to failure of multiple computational nodes. The ex- perimental results provide promising evidence for the possible successful application of this technique.
Procedures for analysis of linear hybrid automata (LHA) do not scale well with the number of continuous state variables in the model. This paper introduces iterative relaxation abstraction (IRA), a new method for reachability analysis of LHA that aims to improve scal- ability by combining the capabilities of current tools for analysis of low- dimensional LHA with the power of linear programming (LP) for large numbers of constraints and variables. IRA is inspired by the success of counterexample guided abstraction refinement (CEGAR) techniques in verification of discrete systems. On each iteration, a low-dimensional LHA called a relaxation abstraction is constructed using a subset of the continuous variables from the original LHA. Hybrid system reachabil- ity analysis then generates a regular language called the discrete path abstraction representing all possible counterexamples (paths to the bad locations) in the relaxation abstraction. If the discrete path abstraction is non-empty, a particular counterexample is selected and LP infeasibil- ity analysis determines if the counterexample is spurious using the con- straints along the path from the original high-dimensional LHA. If the counterexample is spurious, LP techniques identify an irreducible infeasi- ble subset (IIS) of constraints from which the set of continuous variables is selected for the the construction of the next relaxation abstraction. IRA stops if the discrete path abstraction is empty or a legitimate coun- terexample is found. The effectiveness of the approach is illustrated with an example.
Model checking is very effective at finding out even subtle faults in system designs. A counterexample is usually generated by model checking algorithms when a system does not satisfy the given specification. However, a counterexample is not always helpful in explaining and isolating faults in a system when the counterexample is very long, which is usually the case for large scale systems. As such, there is a pressing need to develop fault explanation and isolation techniques. In this paper, we present a new approach for the fault explanation and isolation in discrete event systems with LTL (linear-time temporal logic) specifications. The notion of fault seed is introduced to characterize the cause of a fault. The identification of the fault seed is further reduced to a model checking problem. An algorithm is obtained for the fault seed identification. An example is provided to demonstrate the effectiveness of the approach developed.
Counterexample guided abstraction refinement, a powerful technique for verifying properties of discrete-state systems [4, 9] has been extended recently to hybrid systems verification [1, 3]. Unlike in discrete systems, however, estab- lishing the successor relation for hybrid systems can be a fairly expensive step since it requires evaluation and overapproximation of the continuous dynamics. In  it has been observed that it is often sufficient to consider fragments of counterexamples rather than complete counterexamples. In this paper we further develop the idea of fragments. We extend the notion of cut sets in network flows to cutting sets of fragments in abstractions. Cutting sets of fragments are then uses guide the abstraction refinement in order to prove safety properties for hy- brid systems.