Papers for

automata learning engineers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Symbolic finite state machines tested and learned using finite input sets

Testing and Learning Symbolic Finite State Machines

Abstract: Symbolic finite state machines (SFSMs) describe input/output behaviour using guards and output assignments with possibly infinite data domains. We study deterministic and completely specified SFSMs whose guards and output assignments depend only on the current input. We define finite representative input sets that contain witnesses for relevant guard overlaps and separating witnesses for output assignments that differ on those overlaps. Our main theorem shows that language equivalence of the finite instantiations implies language equivalence over the full input domain. This result transfers complete testing methods for deterministic finite state machines (DFSMs) to SFSMs, provided finite sets of admissible guards and output assignments and an upper bound on the number of distinguishable reachable states are known. Under these assumptions, a DFSM learner with complete testing can learn a finite instantiation, which is then lifted to an equivalent SFSM. We establish a bound on the size of representative input sets and give an SMT construction whose correctness and termination hold under stated solver assumptions.

Tue 22 SeptFormal Languages and Automata TheorySoftware Engineering
The gist
Testing and learning systems that handle inputs with infinite possibilities is tricky. This work focuses on symbolic finite state machines (SFSMs), which are models using symbolic conditions and outputs rather than fixed values. The authors show that by carefully choosing a finite set of representative inputs, one can test and learn SFSMs as effectively as traditional finite state machines. This approach helps build and verify these machines without needing to explore every possible input individually.
Open → 2609.25603v1