Sciweavers

Share
CAV
1998
Springer

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

12 years 12 days ago
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
Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Core
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where CAV
Authors Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Aït Mohamed
Comments (0)
books