Classification-Based Parameter Synthesis for, Parametric Timed Automata

Abstract

Parametric timed automata are designed to model timed systems with unknown parameters, often representing design uncertainties of external environments. In order to design a robust system, it is crucial to synthesize constraints on the parameters, which guarantee the system behaves according to certain properties. Existing approaches suffer from scalability issues. In this work, we propose to enhance existing approaches through classification-based learning. We sample multiple concrete values for parameters and model check the corresponding non-parametric models. Based on the checking results, we form conjectures on the constraint through classification techniques, which can be subsequently confirmed by existing model checkers for parametric timed automata. In order to limit the number of model checker invocations, we actively identify informative parameter values so as to help the classification converge quickly. We have implemented a prototype and evaluated our idea on 24 benchmark systems. The result shows our approach can synthesize parameter constraints effectively and thus improve parametric verification.