%0 Conference Proceedings
%T Learning-Based Compositional Parameter Synthesis for Event-Recording Automata
%+ Laboratoire d'Informatique de Paris-Nord (LIPN)
%+ Nanyang Technological University [Singapour]
%A André, Etienne
%A Lin, Shang-Wei
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Neuchâtel, Switzerland
%Y Ahmed Bouajjani
%Y Alexandra Silva
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-10321
%P 17-32
%8 2017-06-19
%D 2017
%R 10.1007/978-3-319-60225-7_2
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01658415/document
%2 https://inria.hal.science/hal-01658415/file/446833_1_En_2_Chapter.pdf
%L hal-01658415
%U https://inria.hal.science/hal-01658415
%~ UNIV-PARIS13
%~ CNRS
%~ LIPN
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ USPC
%~ IFIP-FORTE
%~ GALILE
%~ IFIP-LNCS-10321
%~ SORBONNE-PARIS-NORD
%~ CONFRENCE-NATIONALE-SUR-LES-APPLICATIONS-PRATIQUES-DE-LINTELLIGENCE-ARTIFICIELLE
%~ ACT-R