SNR 2015: Papers with Abstracts

Abstract. We consider the problem of reachability analysis in hybrid systems defined by the closed-loop interaction of a complex, continuous time plant model with a software-based controller. In practice, the plant model is, often, a coarse approximation of the real-world operating environment of the software, whereas the software itself is the artifact that ends up being deployed in the final system. In this talk, we summarize the state-of-the-art techniques for purely symbolic and purely numeric approaches to reachability analysis of hybrid systems. We make the case for approaches that combine simulation-based exploration of the plant state-space with a corresponding symbolic exploration of the controller. We propose a simple yet elegant method to carry out this joint symbolic-numeric exploration based on an abstraction of the plant model, and present promising experimental results on software-in-the-loop setups that are beyond the scope of many existing verification tools.

Abstract. Stochastic Satisfiability Modulo Theories (SSMT) is a quantitative exten-
sion of classical Satisfiability Modulo Theories (SMT) inspired by stochastic
logics. It extends SMT by the usual as well as randomized quantifiers, fa-
cilitating capture of stochastic game properties in the logic, like reachability
analysis of hybrid-state Markov decision processes. Solving for SSMT for-
mulae with quantification over finite and thus discrete domain has been ad-
dressed by Tino Teige et al. In our work, we extend their work to SSMT
over continuous quantifier domains (CSSMT) in order to enable capture of,
e.g., continuous disturbances and uncertainty in hybrid systems. We extend
the semantics of SSMT and introduce a corresponding solving procedure. A
discussion regarding to reachability analysis is given to demonstrate applica-
bility of our framework to reachability problems in hybrid systems.

Abstract. Towards the goal of correctness and reliability of hybrid systems, we continue our nonstandard static analysis program (with Suenaga and Sekine) where hybrid dynamics is turned into purely discrete one with explicit use of infinitesimals. While our previous results have focused on deductive verification by program logics, the current work aims at automation and enhanced scalability by extending abstract interpretation—a technique known for its ample scalability and widespread use in various verification tools—with infinitesimals. Our theoretical results include soundness and termination via uniform widening operators; and our prototype implementation successfully verifies some benchmark examples.

Abstract. Viability and discriminating kernels are powerful constructs for analyzing system safety through model checking, but until recently the only computational algorithms available were nonparametric grid-based approaches which, although accurate, scaled exponentially with the dimension of the system's state space. In contrast, several polynomial complexity reachability algorithms have been developed using various parametric set representations. In a recent series of papers, two of these parametric approaches -- based on ellipsoids and support vectors -- have been adapted to approximate viability and discriminating kernels in the discrete, continuous and sampled data models of time. This paper briefly summarizes these algorithms and compares their key features with one another and with a representative nonparametric approach.

Abstract. This paper summarizes results related to a novel algorithmic approach for verifying stability of hybrid systems. The traditional approach based on Lyapunov function search suffers from several disadvantages --- it relies on the user expertise to obtain good templates for the Lyapunov function; further, an unsuccessful attempt at instantiating the templates provides no insights into the choice of better templates. To overcome these difficulties, the algorithmic approach relies on an abstraction refinement framework which systematically searches for a proof and provides insights to the user in the event of a failure to prove stability. We summarize the new foundations, techniques and software tools that we have developed for the algorithmic approach to stability verification.

Abstract. In this paper we present a summary of our work on probability reachability in stochastic hybrid systems (SHS). In particular, we give an overview of ProbReach, a tool for computing probabilistic reachability in SHS which we introduced in our HSCC 2015 paper. We also present and an overview of our recent theoretical extensions and modification of the tool.