Symbolic finite state machines tested and learned using finite input sets
Testing and Learning Symbolic Finite State Machines
Formal Languages and Automata TheorySoftware Engineering
Summary
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.
What this means in practice
- •For software testing teams: Test SFSM-based systems by constructing finite input sets that guarantee coverage of all relevant input conditions.
- •For automata learning engineers: Learn SFSM models from finite data by leveraging finite instantiations and complete testing methods for validation.
Authors
Wen-ling Huang, Jan Peleska
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.