TAILIEUCHUNG - Báo cáo khoa học: "A semantically-derived subset of English for hardware verification"

To verify hardware designs by model checking, circuit specifications are commonly expressed in the temporal logic CTL. Automatic conversion of English to CTL requires the definition of an appropriately restricted subset of English. We show how the limited semantic expressibility of CTL can be exploited to derive a hierarchy of subsets. Our strategy avoids potential difficulties with approaches that take existing computational semantic analyses of English as their starting point--such as the need to ensure that all sentences in the subset possess a CTL translation. . | A semantically-derived subset of English for hardware verification Alexander Holt and Ewan Klein HCRC Language Technology Group Division of Informatics University of Edinburgh Abstract To verify hardware designs by model checking circuit specifications are commonly expressed in the temporal logic CTL. Automatic conversion of English to CTL requires the definition of an appropriately restricted subset of English. We show how the limited semantic expressibility of CTL can be exploited to derive a hierarchy of subsets. Our strategy avoids potential difficulties with approaches that take existing computational semantic analyses of English as their starting point such as the need to ensure that all sentences in the subset possess a CTL translation. 1 Specifications in Natural Language Mechanised formal specification and verification tools can significantly aid system design in both software and hardware Clarke and Wing 1996 . One well-established approach to verification particularly of hardware and protocols is temporal model checking which allows the designer to check that certain desired properties hold of the system Clarke and Emerson 1981 . In this approach specifications are expressed in a temporal logic and systems are represented as finite state transition An efficient search method determines whether the desired property is true in the model provided by the transition system if not it provides a counterexample. Despite the undoubted success of temporal model checking as a technique the requirement that specifications be expressed in temporal logic has proved an obstacle to its take-up by circuit designers and therefore alternative interfaces involving graphics and natural language have been explored. In this paper we address some of the challenges raised by converting 1 In practice it turns out to be preferable to use a symbolic representation of the state model thereby avoiding the state explosion problem .

• Báo cáo khoa học
• A semantically derived subset
• English for hardware verification
• Alexander Holt and Ewan Klein
• báo cáo khoa học
• mô hình ngôn ngữ
• xử lý ngôn ngữ tự nhiên
• Bài giảng Xử lý ngôn ngữ tự nhiên
• Ngôn ngữ tự nhiên
• Kỹ thuật lập trình
• Xử lý nhập nhằng ngữ nghĩa
• Xử lý ngữ nghĩa
• Xử lý ngôn ngữ
• Natural Language Processing
• Ngôn ngữ lập trình
• Nhập nhằng cấu trúc
• Tri thức về ngôn ngữ
• Mô hình n gram
• Dịch máy
• Phương pháp dịch máy
• Hiểu ngôn ngữ
• Phân tích ngữ nghĩa
• Phân loại tin tự động
• Biểu diễn vị từ
• Thuộc tính về sự kiện
• Thuộc tính về sự kiện
• Mô hình ngôn ngữ Google Book N grams
• Mô hình ngôn ngữ KenLM
• Phương pháp làm mịn
• Tách từ tiếng Việt
• Gán nhãn từ loại
• Phân tích cú pháp
• Nghĩa từ vựng
• Phân giải nhập nhằng từ
• Phân loại văn bản
• Lexical chain
• Phản hồi thông tin
• Bài toán PTCP
• Cấu trúc ngữ pháp
• Phân tích cú pháp xác suất
• CKY kết hợp xác suất
• Văn phạm phi ngữ cảnh xác suất
• Hình thái học