Luận án tiến sĩ: Đại số khoảng, otomat khoảng và ứng dụng của Bùi Vũ Anh - ĐHQG Hà Nội

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC KHOA HỌC TỰ NHIÊN ??????? BÙI VŨ ANH ĐẠI SỐ KHOẢNG, OTOMAT KHOẢNG VÀ MỘT SỐ ỨNG DỤNG LUẬN ÁN TIẾN SĨ TOÁN HỌC Hà Nội - 2015 z ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC KHOA HỌC TỰ NHIÊN ??????? BÙI VŨ ANH ĐẠI SỐ KHOẢNG, OTOMAT KHOẢNG VÀ MỘT SỐ ỨNG DỤNG Chuyên ngành : Bảo đảm Toán học cho máy tính và hệ thống tính toán Mã số : 62 46 35 01 LUẬN ÁN TIẾN SĨ TOÁN HỌC NGƯỜI HƯỚNG DẪN KHOA HỌC: 1. TS Phan Trung Huy 2. TS Nguyễn Thị Hồng Minh XÁC NHẬN CỦA ĐẠI DIỆN XÁC NHẬN CỦA CÁN BỘ HƯỚNG DẪN CHỦ TỊCH HỘI ĐỒNG TS NGUYỄN THỊ HỒNG MINH GS. TSKH PHẠM KỲ ANH Hà Nội - 2015 z LỜI CAM ĐOAN Tôi xin cam đoan đây là công trình nghiên cứu của riêng tôi dưới sự hướng dẫn của cố PGS.

TS Phan Trung Huy, Viện Toán ứng dụng và Tin học - Trường Đại học Bách Khoa Hà Nội và TS Nguyễn Thị Hồng Minh, Khoa Sau đại học - Đại học Quốc gia Hà Nội. Các số liệu, kết quả nêu trong luận án là trung thực và chưa từng được ai công bố trong bất kỳ công trình nào khác. Hà nội, ngày 15 tháng 5 năm 2015 Tác giả luận án Bùi Vũ Anh 1 z LỜI CẢM ƠN Lời đầu tiên, tôi xin cảm ơn thầy hướng dẫn chính, cố PGS. TS PHAN TRUNG HUY - Viện Toán ứng dụng và Tin học, Trường ĐH Bách Khoa Hà Nội, người đã tận tình hướng dẫn và tạo điều kiện cho tôi trong quá trình làm luận án.

Thầy đã giúp tôi có được phương pháp tư duy khoa học, giúp tôi có được khả năng tự tìm tòi, trao đổi và học hỏi trong quá trình làm nghiên cứu. Tôi cũng xin cảm ơn cô giáo hướng dẫn, TS NGUYỄN THỊ HỒNG MINH - Khoa Sau đại học, ĐHQG Hà Nội, người đã luôn trao đổi với tôi những ý tưởng trong nghiên cứu, động viên chia sẻ với tôi trước những khó khăn trong chuyên môn cũng như trong cuộc sống. Tôi xin gửi lời cảm ơn tới các thầy cô trong Khoa Toán - Cơ - Tin học đã giảng dạy và giúp đỡ tôi trong thời gian học tập tại Khoa từ khi học đại học đến nay. Cảm ơn các đồng nghiệp trong Bộ môn Tin học, Khoa Toán - Cơ - Tin học, Trung tâm tính toán hiệu năng cao thuộc Trường ĐH Khoa học Tự nhiên đã tạo điều kiện thuận lợi để tôi hoàn thành luận án; cảm ơn Ban chủ nhiệm Khoa Toán - Cơ - Tin học, phòng Sau đại học, Ban Giám hiệu Trường ĐH Khoa học Tự nhiên đã giúp đỡ tôi trong các thủ tục bảo vệ.

Tôi xin cảm ơn các thầy cô, các anh chị và các bạn trong seminar Cơ sở Toán học cho Tin học - Viện Toán học và Bộ môn Toán tin, Viện Toán ứng dụng và Tin học - Trường ĐH Bách Khoa Hà Nội đã tạo điều kiện để tôi trao đổi các kết quả nghiên cứu, cho tôi những nhận xét thiết thực, có ý nghĩa. Tôi cũng xin được cảm ơn các thầy cô trong Hội đồng đánh giá luận án cấp cơ sở, các phản biện kín và các anh chị em đã giúp tôi đọc, góp các ý kiến để tôi hoàn thiện luận án. Tôi cũng cảm ơn gia đình và bạn bè đã cổ vũ, động viên tôi trong suốt quá trình làm luận án. Đặc biệt, con xin được bày tỏ lòng biết ơn bố mẹ, những người đã sinh thành, dưỡng dục, động viên con trong cuộc sống và nhất là trong thời gian làm nghiên cứu sinh.

