Model checking for a first-order temporal logic using multiway decision graphs

We study model checking for a first-order linear-time temporal logic. The computation model is based on Abstract State Machines (ASMs) in which data and data operations are described using abstract sorts and uninterpreted function symbols. ASMs are suitable for describing Register-Transfer level designs. We then define a first-order linear time temporal logic called L-MDG which supports the abstract data representations. Both safety and liveness properties can be expressed in L-MDG, however, only universal path quantification is possible. Fairness constraints can also be imposed. The property checking algorithms are based on implicit state enumeration of an ASM and implemented using Multiway Decision Graphs.