Static Analysis of BDI Agents on CPS using Petri Nets and MDE Techniques

This paper introduces a method for the static analysis of belief-desire-intention (BDI) agents integrated with cyber-physical systems (CPS) using Petri nets (PN) and Model-driven Engineering (MDE) techniques, especially for their communication. CPS integrates computational and physical elements that need verification to ensure correct and safe operations before deploying BDI agents. The BDI agents provide intelligent behaviour in CPS, while PN provides a framework for analyzing these behaviours. By simulating PN, the operation of BDI agents can be analysed statically before deployment on CPS. In this regard, MDE enables the transformation of the semantic space of BDI agents into PN. Due to the BDI model's high-level abstraction, high-level expressiveness, such as Colored Petri nets (CPN), is required to detect undesired execution paths within the agent or from another agent via messaging. This process applies the Jason BDI AgentSpeak codes translation into a CPN model. This mapping paves the way to verify reachability, boundedness, and deadlock properties. Additionally, a case study is presented to illustrate the method's applicability. The results demonstrate the feasibility of this approach with multiple agents communicating via a specific messaging structure.