LTL Verification of Memoryful Neural Agents
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917944968085504 |
|---|---|
| author | Hosseini, Mehran Lomuscio, Alessio Paoletti, Nicola |
| author_facet | Hosseini, Mehran Lomuscio, Alessio Paoletti, Nicola |
| contents | We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable environment. Examples of MN-MAS include multi-agent systems based on feed-forward and recurrent neural networks or state-space models. Different from previous approaches, we support the verification of both bounded and unbounded LTL specifications. We leverage well-established bounded model checking techniques, including lasso search and invariant synthesis, to reduce the verification problem to that of constraint solving. To solve these constraints, we develop efficient methods based on bound propagation, mixed-integer linear programming, and adaptive splitting. We evaluate the effectiveness of our algorithms in single and multi-agent environments from the Gymnasium and PettingZoo libraries, verifying unbounded specifications for the first time and improving the verification time for bounded specifications by an order of magnitude compared to the SoA. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_02512 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | LTL Verification of Memoryful Neural Agents Hosseini, Mehran Lomuscio, Alessio Paoletti, Nicola Logic in Computer Science Artificial Intelligence Machine Learning Multiagent Systems Symbolic Computation 68Q60 (Primary) 68T27, 68T07, 68T37, 68T40, 68T42 (Secondary) D.2.4; F.3.1; I.2.4; I.2.11; I.2.8; F.4.1; I.2.2; I.2.3 We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable environment. Examples of MN-MAS include multi-agent systems based on feed-forward and recurrent neural networks or state-space models. Different from previous approaches, we support the verification of both bounded and unbounded LTL specifications. We leverage well-established bounded model checking techniques, including lasso search and invariant synthesis, to reduce the verification problem to that of constraint solving. To solve these constraints, we develop efficient methods based on bound propagation, mixed-integer linear programming, and adaptive splitting. We evaluate the effectiveness of our algorithms in single and multi-agent environments from the Gymnasium and PettingZoo libraries, verifying unbounded specifications for the first time and improving the verification time for bounded specifications by an order of magnitude compared to the SoA. |
| title | LTL Verification of Memoryful Neural Agents |
| topic | Logic in Computer Science Artificial Intelligence Machine Learning Multiagent Systems Symbolic Computation 68Q60 (Primary) 68T27, 68T07, 68T37, 68T40, 68T42 (Secondary) D.2.4; F.3.1; I.2.4; I.2.11; I.2.8; F.4.1; I.2.2; I.2.3 |
| url | https://arxiv.org/abs/2503.02512 |