IMITATOR4AMAS: Strategy Synthesis for STCTL
Davide Catta, Adrien Lacroix, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
TL;DR
IMITATOR4AMAS is a novel tool that enables the synthesis of strategies with imperfect information for networks of parametric timed automata, significantly improving efficiency over previous methods.
Contribution
It introduces the first strategy synthesis tool for STCTL over networks of parametric timed automata with asynchronous execution.
Findings
Substantial speedup over previous approaches
Supports model checking and synthesis of memoryless strategies
First tool for this specific setting
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Machine Learning and Algorithms · Model-Driven Software Engineering Techniques