Source-linked AI summary
LLMs for Executable Multi-Agent System Specification Generation
Andreas Kouvaras, Periklis Mantenoglou, Alexander Artikis
TL;DR
MAS specifications need to represent temporal behavior and be executable for run-time monitoring, but construction requires formal-language expertise and labelled examples for specialised learning are scarce. genRTEC uses pre-trained LLMs to generate RTEC specifications from natural-language descriptions, and its evaluation reports high predictive accuracy without compromising reasoning efficiency.
Problem
MAS specifications require formal-language expertise to construct, while specialised machine-learning techniques depend on labelled datasets that are scarce.
Source: §1 · p. 2Method
GenRTEC uses pre-trained LLMs to translate natural-language descriptions of MAS building blocks into executable RTEC specifications, including specifications with complex dependencies.
Source: §1 · pp. 2–3Results
Generated MAS specifications achieve high predictive accuracy without compromising reasoning efficiency across protocols with complex hierarchical and cyclic dependencies.
Source: §6 · p. 26Takeaways & Limitations
GenRTEC can be reused in a zero-shot manner to generate executable specifications for any MAS.
Source: §1 · p. 3A fluent-arity discrepancy significantly affected reported F1 scores, making them a pessimistic estimate because maximal intervals remained the same as for hand-crafted specifications.
Source: §5.2.2 · p. 24
Abstract
from arXiv · showhide
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.
1 Introduction
MAS specifications must represent temporal and normative behavior and support executable run-time monitoring, but formal-language expertise and scarce labelled data make them difficult to construct. genRTEC uses pre-trained LLMs to generate RTEC specifications from natural-language descriptions; its evaluation reports high predictive accuracy without compromising reasoning efficiency.
1 Introduction
- MAS specifications must express action effects and temporal or normative conditions, including when actions are permitted, prohibited, or obligatory.The introduction gives deadlines, voting-ballot closure, and repeated unsolicited quotes as examples of temporal constraints.Source: §1 · pp. 1–2
- Executable specifications allow run-time computation of agent-action effects and normative positions, supporting compliance monitoring and possible enforcement.The introduction notes that monitoring should scale to large populations and complex specifications.Source: §1 · p. 2
- Constructing temporal-logic MAS specifications requires formal-language expertise, while specialised machine-learning approaches depend on scarce labelled examples.The examples include labels for norm violations.Source: §1 · p. 2
- GenRTEC uses pre-trained LLMs to translate natural-language descriptions of MAS building blocks into executable specifications in RTEC.RTEC includes optimisation techniques for temporal pattern matching over streaming data.Source: §1 · pp. 2–3
- GenRTEC is evaluated across complex hierarchical and cyclic MAS protocols, with additional temporal specifications generated for four application domains.The evaluation spans e-commerce, voting, and argumentation protocols and includes leading LLMs.Source: §1 · p. 3
- GenRTEC’s generated specifications achieve high predictive accuracy without compromising reasoning efficiency.The evaluation assesses similarity to hand-crafted specifications, predictive accuracy on real and synthetic data, reasoning overhead, and qualitative error classes.Source: §1 · p. 3
2 Related Work
Related work uses the Event Calculus for temporal MAS specifications and describes RTEC as supporting efficient streaming pattern matching, including cyclic dependencies. Other work applies LLMs to executable specifications in different formalisms; genRTEC extends prior RTEC prompting toward domain-agnostic, zero-shot generation with cyclic dependencies.
2 Related Work
- The Event Calculus represents events and actions and reasons about their effects, with inertia, durative phenomena, and hierarchical specifications supporting succinct modelling and optimised reasoning.Prior applications include contract lifecycles, authorisation policies, mobility assistance, health monitoring, and simulations.Source: §2 · p. 4
- RTEC adds windowing and incremental caching for streaming temporal pattern matching and supports cyclic dependencies and delayed actions.The passage reports computational-efficiency advantages over competing systems.Source: §2 · pp. 4–5
- Compared with other stream-reasoning frameworks, RTEC supports relational constraints and locally stratified negation while retaining Event Calculus inertia and durative phenomena.The compared systems include CORE, Ticker, Laser, MeTeoR, and StreamMill.Source: §2 · p. 5
- Earlier LLM work generated BC+ and PDDL specifications or other logic and query forms, but the cited formalisms lack features needed for temporal MAS monitoring.The passage notes BC+ lacks explicit time and PDDL cannot reason over input actions for monitoring MAS.Source: §2 · p. 5
- GenRTEC extends domain-specific RTEC prompting to zero-shot, domain-agnostic specification generation and supports cyclic dependencies.The earlier prompting approach targeted composite maritime activities.Source: §2 · p. 5
3 Background: Run-Time Event Calculus
RTEC represents actions, changing properties, and their effects over time through executable rules. Its syntax defines fluent values and maximal intervals, while its dependency structure supports reasoning over both cyclic and acyclic specifications.
3.1 Syntax
- RTEC represents time, events, and fluents, with predicates for event occurrence, fluent initiation and termination, and values holding at time-points or throughout intervals.A fluent is a property whose value may change over time; time-points are non-negative integers.Source: §3.1 · p. 6, §3 · p. 6
- Statically determined fluents can be computed using union, intersection, and relative complement over maximal-interval lists, though not all simple fluents can be translated into this form.Relative complement removes interval segments covered by specified lists; the ARG example defines an objectionable concession as proper but not timely.Source: §3.1 · pp. 8–9, Figure 1 · p. 8
3.2 Semantics
- The dependency graph links fluent-value pairs when rules refer to them, and cycles are contracted into single vertices before assigning levels.In the ARG example, the cyclic dependencies among proper, objectionable, and premise receive level 2 after contraction.Source: §3.2 · pp. 9–10
3 Background: Run-Time Event Calculus
- RTEC computes maximal intervals for fluent-value pairs, deriving simple fluents from initiation and termination rules and statically determined fluents from interval-based rules.For simple fluents, inertia holds a value after initiation until termination; statically determined fluents are computed from other fluent-value pairs.Source: §3.1 · pp. 6, 8, §3.3 · p. 11
3.3 Reasoning
- RTEC's key reasoning task is to compute maximal intervals for fluent-value pairs, deriving simple-fluent intervals by matching initiations to the first subsequent termination.RTEC may then determine whether a value holds at a time-point by checking membership in those intervals.Source: §3.3 · p. 11
4 Generating Executable Specifications
genRTEC uses prompts to translate natural-language descriptions of MAS components into executable RTEC specifications. Its prompting practices support hierarchical and cyclic dependencies and can produce specifications identical to ground truth.
4 Generating Executable Specifications
- genRTEC addresses the expertise and training-data demands of hand-crafting or learning RTEC specifications by using pre-trained LLMs to generate executable event descriptions.The output is an RTEC event description for a MAS specification.Source: §4 · p. 11
4.1 Prompting Pipeline
- The pipeline first teaches RTEC predicates and rule syntax, then supplies MAS actions and background predicates before requesting rules for each natural-language component.Example descriptions guide mapping into fluents, events, and initiatedAt, terminatedAt, and holdsFor rules.Source: §4.1 · pp. 11–13
- Prompts R and S are reused across MAS, while prompts E, B, and G are customised for each MAS; generation is zero-shot, without feedback.E describes actions, B supplies background predicates, and G requests rules for described components.Source: §4.1 · p. 13, §4.2 · p. 16
4.2 Optimising Performance
- Prompting practices reuse prior output fluents to build hierarchies, state property conditions explicitly, enumerate facets, and warn LLMs early about cycles.The paper reports that hierarchies yield compact event descriptions, enable caching, and improve reasoning efficiency; early cycle warnings address inconsistent rule sets.Source: §4.2 · p. 15
- For the intricate claim-effects and proper-actions examples, genRTEC produced rule sets identical to the ground truth.The authors describe these as “perfect” rule sets.Source: §4.2 · pp. 15–16
5.1 Experimental Setup
The evaluation covers seven MAS applications and compares generated specifications with hand-crafted references using predictive accuracy, syntactic similarity, and reasoning time. The setup uses three LLMs, repeated prompting, and datasets that vary by application.
5.1.1 Applications
- The evaluation covers NET, VP, and ARG protocols, plus MSA, CTM, ACR, and clinical-guideline conformance (CG).The protocols concern negotiation, voting, and argumentation; the additional applications address vessel activity, public transport, activity recognition, and guideline conformance.Source: §5.1.1 · pp. 16–17
5.1.2 Evaluation Metrics
- Generated specifications are assessed by F1-score against ground-truth intervals, syntactic similarity to estimate correction effort, and RTEC reasoning time.Perfect F1 does not necessarily imply perfect syntactic similarity, while perfect syntactic similarity implies perfect F1.Source: §5.1.2 · p. 17
5.1.3 Ground Truth and Datasets
- Hand-crafted ground truths were publicly available for NET, VP, MSA, ACR, and CTM; the authors constructed ARG and CG references, and lacked datasets for both.NET and VP used synthetic interactions; MSA used real vessel signals, CTM used synthetic Helsinki data, and ACR used CAVIAR. ARG used synthetic data, while CG was assessed only for syntactic similarity.Source: §5.1.3 · pp. 18–19
5.1.4 Prompting
- GPT-5, Gemini 2.5 Pro, and Claude Sonnet-4 were each prompted five times per application using default hyperparameters.Examples from MSA were used for prompt S before customised prompts generated specifications for the other applications.Source: §5.1.4 · p. 19
5.2 Experimental Results
Across tested applications, at least one LLM achieved near-perfect predictive accuracy wherever data were available, and top-performing models generally matched ground-truth reasoning complexity. The qualitative analysis found errors with differing effects on similarity, predictive accuracy, and reasoning time.
5.2.1 Quantitative Analysis
- At least one LLM achieved an (almost) perfect F1-score in every application with available data, while top-performing models generally produced ground-truth-comparable complexity.The authors conclude that predictive accuracy need not be sacrificed for efficiency, or vice versa.Source: §5.2.1 · p. 21
- Cyclic dependencies in NET, VP, and ARG did not compromise genRTEC’s performance; prompting about later-defined rule components helped capture them.The prompting practices allowed genRTEC to capture cyclic dependencies in the hand-crafted specifications.Source: §5.2.1 · p. 21
- CG specifications had almost perfect syntactic similarity, but no predictive-accuracy result was available because CG had no dataset.The reported predictive-accuracy comparisons cover applications for which data were available.Source: §5.2.1 · p. 21
5.2.2 Qualitative Analysis
- In ARG, Claude turned a disjunction into a conjunction, realizing concession effects in fewer cases; F1 fell, while reasoning times decreased with shorter premise intervals.The issue affected both syntactic similarity and F1-score.Source: §5.2.2 · p. 22
- Gemini omitted VP’s vote-reset rule, allowing votes to persist into later rounds and potentially affect outcomes; smaller rule-sets also appeared in ARG.The VP omission affected both syntactic similarity and F1-score.Source: §5.2.2 · pp. 22–23
- Fluent-arity errors affected NET, CTM, and CG; in NET, the F1-score understated interval accuracy, while grounding all consumer–merchant combinations substantially increased reasoning time.In CTM, arity errors severely penalized F1 and increased reasoning time; in CG, they slightly reduced similarity without affecting maximal-interval computation.Source: §5.2.2 · p. 24
- Superfluous rules reduced VP similarity without affecting F1 or efficiency much; redundant ACR conditions reduced similarity and slightly increased reasoning times.In ACR, the redundant conditions did not affect maximal-interval computation.Source: §5.2.2 · p. 25
6 Summary and Future Work
genRTEC addresses barriers to hand-crafting and machine-learning-based MAS specification construction. Its generated specifications achieve high predictive accuracy without compromising reasoning efficiency, and the method can be reused zero-shot for any MAS.
6 Summary and Future Work
- genRTEC can be reused zero-shot to generate executable specifications for any MAS.Source: §6 · p. 25
- Hand-crafting MAS specifications requires formal-language knowledge, while automated machine-learning construction requires large labelled datasets that are not always available.Source: §6 · p. 25
- Generated MAS specifications achieve high predictive accuracy without compromising reasoning efficiency across interaction protocols with complex hierarchical and cyclic dependencies.Source: §6 · p. 26
- Future work includes self-revision using compiler feedback and fine-tuning manageable LLMs to avoid errors found in the qualitative analysis.Source: §6 · p. 26
Appendix A Dependency Graphs
The appendix depicts dependency graphs for hand-crafted specifications of MSA, CTM, ACR, and CG; red marks cyclic dependencies.
Appendix A Dependency Graphs
- Red marks cyclic dependencies in the hand-crafted specification graphs for MSA, CTM, ACR, and CG.Source: Figure A1 · p. 32