Learning-Based Compositional Parameter Synthesis for Event-Recording Automata

Abstract : We address the verification of timed concurrent systems with unknown or uncertain constants considered as parameters. First, we introduce parametric event-recording automata (PERAs), as a new subclass of parametric timed automata (PTAs). Although in the non-parametric setting event-recording automata yield better decidability results than timed automata, we show that the most common decision problem remains undecidable for PERAs. Then, given one set of components with parameters and one without, we propose a method to compute an abstraction of the non-parametric set of components, so as to improve the verification of reachability properties in the full (parametric) system. We also show that our method can be extended to general PTAs. We implemented our method, which shows promising results.
Type de document :
Communication dans un congrès
Ahmed Bouajjani; Alexandra Silva. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10321, pp.17-32, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_2〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01658415
Contributeur : Hal Ifip <>
Soumis le : jeudi 7 décembre 2017 - 15:48:46
Dernière modification le : jeudi 11 janvier 2018 - 06:17:33

Fichier

 Accès restreint
Fichier visible le : 2020-01-01

Connectez-vous pour demander l'accès au fichier

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Etienne André, Shang-Wei Lin. Learning-Based Compositional Parameter Synthesis for Event-Recording Automata. Ahmed Bouajjani; Alexandra Silva. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. Springer International Publishing, Lecture Notes in Computer Science, LNCS-10321, pp.17-32, 2017, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-319-60225-7_2〉. 〈hal-01658415〉

Partager

Métriques

Consultations de la notice

104