Máy trạng thái trừu tượng
Trong khoa học máy tính, một máy trạng thái trừu tượng (MTT) (hay trong tiếng Anh: Abstract State Machine - ASM) là một máy trạng thái trong đó, số lượng các trạng thái không nhất thiết là hữu hạn và các trạng thái không chỉ đơn thuần là các điểm trong không gian trạng thái. Chính xác hơn, một trạng thái của máy trạng thái trừu tượng là một cấu trúc, theo cách hiểu của toán logic, là một tập hợp không rỗng các phần tử cùng với một số hàm số (toán tử) và các quan hệ trên tập đó. (Các cấu trúc có thể được xem như các đại số, điều này giải thích tên ban đầu của MTT là các đại số tiến hóa). Trong khái niệm ban đầu của máy trạng thái tổng quát, một tác tử (agent) thực hiện một chương trình theo các bước, có thể tương tác với môi trường. Khái niệm này đã được mở rộng để có thể thực hiện các tính toán phân tán, trong đó các tác tử thực hiện các chương trình đồng thời.
Khái niệm về Máy trạng thái trừu tượng được đưa ra bởi Yuri Gurevich, người đầu tiên đề xuất ý tưởng này vào giữa nhưng năm 80 như là một cách để cải thiện các luận điểm của Church rằng bất kỳ một giải thuật nào cũng đều có thể mô phỏng bởi một máy Turing tương ứng. Yuri Gurevich đã đưa ra "Luận đề về máy trạng thái trừu tượng" như sau: các giải thuật, dù trừu tượng ở mức độ nào, cũng đều có thể được thực hiện bởi một Máy trạng thái trừu tượng tương ứng. Năm 2000, Gurevich tiên đề hóa khái niệm về giải thuật tuần tự, và đã chứng minh các luận đề về máy trạng thái trừu tượng cho hệ tiên đề đó. Đại khái, hệ tiên đề này bao gồm: các trạng thái là các cấu trúc, việc chuyển trạng thái chỉ nằm trong một số lượng giới hạn các trạng thái nào đó.
MTT được sử dụng trong đặc tả hình thức của phần cứng máy tính và phần mềm. Egon Börger đã tham gia vào quá trình ứng dụng MTT trong thiết kế và kiểm định phần cứng và phần mềm. Ông cũng là người đầu tiên đề xuất các ứng dụng trong công nghệ phần mềm. Bởi vì các mô hình giải thuật MTT, ở một mức độ trừu tượng nào đó, có thể đưa ra một cái nhìn về thiết kế phần cứng và phần mềm ở các cấp độ từ thấp, trung bình đến cao. Các đặc tả MTT thường bao gồm một tập các mô hình MTT, bắt đầu ở các tầng trừu tượng cơ sở, sau đó phát triển dần lên các tầng cao hơn, chi tiết và tinh xảo hơn. Các đặc tả MTT đã được phát triển bao gồm các ngôn ngữ lập trình (Prolog, C, và Java) và các ngôn ngữ thiết kế (UML và SDL). Hiện nay, có một số các phần mềm cho phép thực thi và phần tích máy tổng quát trừu tượng.
Tham khảo[sửa | sửa mã nguồn]
- Y. Gurevich, Evolving Algebras 1993: Lipari Guide, E. Börger (ed.), Specification and Validation Methods, Oxford University Press, 1995, 9-36. (ISBN 0-198-53854-5)
- E. Börger and R. Stärk, Abstract State Machines: A Method for High-Level System Design and Analysis, Springer-Verlag, 2003. (ISBN 3-540-00702-4)
- R. Stärk, J. Schmid and E. Börger, Java and the Java Virtual Machine: Definition, Verification, Validation, Springer-Verlag, 2001. (ISBN 3-540-42088-6)
- Y. Gurevich, Sequential Abstract State Machines capture Sequential Algorithms, ACM Transactions on Computational Logic 1(1) (tháng 7 năm 2000), 77-111.