Cảm ơn con gái và con trai cưng của bố. Các con là niềm vui, là nguồn động lực cho bố. Cảm ơn vợ và các em đã luôn đồng hành cùng anh. Hà Nội, ngày 15 tháng 5 năm 2015 Nghiên cứu sinh Bùi Vũ Anh 2 z Mục lục Lời cam đoan.

2 Danh mục từ viết tắt. 5 Danh sách hình vẽ. Các cách tiếp cận theo hướng otomat. Các cách tiếp cận theo hướng đại số.

Mục tiêu của luận án. Các kết quả chính của luận án. Cấu trúc của luận án. Một số khái niệm cơ sở.

Quan hệ hai ngôi. Nửa nhóm, vị nhóm. Từ và ngôn ngữ. Otomat hữu hạn.

Otomat hữu hạn đơn định. Mối quan hệ giữa otomat đơn định và đa định. Bài toán xác định ngôn ngữ. Otomat tối tiểu.

Cấu trúc đại số khoảng. Đại số khoảng. Quan hệ thứ tự trên khoảng. Giao thức chứng thực Zero-Knowledge.

Ví dụ về giao thức Zero-Knowledge. Hệ thống Zero-Knowledge dùng tích khoảng. Giao thức Zero-Knowledge kiểm chứng một phía. Ngôn ngữ và otomat khoảng.

Ngôn ngữ khoảng. Các phép toán trên d-ngôn ngữ. Otomat khoảng đơn định và đa định. Bài toán đơn định hoá otomat khoảng.

Otomat khoảng tối tiểu. Một số ứng dụng. Bài toán tìm d-đường đi nhanh nhất. Mô hình mạng ưu tiên (Priority Network - PN).

Mô hình mạng ưu tiên bằng otomat khoảng. Bài toán đạt được. Ví dụ về PN trong thực tiễn. Mô hình hệ thống máy tính ghép cụm.

Lập lịch công việc. Thuật toán lập lịch tổng quát. 123 Các công trình đã công bố. 125 Tài liệu tham khảo.

126 4 z DANH MỤC TỪ VIẾT TẮT Stt Viết tắt Giải thích Ghi chú 1 CCS Calculus of Commu- Là một công cụ đại số quá trình do nicating Systems Robin Milner đề xuất. 2 CSP Communicating Là một đại số quá trình, do Charles Sequential Processes Antony Richard Hoare đề xuất, là cơ sở của ngôn ngữ lập trình tương tranh OCCAM 3 HOL Higher Order Logic - Là một bộ phận trong nhóm công cụ Light Light chứng minh định lý trên logic bậc cao, phiên bản đơn giản do John Harrison đề xuất. 4 SPIN Simple Promela In- Là công cụ nguồn mở dùng để kiểm terpreter chứng hình thức các hệ thống phần mềm phân tán do Bell Labs phát triển. 5 RAISE Rigorous Approach Là sản phẩm của dự án European to Industrial Soft- ESPRIT II LaCoS do Dines Bjørner ware Engineering làm trưởng dự án.

Sau này bộ công cụ được Viện Công nghệ phần mềm quốc tế của Đại học Liên hiệp quốc UNU-IIST sử dụng để đào tạo về Công nghệ phần mềm cho các nước đang phát triển. Bảng 1 – tiếp ở trang sau 5 z Stt Viết tắt Giải thích Ghi chú 6 UML Unified Modeling Ngôn ngữ mô hình hoá thống nhất. Language Đây là ngôn ngữ mô hình chung được chuẩn hoá dùng trong công nghệ phần mềm hướng đối tượng do Grady Booch, Ivar Jacobson và James Rumbaugh phát triển từ những năm 90. Đến năm 2000, nó đã trở thành chuẩn ISO cho mô hình các hệ thống phần mềm.

