-
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Authors:
Udayan Mandal,
Guy Amir,
Haoze Wu,
Ieva Daukantas,
Fletcher Lee Newell,
Umberto J. Ravaioli,
Baoluo Meng,
Michael Durling,
Milan Ganai,
Tobey Shim,
Guy Katz,
Clark Barrett
Abstract:
Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the "black box" nature of DRL agents limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent's behavior is to use Neural Lyapunov Barrier (NLB) certificates, which are learned functions…
▽ More
Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the "black box" nature of DRL agents limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent's behavior is to use Neural Lyapunov Barrier (NLB) certificates, which are learned functions over the system whose properties indirectly imply that an agent behaves as desired. However, NLB-based certificates are typically difficult to learn and even more difficult to verify, especially for complex systems. In this work, we present a novel method for training and verifying NLB-based certificates for discrete-time systems. Specifically, we introduce a technique for certificate composition, which simplifies the verification of highly-complex systems by strategically designing a sequence of certificates. When jointly verified with neural network verification engines, these certificates provide a formal guarantee that a DRL agent both achieves its goals and avoids unsafe behavior. Furthermore, we introduce a technique for certificate filtering, which significantly simplifies the process of producing formally verified certificates. We demonstrate the merits of our approach with a case study on providing safety and liveness guarantees for a DRL-controlled spacecraft.
△ Less
Submitted 22 May, 2024;
originally announced May 2024.
-
Local Area Routes for Vehicle Routing Problems
Authors:
Udayan Mandal,
Amelia Regan,
Julian Yarkony
Abstract:
We consider an approach for improving the efficiency of column generation (CG) methods for solving vehicle routing problems. We introduce Local Area (LA) route relaxations, an alternative/complement to the commonly used ng-route relaxations and Decremental State Space Relaxations (DSSR) inside of CG formulations. LA routes are a subset of ng-routes and a super-set of elementary routes. Normally, t…
▽ More
We consider an approach for improving the efficiency of column generation (CG) methods for solving vehicle routing problems. We introduce Local Area (LA) route relaxations, an alternative/complement to the commonly used ng-route relaxations and Decremental State Space Relaxations (DSSR) inside of CG formulations. LA routes are a subset of ng-routes and a super-set of elementary routes. Normally, the pricing stage of CG must produce elementary routes, which are routes without repeated customers, using processes which can be computationally expensive. Non-elementary routes visit at least one customer more than once, creating a cycle. LA routes relax the constraint of being an elementary route in such a manner as to permit efficient pricing. LA routes are best understood in terms of ng-route relaxations. Ng-routes are routes which are permitted to have non-localized cycles in space; this means that at least one intermediate customer (called a breaker) in the cycle must consider the starting customer in the cycle to be spatially far away. LA routes are described using a set of special indexes corresponding to customers on the route ordered from the start to the end of the route. LA route relaxations further restrict the set of permitted cycles beyond that of ng-routes by additionally enforcing that the breaker must be a located at a special index where the set of special indexes is defined recursively as follows. The first special index in the route is at index 1 meaning that it is associated with the first customer in the route. The k'th special index corresponds to the first customer after the k-1'th special index, that is not considered to be a neighbor of (considered spatially far from) the customer located at the k-1'th special index. We demonstrate that LA route relaxations can significantly improve the computational speed of pricing when compared to the standard DSSR.
△ Less
Submitted 10 July, 2022;
originally announced July 2022.
-
On Service-Chaining Strategies using Virtual Network Functions in Operator Networks
Authors:
Abhishek Gupta,
M. Farhan Habib,
Uttam Mandal,
Pulak Chowdhury,
Massimo Tornatore,
Biswanath Mukherjee
Abstract:
Network functions (e.g., firewalls, load balancers, etc.) have been traditionally provided through proprietary hardware appliances. Often, hardware appliances need to be hardwired back to back to form a service chain providing chained network functions. Hardware appliances cannot be provisioned on demand since they are statically embedded in the network topology, making creation, insertion, modifi…
▽ More
Network functions (e.g., firewalls, load balancers, etc.) have been traditionally provided through proprietary hardware appliances. Often, hardware appliances need to be hardwired back to back to form a service chain providing chained network functions. Hardware appliances cannot be provisioned on demand since they are statically embedded in the network topology, making creation, insertion, modification, upgrade, and removal of service chains complex, and also slowing down service innovation. Hence, network operators are starting to deploy Virtual Network Functions (VNFs), which are virtualized over commodity hardware. VNFs can be deployed in Data Centers (DCs) or in Network Function Virtualization (NFV) capable network elements (nodes) such as routers and switches. NFV capable nodes and DCs together form a Network enabled Cloud (NeC) that helps to facilitate the dynamic service chaining required to support evolving network traffic and its service demands. In this study, we focus on the VNF service chain placement and traffic routing problem, and build a model for placing a VNF service chain while minimizing network resource consumption. Our results indicate that a NeC having a DC and NFV capable nodes can significantly reduce network-resource consumption.
△ Less
Submitted 10 November, 2016;
originally announced November 2016.
