MoGym: Using Formal Models for Training and Verifying Decision-making Agents

Abstract

MoGym, is an integrated toolbox enabling the training and verification of machine-learned decision-making agents based on formal models, for the purpose of sound use in the real world. Given a formal representation of a decision-making problem in the JANI format and a reach-avoid objective, MoGym (a) enables training a decision-making agent with respect to that objective directly on the model using reinforcement learning (RL) techniques, and (b) it supports rigorous assessment of the quality of the induced decision-making agent by means of deep statistical model checking (DSMC). MoGym implements the standard interface for training environments established by OpenAI Gym, thereby connecting to the vast body of existing work in the RL community. In return, it makes accessible the large set of existing JANI model checking benchmarks to machine learning research. It thereby contributes an efficient …

@inproceedings{grosMoGymUsingFormalModels2022,
 author = {Timo P. Gros and Holger Hermanns and Jörg Hoffmann and Michaela Klauck and Maximilian A Köhl and Verena Wolf},
 booktitle = {International Conference on Computer Aided Verification. International Conference on Computer Aided Verification (CAV)},
 doi = {10.1007/978-3-031-13188-2_21},
 isbn = {978-3-031-13188-2},
 organization = {Springer, Cham},
 pages = {430-443},
 publisher = {Springer Cham},
 title = {MoGym: Using Formal Models for Training and Verifying Decision-making Agents},
 year = {2022}
}