Logic Thời Gian và Logic Hình Thái trong Tính Toán

Logic thời gian và hình thái mở rộng logic cổ điển bằng các toán tử cho thời gian và khả năng, cung cấp các ngôn ngữ chính xác để xác định cách một chương trình hoặc hệ thống phản ứng phải hoạt động trong suốt quá trình thực thi của nó.

Definition

Logic thời gian bổ sung cho logic mệnh đề hoặc logic bậc nhất bằng các toán tử mô tả khi nào các thuộc tính được giữ vững trong một tính toán, chẳng hạn như luôn luôn, cuối cùng, và cho đến khi; logic hình thái tổng quát hóa điều này bằng các toán tử cho sự cần thiết và khả năng trên một cấu trúc các trạng thái và chuyển đổi.

Scope

Chủ đề này bao gồm logic thời gian tuyến tính và thời gian phân nhánh như LTL và CTL, các logic hình thái bao gồm logic động và phép tính mu-hình thái, biểu diễn các thuộc tính an toàn và sống còn, và các vấn đề thuật toán của kiểm tra mô hình và tính thỏa mãn làm cho các logic này trở thành trung tâm của xác minh tự động.

Core questions

• Làm thế nào một logic có thể diễn đạt rằng một điều tốt cuối cùng sẽ xảy ra hoặc một điều xấu sẽ không bao giờ xảy ra?
• Sự khác biệt giữa việc lập luận về một lần thực thi và về tất cả các tương lai có thể là gì?
• Làm thế nào để việc kiểm tra xem một hệ thống có thỏa mãn một thuộc tính thời gian được thực hiện theo thuật toán?
• Những logic thời gian nào cân bằng giữa sức mạnh biểu cảm và xác minh hiệu quả?

Key theories

Logic thời gian cho đặc tả chương trình

Pnueli đã chỉ ra rằng logic thời gian nắm bắt tính đúng đắn của các chương trình phản ứng và đồng thời bằng cách diễn đạt các thuộc tính trên các lần thực thi của chúng, cung cấp một ngôn ngữ thống nhất cho các yêu cầu an toàn và sống còn.

Kiểm tra mô hình logic thời gian phân nhánh

Clarke và Emerson đã giới thiệu logic cây tính toán và một thuật toán để tự động xác minh nó dựa trên một mô hình trạng thái hữu hạn, đặt nền móng cho lĩnh vực kiểm tra mô hình.

Clinical relevance

Các logic thời gian là ngôn ngữ đặc tả của các bộ kiểm tra mô hình được sử dụng thường xuyên để xác minh thiết kế phần cứng, giao thức truyền thông và phần mềm đồng thời, phát hiện các bế tắc và vi phạm an toàn và sống còn trước khi triển khai; công nghệ này đã mang lại Giải thưởng Turing cho những người khởi xướng và là tiêu chuẩn trong thiết kế chip.

History

Pnueli đã đề xuất logic thời gian để lập luận về các chương trình vào năm 1977, và Clarke và Emerson, cùng với Queille và Sifakis một cách độc lập, đã phát triển kiểm tra mô hình vào khoảng năm 1981. Phương pháp này đã mở rộng sang các hệ thống công nghiệp thông qua các phương pháp ký hiệu vào đầu những năm 1990, và những người tạo ra nó đã nhận Giải thưởng Turing cho kỹ thuật này.

Key figures

• Amir Pnueli
• Edmund Clarke
• E. Allen Emerson
• Joseph Sifakis

Seminal works

• clarkeEmerson1981
• huthRyan2004

Frequently asked questions

Sự khác biệt giữa logic thời gian tuyến tính và thời gian phân nhánh là gì?

Các logic thời gian tuyến tính như LTL mô tả các thuộc tính của một đường dẫn thực thi duy nhất, có thể vô hạn. Các logic thời gian phân nhánh như CTL định lượng trên cây của tất cả các tương lai có thể từ mỗi trạng thái, cho phép người ta nói rằng dọc theo một số đường dẫn hoặc dọc theo tất cả các đường dẫn một thuộc tính được giữ vững. Chúng có sức mạnh biểu cảm và thuật toán xác minh khác nhau.

Kiểm tra mô hình sử dụng các logic này như thế nào?

Một hệ thống được biểu diễn dưới dạng mô hình trạng thái hữu hạn và một thuộc tính mong muốn dưới dạng công thức logic thời gian. Một bộ kiểm tra mô hình khám phá cạn kiệt các trạng thái để xác định xem công thức có đúng hay không, và nếu nó thất bại, nó sẽ tạo ra một dấu vết phản ví dụ, làm cho việc xác minh vừa tự động vừa có tính chẩn đoán.