Invention Grant
- Patent Title: Efficient approaches for bounded model checking
- Patent Title (中): 有限模型检查的有效方法
-
Application No.: US10157486Application Date: 2002-05-30
-
Publication No.: US07711525B2Publication Date: 2010-05-04
- Inventor: Malay Ganai , Lintao Zhang , Aarti Gupta , Zijiang Yang , Pranav Ashar
- Applicant: Malay Ganai , Lintao Zhang , Aarti Gupta , Zijiang Yang , Pranav Ashar
- Applicant Address: JP Tokyo
- Assignee: NEC Corporation
- Current Assignee: NEC Corporation
- Current Assignee Address: JP Tokyo
- Agency: Sughrue Mion, PLLC
- Main IPC: G06F17/10
- IPC: G06F17/10
Abstract:
A method for bounded model checking of arbitrary Linear Time Logic temporal properties. The method comprises translating properties associated with temporal operators F(p), G(p), U(p, q) and X(p) into property checking schemas comprising Boolean satisfiability checks, wherein F represents an eventuality operator, G represents a globally operator, U represents an until operator and X represents a next-time operator. The overall property is checked in a customized manner by repeated invocations of the property checking schemas for F(p), G(p), U(p, q), X(p) operators and standard handling of atomic propositions and Boolean operators.
Public/Granted literature
- US20030225552A1 Efficient approaches for bounded model checking Public/Granted day:2003-12-04
Information query
