We propose ΛM∗—an active learning algorithm that learns symbolic Mealy automata, which support infinite input alphabets and multiple output characters. Each of these two features has been addressed separately in prior work. Combining these two features poses a challenge in learning the outputs corresponding to potentially infinite sets of input characters at each state. To address this challenge, we introduce the notion of essential input characters, a finite set of input characters that is sufficient to learn the output function of a symbolic Mealy automaton. ΛM∗ maintains an underapproximation of the essential input characters and refines this set during learning. We prove that ΛM∗ terminates under certain assumptions. Moreover, we provide upper and lower bounds for the query complexity. Their similarity suggests the tightness of the bounds. We empirically demonstrate that ΛM∗ is i) efficient regarding the number of queries on practical benchmarks and ii) scalable according to evaluations with randomly generated benchmarks. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

Cyber-physical systems (CPSs) often contain components whose internal design is unknown, making their verification challenging. Although black-box checking (BBC)—an automated black-box testing method that combines automata learning and model checking—can detect unsafe behaviors without requiring a complete model, it becomes computationally expensive for large or infinite-state systems. To address this problem, we propose a specification-guided abstraction that identifies and merges states in the system’s state space if they are equivalent under the verified specifications. Building on this abstraction, we develop an algorithm that directly learns the resulting abstract Mealy machine, thereby bypassing the need to learn the full system behavior first. We then integrate the new learning procedure with model checking to obtain an enhanced BBC framework that efficiently handles large or infinite-state systems, particularly when verifying multiple properties. Our empirical evaluation demonstrates that specification-guided abstraction improves detection and efficiency in uncovering unsafe behaviors in CPSs. © 2025 Copyright held by the owner/author(s).