Homing Sequence Derivation with Quantified Boolean Satisfiability
Abstract—Homing sequence derivation for nondeterministic finite state machines (NFSMs) has important applications in system5testing and verification. Unlike prior methods based on explicit tree-based search, in this article we formulate the derivation of a preset/6adaptive homing sequence in terms of quantified Boolean formula (QBF) solving. This formulation exploits compact circuit7representation of NFSMs and QBF encoding of the existence condition of homing sequence for effective computation. The implicit8circuit representation effectively avoids explicit state enumeration, and can be more scalable. Different encoding schemes and QBF9solvers are evaluated for their suitability for the homing sequence derivation. Experiments on various computation methods and10benchmarks show the generality and feasibility of a proposed approach.