Learning Event-recording Automata Passively

Learning models for real-time systems is an active area of research. Timed Automata (TA) is a popular model for real-time systems. Learning TA being a difficult problem, several works have been dedicated to learning different subclasses of TA. Event-recording Automata (ERA) is a well-studied, determinizable subclass of TA. In this talk, we will illustrate a state-merging algorithm -- called LEAP -- designed to learn timed languages definable by ERA. We adapt the classical framework of RPNI -- a passive learning algorithm for inferring deterministic fininite-state automata for regular languages -- to the timed setting. As inputs, we consider a set of positive and a set of negative symbolic words. Symbolic words are a natural formalism for specifying requirements by a human user. The objective is to construct an ERA that accepts every timed word that satisfies a positive symbolic word and rejects every timed word that satisfies a negative symbolic word. We show that, during the execution of the state-merging algorithm, determining when merging of two states is allowed, is an NP-complete problem -- which we solve by encoding it as an SMT formula. We conclude by showing that for every timed language L definable by an ERA, there exists a set of positive and negative symbolic words -- generally referred to as the characteristic set -- such that, whenever these words are provided as input, LEAP constructs an ERA whose language is L. This is a joint work with Anirban Majumdar and Jean-François Raskin.

Authors

• Sayan Mukherjee

Keywords

No keywords are indexed for this paper.