Towards Static Analysis of BDI Agents on CPS Using Petri Nets and Model-Driven Engineering

Towards Static Analysis of BDI Agents on CPS Using Petri Nets and Model-Driven Engineering

연구 분야: Strategies

학회: International Conference on Practical Applications of Agents and Multi-Agent Systems

This paper presents an approach for the static analysis of the belief-desire-intention (BDI) agents deployed on cyber-physical systems (CPS) using the Petri nets (PN) and Model-driven Engineering (MDE) techniques. A CPS integrates computational and physical components that require verification to ensure correct and safe operation before executing the BDI agents deployed on the CPS. The BDI agent architecture provides a model for programming intelligent behaviour on CPS, while PN offers a formalism for analyzing these behaviours. This way, the operation of the BDI agents can be statically analyzed by simulating the PN before their deployment on the CPS. To this end, the semantic space of the BDI agents can be transformed into the PN by MDE. Since the BDI model provides a high-level programming abstraction that requires high expressiveness, the Coloured Petri nets (CPN) formalism has been employed to detect the undesired execution paths. Hence, BDI agents are mapped onto Petri nets, allowing the translation of the Jason BDI AgentSpeak code into a CPN model. This mapping verifies properties such as reachability, boundedness and deadlock. Moreover, a case study is presented to demonstrate the approach’s applicability. The results highlight the proof-of-concept of this approach on a single but pertinent agent to identify and resolve potential issues, contributing to developing verified CPSs.