Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs

bstract description of state machines (ASMs), in which data and data operations are d using abstract sort and uninterpreted function symbols. ASMs are suitable for describing RegisterTransferleveldesigns. Wedefineafirst-orderlinear-timetemporallogiccalledLMDG which the abstract data representations. Both safety and liveness properties can be expressed in LMDG, 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. Received 26 March 2002; revised 20 June 2003

• Type: Conference
• Year: 1998
• Where: CAV
• Authors: Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Aït Mohamed
• Keywords: Abstract Data Representations, CAV 1998, Hardware, Uninterpreted Function Symbols, Universal Path Quantification