Exploring and Evaluating Interplays of BPpy with Deep Reinforcement Learning and Formal Methods

TL;DR

This paper investigates how Behavioral Programming (BP) can be integrated with AI and Formal Methods tools, including Deep Reinforcement Learning, to enhance modeling and analysis of complex systems within a unified framework.

Contribution

It introduces the BPpy framework's integration with AI and FM tools, demonstrating enhanced capabilities for modeling and analyzing complex systems.

Findings

BPpy effectively integrates with SMT solvers and model checkers.

Combining BP with DRL scales modeling of complex behaviors.

Unified framework supports multifaceted analysis and development.

Abstract

We explore and evaluate the interactions between Behavioral Programming (BP) and a range of Artificial Intelligence (AI) and Formal Methods (FM) techniques. Our goal is to demonstrate that BP can serve as an abstraction that integrates various techniques, enabling a multifaceted analysis and a rich development process. Specifically, the paper examines how the BPpy framework, a Python-based implementation of BP, is enhanced by and enhances various FM and AI tools. We assess how integrating BP with tools such as Satisfiability Modulo Theory (SMT) solvers, symbolic and probabilistic model checking, and Deep Reinforcement Learning (DRL) allow us to scale the abilities of BP to model complex systems. Additionally, we illustrate how developers can leverage multiple tools within a single modeling and development task. The paper provides quantitative and qualitative evidence supporting the feasibility of our vision to create a comprehensive toolbox for harnessing AI and FM methods in a unified development framework.