-
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.
-
Robotic Wireless Networks in a Narrow Alley: A Game Theoretic Approach
Authors:
Taehyoung Shim,
Seong-Lyun Kim
Abstract:
There are many situations where vehicles may compete with each other to maximize their respective utilities.We consider a narrow alley where two groups, eastbound and westbound, of autonomous vehicles are heading toward each of their destination to minimize their travel distance. However, if the two groups approach the road simultaneously, it will be blocked. The main goal of this paper is to inve…
▽ More
There are many situations where vehicles may compete with each other to maximize their respective utilities.We consider a narrow alley where two groups, eastbound and westbound, of autonomous vehicles are heading toward each of their destination to minimize their travel distance. However, if the two groups approach the road simultaneously, it will be blocked. The main goal of this paper is to investigate how wireless communications among the vehicles can lead the solution near to Pareto optimum. In addition, we implemented such a vehicular test-bed, composed of networked robots that have an infrared sensor, a DC motor, and a wireless communication module: ZigBee (IEEE 802.15.4).
△ Less
Submitted 2 March, 2015;
originally announced March 2015.
-
Traffic Convexity Aware Cellular Networks: A Vehicular Heavy User Perspective
Authors:
Taehyoung Shim,
Jihong Park,
Seung-Woo Ko,
Seong-Lyun Kim,
Beom Hee Lee,
** Gu Choi
Abstract:
Rampant mobile traffic increase in modern cellular networks is mostly caused by large-sized multimedia contents. Recent advancements in smart devices as well as radio access technologies promote the consumption of bulky content, even for people in moving vehicles, referred to as vehicular heavy users. In this article the emergence of vehicular heavy user traffic is observed by field experiments co…
▽ More
Rampant mobile traffic increase in modern cellular networks is mostly caused by large-sized multimedia contents. Recent advancements in smart devices as well as radio access technologies promote the consumption of bulky content, even for people in moving vehicles, referred to as vehicular heavy users. In this article the emergence of vehicular heavy user traffic is observed by field experiments conducted in 2012 and 2015 in Seoul, Korea. The experiments reveal that such traffic is becoming dominant, captured by the 8.62 times increase in vehicular heavy user traffic while the total traffic increased 3.04 times. To resolve this so-called vehicular heavy user problem (VHP), we propose a cell association algorithm that exploits user demand diversity for different velocities. This user traffic pattern is discovered first by our field trials, which is convex-shaped over velocity, i.e. walking user traffic is less than stationary or vehicular user traffic. As the VHP becomes severe, numerical evaluation verifies the proposed user convexity aware association outperforms a well-known load balancing association in practice, cell range expansion (CRE). In addition to the cell association, several complementary techniques are suggested in line with the technical trend toward 5G.
△ Less
Submitted 21 August, 2015; v1 submitted 12 January, 2015;
originally announced January 2015.
-
An Introduction to Socially Connected Machines: Characteristics and Applications
Authors:
Taehyoung Shim,
Dong Min Kim,
Seong-Lyun Kim
Abstract:
Due to the development of information and communication technologies, it is difficult to handle the billions of connected machines. In this paper, to cope with the problem, we introduce machine social networks, where they freely follow each other and share common interests with their neighbors. We classify characteristics and describe required functionalities of socially connected machines. We als…
▽ More
Due to the development of information and communication technologies, it is difficult to handle the billions of connected machines. In this paper, to cope with the problem, we introduce machine social networks, where they freely follow each other and share common interests with their neighbors. We classify characteristics and describe required functionalities of socially connected machines. We also illustrate two examples; a twit-bot and maze scenario.
△ Less
Submitted 20 December, 2013;
originally announced December 2013.
