This paper presents a state-merging algorithm for learning timed languages definable by Event-Recording Automata (ERA) using positive and negative samples in the form of symbolic timed words. Our algorithm, LEAP (Learning Event-recording Automata Passively), constructs a possibly nondeterministic ERA from such samples based on merging techniques. We prove that determining whether two ERA states can be merged while preserving sample consistency is an NP-complete problem, and address this with a practical SMT-based solution. Our implementation demonstrates the algorithm’s effectiveness through examples. We also show that every ERA-definable language can be inferred using our algorithm with a suitable sample.
Tue 28 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
Tue 28 Oct
Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
11:00 - 12:30 | |||
11:00 30mPaper | Componentwise Automata Learning for System IntegrationDistinguished Paper ATVA Papers Hiroya Fujinami , Masaki Waga Kyoto University, Jie An Institute of Software Chinese Academy of Sciences, Kohei Suenaga Graduate School of Informatics, Kyoto University, Nayuta Yanagisawa , Hiroki Iseri NPO ASTER Minato-ku, Tokyo, Ichiro Hasuo National Institute of Informatics, Japan | ||
11:30 30mPaper | Learning Event-recording Automata Passively ATVA Papers Anirban Majumdar , Sayan Mukherjee Univ Rennes, Inria, CNRS, IRISA, France, Jean-François Raskin Université Libre de Bruxelles | ||
12:00 15mPaper | TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets (tool paper) ATVA Papers Bruno Maria René Gonzalez TU Berlin, Germany, Peter Gjøl Jensen Aalborg University, Denmark, Jiri Srba , Stefan Schmid TU Berlin, Germany, Martin Zimmermann University of Liverpool | ||