LLMs for Executable Multi-Agent System Specification Generation

Andreas Kouvaras; Periklis Mantenoglou; Alexander Artikis

cs.AISep 28, 2026

LLMs for Executable Multi-Agent System Specification Generation

Authors: Andreas Kouvaras, Periklis Mantenoglou, Alexander Artikis

Organizations: University of Piraeus, Greece. · Örebro University, Sweden. · NCSR “Demokritos”, Greece.

Abstract

MAS specifications express the effects of the actions of the agents and their environment, as well as other temporal phenomena, such as the intervals during which an agent may perform an action. The specification of a MAS should also be executable in order to allow for run-time monitoring. Constructing the specification of a MAS requires formal language expertise, while machine learning techniques depend on labelled data which are rarely available. To address these issues, we propose genRTEC', a method that leverages pre-trained Large Language Models (LLMs) to generate executable MAS specifications, in the language of the Run-Time Event Calculus' (RTEC), from natural language descriptions. genRTEC constructs MAS specifications with complex hierarchical and cyclic dependencies based only on short natural language descriptions of the concepts involved. We present an extensive empirical evaluation of genRTEC, spanning various MAS specifications, including both a qualitative and a quantitative assessment. Our results demonstrate that genRTEC constructs executable MAS specifications of high predictive accuracy without compromising reasoning efficiency.

Figures & tables

Predicate	Meaning
happensAt $\it(E,T)$	Event $\it E$ occurs at time-point $\it T$ .
initiatedAt $\it(F\val V,T)$	At time-point $\it T$ , a period of time
	during which $\it F\val V$ is initiated.
terminatedAt $\it(F\val V,T)$	At time-point $\it T$ , a period of time
	during which $\it F\val V$ is terminated.
holdsFor $\it(F\val V,I)$	$\it I$ is the list of the maximal intervals

Table 1 : The main predicates of RTEC.

Figure 1 : Interval manipulation constructs of RTEC.

\it I_{1}

\it I_{2}

and

\it I_{3}

(resp.

\it I_{c}

\it I_{i}

and

\it I_{u}

) are input (output) lists of maximal intervals.

Figure 2 : Dependency graph fragment of the event description for ARG. Underscores denote variables grounded on input entities, action types or agent roles.

Figure 3 : genRTEC: LLM prompting for executable MAS specification generation. In this illustration, genRTEC is used for the construction of the specifications of a negotation protocol, a voting protocol and an argumentation protocol. Prompt B is optional.

	NET	VP	ARG	MSA	CTM	ACR	CG
Rules	15	15	24	32	23	9	19
Conditions	27	29	61	105	52	31	30
Cyclic Dependencies	✓	✓	✓	✗	✗	✗	✓
Dataset Items	132K	100K	100K	15M	50K	182K	N/A

Table 2 : Size of ground truth specifications and datasets

Panel of Figure 4 — Figure 4 : The dependency graphs of the hand-crafted specifications of NET, VP and ARG. To avoid clutter, we omitted the FVPs from the nodes and the edges in a cycle. The nodes in a cycle are coloured red, blue or green. We grouped together the nodes of the same level, i.e. NET has four levels, VP has three levels, and ARG has four levels.

Panel of Figure 5 — Figure 5 : Syntactic similarity (line-hatched bars) and f1-score (dotted bars) of genRTEC-constructed specifications compared to ground truth specifications. ‘ $\it\triangle$ ’, ‘ $\it\blacktriangle$ ’ and ‘ $\it\blacksquare$ ’ refer to the use of GPT, Gemini and Claude.

Panel of Figure 6 — Figure 6 : Reasoning times of RTEC when operating on genRTEC-constructed specifications and ground truth specifications. ‘ $\it\triangle$ ’, ‘ $\it\blacktriangle$ ’ and ‘ $\it\blacksquare$ ’ refer to the use of GPT, Gemini and Claude, and ‘ $\it\circ$ ’ refers to the ground truth specifications. The ranges of values in the vertical axes differ.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 7 — Figure 7 : The dependency graphs of the hand-crafted specifications of MSA, CTM, ACR and CG. The use of red colour indicates a cyclic dependency.

Explore similar work

Translating Natural Language to Strategic Temporal Specifications via LLMs
Jun 29, 2026Marco Aruta, Francesco Improta, Vadim Malvone +2Multi-Agent Large Language Model Systems Natural Language
University of Naples Federico II, Naples, Italy · LTCI, Télécom Paris, Institut Polytechnique de Paris, Palaiseau, France · STIMicroelectronics, Grenoble, France
RepoMAS: Solving Progressively Specified Tasks with Issue-Driven Multi-Agent Systems
Sep 26, 2026Yuchen Song, Andong Chen, Wenxin Zhu +2Model-Based Multi-Agent Systems Open-Source
Harbin Institute of Technology, Harbin, China
MAS-Lab: A Specification-Driven Validation Framework for Reliable Multi-Agent Systems
Jun 29, 2026Jordan Augé, Giovanna Carofiglio, Giulio Grassi +1Model-Based Multi-Agent Systems Agentic Framework
Cisco Systems Paris, France

Jun 29, 2026, cs.MAJ/K move · Enter open · S save

Translating Natural Language to Strategic Temporal Specifications via LLMs

Marco Aruta, Francesco Improta, Vadim Malvone, Aniello Murano+1

University of Naples Federico II, Naples, Italy · LTCI, Télécom Paris, Institut Polytechnique de Paris, Palaiseau, France · STIMicroelectronics, Grenoble, France

Multi-Agent Large Language Model Systems Natural Language Probabilistic Model Checking Multi-Agent Communication

Open paper AskPDF arXiv

A rigorous formalization of system requirements is a fundamental prerequisite for the verification of Multi-Agent Systems (MAS). However, writing correct formal specifications is well known as an error-prone, time-consuming, and expertise-intensive task. This difficulty is further accentuated in MAS, where requirements must capture strategic abilities and temporal objectives. At present, there is no established methodology for deriving MAS specifications from natural language. We present a framework for translating Natural Language descriptions of strategic requirements into well-formed ATL/ATL* formulas using Large Language Models (LLMs). Since no available dataset supports supervised learning for the NL-to-ATL/ATL* translation task, we create and curate a novel expert-validated dataset, employed for training and evaluating fine-tuned models. On a held-out test set, evaluated under the LLM judge that best agrees with expert annotations, in-domain fine-tuning of small open-weight models (3 - 7B parameters) matches strong few-shot proprietary API baselines. Our best fine-tuned system reaches 0.84 semantic accuracy, statistically on par with 0.86 for the strongest few-shot proprietary baseline, while keeping requirements on-premises. We further find that judge reliability is inverse to generator strength. The open-weight Llama-3.3-70B tracks human verdicts most closely, whereas the strongest proprietary models are the least reliable judges, over-rejecting faithful paraphrases of the reference. To assess the practical applicability of the generated specifications, we embed our tool to an existing strategic logics model checker, enabling non-expert users to specify strategic properties in natural language.

Abstract

Explore similar work

Translating Natural Language to Strategic Temporal Specifications via LLMs

RepoMAS: Solving Progressively Specified Tasks with Issue-Driven Multi-Agent Systems

MAS-Lab: A Specification-Driven Validation Framework for Reliable Multi-Agent Systems