Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

8

ATVA
2004
Springer

favoriteEmaildiscussreport

115views Hardware» more ATVA 2004»

First-Order LTL Model Checking Using MDGs

13 years 8 months ago

First-Order LTL Model Checking Using MDGs

Download hvg.ece.concordia.ca

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

Fang Wang, Sofiène Tahar, Otmane Aït M

Real-time Traffic

ATVA 2004 | First-order Linear Time | First-order Temporal Language | Hardware | Many-sorted First-order Ltl |

claim paper

Related Content

» MDGs Reduction Technique Based on the HOL Theorem Prover

» LTL satisfiability checking

» Model Checking for a FirstOrder Temporal Logic Using Multiway Decision Graphs

» Conflict Detection in Call Control Using FirstOrder Logic Model Checking

» Efficient FirstOrder ModelChecking Using Short Labels

» A FirstOrder Policy Language for HistoryBased Transaction Monitoring

» Decidable FirstOrder Transition Logics for PAProcesses

» Validity of FirstOrder Knowledge Bases

» Formal verification of ASMs using MDGs

Post Info
More Details (n/a)

Added	20 Aug 2010
Updated	20 Aug 2010
Type	Conference
Year	2004
Where	ATVA
Authors	Fang Wang, Sofiène Tahar, Otmane Aït Mohamed

Comments (0)