Towards First-Order Symbolic Trajectory Evaluation

Symbolic trajectory evaluation (STE) is a symbolic simulation based bounded model checking approach and its computational complexity depends only on the property being checked not on the size of the circuit. In this paper, we study first-order symbolic trajectory evaluation (FSTE). We first present the computation model: abstract state machines (ASMs) combined with a partial order over the state space, in which data and data operations are described using abstract sort and uninterpreted function symbols. Second, we devise an FSTE algorithm which is based on implicit state enumeration of an ASM and implemented using multiway decision graphs (MDGs). Finally, an illustrative example is presented to demonstrate the effectiveness of this approach.