Inductive temporal formula specifications

Design verification has played an important role in the design of large scale and complex systems. In this article, we focus on model checking methods. Behaviors of modeled systems are in general specified in terms of temporal formulas of computation tree logic and users must have enough knowledge of temporal specification because the specification might be complex. We propose a method through which temporal formulas are obtained inductively and amounts of required memory and time are reduced. We will show verification results which are obtained by the proposed method.