IMITATOR4AMAS: Strategy Synthesis for STCTL

arXiv (Cornell University) 2026 Preprint Open access

Read full text
Authors: Davide Catta, Adrien Lacroix, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
DOI: 10.48550/arxiv.2602.10810
Cited by: 0

Abstract

IMITATOR4AMAS supports model checking and synthesis of memoryless imperfect information strategies for STCTL, interpreted over networks of parametric timed automata with asynchronous execution. While extending the verifier IMITATOR, IMITATOR4AMAS is the first tool for strategy synthesis in this setting. Our experimental results show a substantial speedup over previous approaches.

Fields of Study & Subjects

Formal Methods in Verification Petri Nets in System Modeling Logic programming and type systems

Publication details

Journal / source
arXiv (Cornell University)
Publication date
11 February 2026
Language
EN
Document type
Preprint