The inductive inference of cyclic synchronized interleaving
Brian J. Ross · 1994
An inductive inference algorithm for inferring cyclic interleaving expressions from homing sequences is presented. The restricted language studied uses a synchronized interleaving or shuffle operator, which is an important component in algebraic theories of concurrency. Expressions of this language denote concurrent perpetual processes that communicate via synchronized handshaking. The paper introduces an algorithm for inferring an interleaved expression from a homing sequence, which is a contiguous, non-resettable trace describing a desired target behaviour. A main component of the algorithm deals with the determination of language terms that are consistent with the homing sequence. Term consistency is modelled via a labelled acyclic digraph. Various orderpreserving properties of interleaving are used to refine this digraph during the inference session. In addition, the digraph permits efficient construction of hypotheses that admit correction by the teacher. The inference algorithm converges to any target expression equivalence class in O(nk ) time and O(k ) space for an alphabet of size k and homing sequence of size n. Given the importance of infinitary cyclic interleaving in concurrency theory, this research shows that machine learning can be tractably applied towards concurrent computations. This may lead to new semi-automated methodologies founded in machine learning technology for synthesizing and testing concurrent and distributed systems.