Runtime verification of self-adaptive multi-agent system using probabilistic timed automata

The self-adaptive multi-agent system requires adaptive adjustments based on the dynamic environment during its runtime. Heterogeneous agent can accomplish different task goals, enhance the efficiency of system operation, but its complex collaboration problem poses new challenges to the study of verification of adaptive policies for heterogeneous multi-agents. This paper proposes a runtime verification method for self-adaptive multi-agent systems using probabilistic timed automata. The method constructs a probabilistic timed automaton model by formally describing the functional characteristics of heterogeneous agents and integrating random factors in the environment to simulate the operation process of the self-adaptive multi-agent system. Regarding the collaboration logic among heterogeneous agents, security constraints are established to ensure the security of state transition processes during system operation. Combining model checking with runtime quantitative verification methods to conduct experiment and applying it in the case of an intelligent unmanned parking system. Experimental results manifest the correctness of the cooperation logic between agents can effectively ensure the stability of the system at runtime. Significant improvement in system uptime and efficiency compared to the initial system without runtime quantitative validation.