First-Order LTL Model Checking Using MDGs

In this paper, we describe a first-order linear time temporal logic (LTL) model checker based on multiway decision graphs (MDG). We developed a first-order temporal language, LMDG , which expresses a subset of many-sorted first-order LTL and extends an earlier language, fined for an MDG based abstract CTL model checking. We derived a set of rules, enabling the transformation of LMDG formulas into generalized B

• Type: Conference
• Year: 2004
• Where: ATVA
• Authors: Fang Wang, Sofiène Tahar, Otmane Aït Mohamed
• Keywords: ATVA 2004, First-order Linear Time, First-order Temporal Language, Hardware, Many-sorted First-order Ltl