7 UPPAAL Upp-sala và Aal-borg Là môi trường công cụ tích hợp xác nhận (validation) và kiểm chứng (ver- ification) các hệ thời gian thực được mô hình bằng mạng các otomat thời gian. Công cụ này do Đại học Upp- sala ở Thuỵ Điển và Đại học Aalborg ở Đan Mạch phát triển. 8 UTP Unifying Theories of Lý thuyết hợp nhất ngôn ngữ lập Programming trình, do Charles Antony Richard Hoare và He Jifeng đề xuất. 6 z Danh sách hình vẽ 1.1 Giao hai khoảng khác rỗng a) và một điểm thuộc một khoảng b) .2 Hiệu liên tục của hai khoảng .3 Hợp liên tục khác rỗng của hai khoảng .4 Hợp không liên tục của hai khoảng cho kết quả rỗng .5 Tích khoảng xác định .6 Tích khoảng theo cấu hình 1 .7 Tích khoảng theo cấu hình 2 .8 Tích khoảng theo cấu hình 3 .9 Tích khoảng theo cấu hình 4 .10 Thứ tự trung vị .11 Ví dụ về Zero-Knowledge .12 Cấu hình kết hợp trái và kết hợp phải với tỉ lệ chia chuẩn .13 Ví dụ về chia khoảng [0, 1] dùng khoá nhị phân 0110001 .14 Cây biểu diễn cách kết hợp để tích xác định theo khóa 0 11 00 01 .15 Tạo cây tương ứng với khoá nhị phân .16 Cây biểu diễn cách kết hợp để tích xác định theo khóa 0 01 00 11 .16 sau khi biến đổi với khóa 1 01 00 01 .1 Tích khoảng của hai d-xâu .3 Trạng thái di chuyển được a) và trạng thái treo b) theo ngữ nghĩa 2 .4 Trạng thái di chuyển được và trạng thái treo theo ngữ nghĩa 3 .5 Otomat khoảng đa định .7 So sánh tính đa định của otomat truyền thống với otomat khoảng .9 Otomat cần đơn định .10 Otomat sau khi ghép cung .11 Otomat sau khi tách cung .12 Trạng thái đạt được và trạng thái treo .13 Loại trạng thái không đạt được .14 Loại trạng thái treo không kết .15 Tối tiểu hóa otomat .1 Chuyển từ otomat sang đồ thị .2 Ví dụ tìm đường từ s đến t .4 Ví dụ về hai nút trong mạng ưu tiên .5 Mô hình mạng ưu tiên .6 Mạng ưu tiên sau khi chiếu tại thời điểm t = 8 .7 Cây suy dẫn của DA trong hình 4.8 Từ ràng buộc cung sang ràng buộc nút .9 Từ ràng buộc nút sang ràng buộc cung.

Đặt vấn đề Để thuận tiện trong nghiên cứu hoặc trước khi triển khai một hệ thống thông tin vào thực tế, người ta thường mô hình hoá chúng bằng một công cụ hình thức. Cách dùng công cụ để mô hình hóa các hệ thống được gọi là phương pháp hình thức. Phương pháp hình thức nghiên cứu cách dùng các ký hiệu trừu tượng, logic cấp 1 và các cấp cao hơn trong việc mô tả và kiểm tra các tính chất của hệ thống trong thế giới thực. Bộ các ký hiệu cùng các quy tắc sử dụng các ký hiệu đó được gọi là các ký pháp hình thức.

Người ta dùng các ký pháp hình thức để mô tả hệ thống và kết quả thu được sau khi mô hình hoá được gọi là mô hình hay đặc tả hình thức của hệ thống. Việc mô hình hoá giúp ta có được hình dung về hệ thống trong thế giới thực và những vấn đề cần quan tâm nghiên cứu đối với hệ thống, các đặc tả chặt chẽ, rõ ràng về hệ thống đó. Thông qua mô hình, ta có thể tìm ra hoặc chứng minh các tính chất, đặc trưng riêng của hệ thống, triển khai các thuật toán để giải quyết hiệu quả các bài toán đặt ra trên mô hình trước khi sử dụng chúng trong thực tiễn. Nghiên cứu về phương pháp hình thức chủ yếu phát triển theo hai hướng chính.

Các cách tiếp cận theo hướng otomat Otomat cổ điển là công cụ hữu hiệu để mô hình hoá các hệ thống hoạt động dưới dạng chuyển trạng thái thông qua nghiên cứu hành vi của chúng. Tuỳ theo nhu cầu thực tế, người ta có thể gia tăng thêm ràng buộc, bổ sung thông tin vào mô hình nhằm tăng thêm sự linh hoạt và mở rộng khả năng biểu diễn của otomat.