Formalization and Verification of Group Behavior Interactions

Group behavior interactions, such as multirobot teamwork and group communications in social networks, are widely seen in both natural, social, and artificial behavior-related applications. Behavior interactions in a group are often associated with varying coupling relationships, for instance, conjunction or disjunction. Such coupling relationships challenge existing behavior representation methods, because they involve multiple behaviors from different actors, constraints on the interactions, and behavior evolution. In addition, the quality of behavior interactions are not checked through verification techniques. In this paper, we propose an ontology-based behavior modeling and checking system (OntoB for short) to explicitly represent and verify complex behavior relationships, aggregations, and constraints. The OntoB system provides both a visual behavior model and an abstract behavior tuple to capture behavioral elements, as well as building blocks. It formalizes various intra-coupled interactions (behaviors conducted by the same actor) via transition systems (TSs), and inter-coupled behavior aggregations (behaviors conducted by different actors) from temporal, inferential, and party-based perspectives. OntoB converts a behavior-oriented application into a TS and temporal logic formulas for further verification and refinement. We demonstrate and evaluate the effectiveness of the OntoB in modeling multirobot behaviors and their interactions in the Robocup soccer competition game. We show, that the OntoB system can effectively model complex behavior interactions, verify and refine the modeling of complex group behavior interactions in a sound manner.