Automata trên các đối tượng vô hạn

Automata trên các đối tượng vô hạn đọc các đầu vào không bao giờ kết thúc, chẳng hạn như các từ vô hạn hoặc cây vô hạn, và chấp nhận dựa trên việc các trạng thái hoặc chuyển đổi nào được truy cập vô hạn lần, cung cấp bộ máy toán học để lý luận về các hệ thống đang diễn ra, không kết thúc.

Definition

Một omega-automaton là một máy trạng thái hữu hạn có các lần chạy là vô hạn, với sự chấp nhận được định nghĩa bởi một điều kiện trên tập hợp các trạng thái được truy cập vô hạn lần; các automata như vậy nhận dạng các tập hợp các từ hoặc cây vô hạn được gọi là ngôn ngữ omega-regular.

Scope

Chủ đề này bao gồm các automata Büchi, Muller, Rabin và parity trên các từ vô hạn, các điều kiện chấp nhận phân biệt chúng, kết quả xác định và bổ sung, automata trên cây vô hạn, và các kết nối sâu sắc giữa các automata này, logic bậc hai đơn nguyên và các trò chơi vô hạn được sử dụng trong tổng hợp và xác minh.

Core questions

• Làm thế nào một máy hữu hạn có thể chấp nhận hoặc từ chối một đầu vào không có điểm kết thúc?
• Tại sao automata Büchi không xác định và xác định lại khác nhau về sức mạnh biểu cảm?
• Automata trên các đối tượng vô hạn liên quan như thế nào đến các logic để chỉ định hành vi hệ thống?
• Điều gì làm cho việc bổ sung các automata này trở nên khó khăn, và tại sao điều đó lại quan trọng?

Key theories

Chấp nhận Büchi và ngôn ngữ omega-regular

Một automaton Büchi chấp nhận một từ vô hạn khi một trạng thái chấp nhận nào đó được truy cập vô hạn lần, và các ngôn ngữ được nhận dạng như vậy, các ngôn ngữ omega-regular, trùng khớp với những ngôn ngữ có thể định nghĩa trong logic bậc hai đơn nguyên trên các số tự nhiên.

Xác định và điều kiện parity

Automata Büchi không xác định nói chung không thể được làm cho xác định mà không thay đổi điều kiện chấp nhận, nhưng cấu trúc của Safra chuyển đổi chúng thành automata Rabin hoặc parity xác định, điều này rất cần thiết cho việc bổ sung và giải quyết các trò chơi.

Clinical relevance

Omega-automata là xương sống thuật toán của kiểm tra mô hình: một hệ thống phản ứng và một thuộc tính logic thời gian đều được dịch thành automata trên các từ vô hạn, và việc kiểm tra thuộc tính giảm xuống thành một phép thử rỗng, cho phép xác minh tự động phần cứng, giao thức và phần mềm đồng thời.

History

Büchi đã giới thiệu automata trên các từ vô hạn vào khoảng năm 1960 để quyết định lý thuyết bậc hai đơn nguyên của các số tự nhiên, McNaughton đã chỉ ra cách xác định chúng với các điều kiện chấp nhận mạnh hơn, và Rabin đã mở rộng lý thuyết sang cây vô hạn, những kết quả này trở nên trung tâm cho việc xác minh sau khi logic thời gian đi vào khoa học máy tính vào cuối những năm 1970.

Key figures

• J. Richard Büchi
• Robert McNaughton
• Michael Rabin
• Shmuel Safra

Seminal works

• thomas1990
• graedel2002

Frequently asked questions

Làm thế nào một máy có thể chấp nhận một đầu vào vô hạn?

Sự chấp nhận không được định nghĩa bằng cách đạt đến trạng thái cuối cùng ở cuối, vì không có điểm cuối, mà bằng cách các trạng thái nào lặp lại. Ví dụ, một automaton Büchi chấp nhận khi nó đi qua một trạng thái chấp nhận được chỉ định vô hạn lần trong quá trình chạy không ngừng của nó.

Tại sao các automata này quan trọng đối với việc xác minh?

Các hệ thống không kết thúc như hệ điều hành và giao thức mạng được mô hình hóa một cách tự nhiên bằng các hành vi vô hạn. Các thuộc tính như "hệ thống không bao giờ bị tắc nghẽn" hoặc "mọi yêu cầu cuối cùng đều được phục vụ" trở thành các ngôn ngữ omega-regular, vì vậy việc kiểm tra chúng giảm xuống các hoạt động automata mà một trình kiểm tra mô hình có thể thực hiện tự động.