Towards Verifiable Multi-Agent Interaction Pattern Specification

Abstract

Smart cyber agents play a crucial role in software-intensive systems by monitoring their physical surroundings and making impactful decisions. This paper addresses the challenge of specifying multi-agent patterns, which include interactions with human agents in possibly safety-critical environments. To this end, we introduce the foundations of a domain-agnostic and flexible Domain-Specific Language (DSL) called LIrAs. The language is designed to be accessible to users without programming expertise. LIrAs' semantics are mapped to Deterministic Finite-state Automata, making specifications amenable to formal verification. The DSL is exemplified through an illustrative scenario from the service robotics field.