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.

翻译：IMITATOR4AMAS支持对STCTL进行模型检测及无记忆非完美信息策略的综合，该逻辑在具有异步执行的参数化时间自动机网络上进行解释。作为验证工具IMITATOR的扩展，IMITATOR4AMAS是该领域首个实现策略综合的工具。实验结果表明，相较于现有方法，本工具实现了显著的加速。