skip to main content


Search for: All records

Editors contains: "Silva, A."

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. Silva, A. (Ed.)
    This paper presents Verisig 2.0, a verification tool for closed-loop systems with neural network (NN) controllers. We focus on NNs with tanh/sigmoid activations and develop a Taylor-model-based reachability algorithm through Taylor model preconditioning and shrink wrapping. Furthermore, we provide a parallelized implementation that allows Verisig 2.0 to efficiently handle larger NNs than existing tools can. We provide an extensive evaluation over 10 benchmarks and compare Verisig 2.0 against three state-of-the-art verification tools. We show that Verisig 2.0 is both more accurate and faster, achieving speed-ups of up to 21x and 268x against different tools, respectively. 
    more » « less
  2. Silva, A. and (Ed.)
    We present 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋 converts the scenario verification problem to a standard hybrid system verification problem, and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋 uses symmetry abstractions, a novel refinement algorithm, and importantly, is built to boost the performance of any existing reachability analysis tool as a plug-in subroutine. We evaluated 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋 on several scenarios involving ground and aerial vehicles with nonlinear dynamics and neural network controllers, employing different kinds of symmetries, using different reachability subroutines, and following plans with hundreds of waypoints in complex workspaces. Compared to two leading tools, DryVR and Flow*, 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋 shows 14Γ— average speedup in verification time, even while using those very tools as reachability subroutines. 
    more » « less
  3. Silva, A. ; Leino, K.R.M. (Ed.)
    We study reinforcement learning for the optimal control of Branching Markov Decision Processes (BMDPs), a natural extension of (multitype) Branching Markov Chains (BMCs). The state of a (discrete-time) BMCs is a collection of entities of various types that, while spawning other entities, generate a payoff. In comparison with BMCs, where the evolution of a each entity of the same type follows the same probabilistic pattern, BMDPs allow an external controller to pick from a range of options. This permits us to study the best/worst behaviour of the system. We generalise model-free reinforcement learning techniques to compute an optimal control strategy of an unknown BMDP in the limit. We present results of an implementation that demonstrate the practicality of the approach. 
    more » « less
  4. Silva, A. ; Leino, K.R.M. (Ed.)
    In the Adapter-Design Pattern, a programmer implements a Target interface by constructing an Adapter that accesses an existing Adaptee code. In this work, we presented a reactive synthesis interpretation to the adapter design pattern, wherein an algorithm takes an Adaptee and a Target transducers, and the aim is to synthesize an Adapter transducer that, when composed with the Adaptee, generates a behavior that is equivalent to the behavior of the Target. One use of such an algorithm is to synthesize controllers that achieve similar goals on different hardware platforms. While this problem can be solved with existing synthesis algorithms, current state-of-the-art tools fail to scale. To cope with the computational complexity of the problem, we introduced a special form of specification format, called Separated GR(k), which can be solved with a scalable synthesis algorithm but still allows for a large set of realistic specifications. We solved the realizability and the synthesis problems for Separated GR(k), and showed how to exploit the separated nature of our specification to construct better algorithms, in terms of time complexity, than known algorithms for GR(k) synthesis. We then described a tool, called SGR(k), which we have implemented based on the above approach and showed, by experimental evaluation, how our tool outperforms current state-of-the-art tools on various benchmarks and test-cases. 
    more » « less