符号有限状态机的测试与学习

中文摘要 AI 辅助

符号有限状态机（SFSMs）使用守卫和输出赋值来描述输入/输出行为，这些守卫和输出赋值可能涉及无限的数据域。我们研究确定性的且完全指定的SFSMs，其守卫和输出赋值仅依赖于当前输入。我们定义了有限的代表性输入集，其中包含相关守卫重叠的见证，以及在这些重叠上输出赋值不同的分离见证。我们的主要定理表明，有限实例的语言等价性蕴含整个输入域上的语言等价性。这一结果将确定性有限状态机（DFSMs）的完整测试方法转移到SFSMs，前提是已知有限的允许守卫和输出赋值集合以及可区分可达状态数量的上界。在这些假设下，具有完整测试能力的DFSM学习器可以学习一个有限实例，然后将其提升为等价的SFSM。我们建立了代表性输入集大小的界限，并给出了一个SMT构造，其正确性和终止性在所述求解器假设下成立。

英文摘要

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.

发表机构

• University of Bremen（不来梅大学）

机构由 AI 辅助整理，请以论文原文为准。