đặt vấn đề nghiên cứu và đề xuất các thuật toán kiểm chứng cho lớp các công thức này. Trên cơ sở đó chúng tôi xin tóm tắt vài kết quả chính mà chúng tôi đã đạt được trong quá trình thực hiện mục đích của luận án. Một số kết quả chính • Đề xuất biểu diễn dáng điệu lưới ôtômat thời gian thực bởi biểu thức chính qui theo thời gian, trên cơ sở đó giải bài toán kiểm chứng các tính chất khoảng tuyến tính (LDP) và bất biến khoảng tuyến tính (LDI) bằng qui hoạch tuyến tính. • Chứng minh tính rời rạc hoá được (với ngữ nghĩa tổng quát) của lớp các công thức LDP, LDI.
• Xây dựng đồ thị đạt được có trọng số hướng đến LDP, trên cơ sở đó đề nghị một thuật toán kiểm chứng lớp công thức LDP bằng cách áp dụng thuật toán tìm đường đi ngắn nhất của Warshall-Floyd. • Đề xuất đồ thị "rời rạc hoá" của đồ thị đạt được. Chứng minh tính quyết định được của lớp công thức LDI bằng một thuật toán duyệt đồ thị này. Các kết quả này đã được báo cáo tại các xemine của bộ môn Khoa học máy tính, hội nghị khoa học Khoa Công nghệ Đại học Quốc gia Hà Nội, hội thảo quốc gia về Công nghệ thông tin, xemine của UNU/IIST và các hội nghị quốc tế (Nhật bản-1998, Việt Nam-2002, Trung Quốc-2004) và đã được công bố chính trong các công trình [56], [57], [58], [59].
LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 13 Cấu trúc của luận án Phần chính của luận án gồm 4 chương. Trong chương này chúng tôi đã trình bày tóm tắt về một số đặc trưng của kiểm chứng mô hình, cũng như những kết quả và hạn chế trong lĩnh vực kiểm chứng các tính chất thời khoảng cho đến thời điểm hiện nay. Các kiến thức cơ bản để phục vụ luận án như ôtômat thời gian và lôgic khoảng được trình bày trong chương 2. Kết quả chính của luận án được trình bày trong hai chương 3 và 4.
Trong đó, ở chương 3 chúng tôi trình bày về cách biểu diễn lưới ôtômat thời gian thực bởi biểu thức chính quy thời gian và thiết lập bài toán qui hoạch tuyến tính để kiểm chứng các lớp công thức LDP, LDI. Đặc trưng của biểu thức chính quy ở đây là phép toán đồng bộ hoá quá trình chuyển trạng thái, một phép toán cơ bản để biểu diễn ôtômat thời gian bằng các biểu thức chính quy thời gian ([10]). Trong chương 4 chúng tôi chứng minh tính rời rạc hoá được của LDP, LDI và xây dựng các đồ thị đạt được có trọng số trên cơ sở các đồ thị vùng từ đó đưa ra thuật toán hữu hiệu kiểm chứng công thức LDP. Cũng trong chương này thuật toán duyệt trên đồ thị vùng đã "rời rạc hoá" được xây dựng để kết luận tính quyết định được của LDI theo ngữ nghĩa tổng quát của nó.
Cuối cùng trong phần kết luận chúng tôi tóm tắt về luận án, nhận xét các ưu khuyết điểm của các phương pháp đã được sử dụng, chỉ ra triển vọng của các phương pháp và đề nghị một vài cải tiến để hoàn chỉnh các thuật toán cũng như đề xuất một vài hướng nghiên cứu tiếp tục. Để minh hoạ các thuật toán đã trình bày trong chương 4, chúng tôi cũng cài đặt một bộ chương trình kiểm chứng mô hình ở mức độ đơn giản. Một số nét đặc trưng và kết quả áp dụng của bộ kiểm chứng mô hình này được mô tả trong phần phụ lục. Chúng tôi hy vọng luận án là những kết quả bước đầu đặt nền tảng cho các nghiên cứu tiếp của chúng tôi về một lĩnh vực đã đạt nhiều thành tựu nhưng cũng còn nhiều khó khăn như trong lĩnh vực kiểm chứng mô hình này.
LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Chương 2 Đặc tả hệ thống và tính chất Để đặc tả hệ thống luận án sẽ sử dụng ôtômat thời gian là mô hình được dùng rộng rãi hiện nay, còn tính chất thời khoảng sẽ được đặc tả bởi các công thức trong lôgic khoảng. Việc sử dụng hai công cụ hình thức này được gặp hầu hết trong các tài liệu tham khảo và được trình bày chi tiết trong [7, 8, 18, 35].1 Mô hình thời gian 2.1 Thể hiện đồng hồ và ràng buộc thời gian Để đánh dấu và đo lượng thời gian chúng ta sử dụng một tập X các biến thời gian x (mà có thể gọi ngắn gọn và hình ảnh hơn là các đồng hồ). Về mặt tổng quát giá trị của các đồng hồ có thể thay đổi với các vận tốc khác nhau, tuy nhiên luận án này chỉ xét hệ thống với giá trị của các đồng hồ tăng đều và theo cùng một vận tốc giống nhau. Tại một thời điểm cụ thể mỗi đồng hồ trong X sẽ nhận một giá trị số trong tập hợp TIME nào đấy biểu thị lượng thời gian đã trôi qua.
Thông thường TIME là tập các số tự nhiên N hoặc tập các số thực R+ tuỳ theo theo ngữ cảnh thời gian được sử dụng và được mặc định lấy trên tập số thực R+. Mỗi đồng hồ đóng vai trò đếm lượng thời gian trôi của một hay nhiều tác vụ của hệ thống, có thể được đặt lại giá trị ban đầu (0) sau mỗi tác vụ. Một bộ ν bất kỳ các giá trị đồng hồ được gọi là thể hiện đồng hồ 14 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 15 (clock interpretations), tức ν là một ánh xạ từ X tới TIME. Giá trị của một đồng hồ x trong thể hiện ν được kí hiệu bởi ν(x).
Thông thường, một thể hiện đồng hồ có thể được gọi một cách ngắn gọn là thể hiện. Cho δ là một số thực không âm và λ ⊆ X là một tập đồng hồ. Khi đó ν = ν + δ kí hiệu cho thể hiện mà nó ánh xạ mỗi đồng hồ x tới giá trị ν(x) + δ, tức ν (x) = ν(x) + δ, ∀x ∈ X. Một hệ thời gian thực khi hoạt động phải tuân theo một qui luật thời gian nào đó thông qua các ràng buộc thời gian trên tập đồng hồ X.
Một ràng buộc thời gian như vậy là một công thức ϕ được cho theo cú pháp sau đây: ϕ := x ≤ c | c ≤ x | x − y ≤ c | c ≤ x − y | ϕ ∧ ϕ ở đây x, y ∈ X và c ∈ N. Để viết gọn ϕ ta cũng sử dụng các phép toán ¬, ∨ theo nghĩa thông thường trong lôgic mệnh đề. Thực tế c có thể được xét như các hằng hữu tỷ, tuy nhiên bằng cách nhân tất cả các hằng với bội chung nhỏ nhất của các mẫu số của c trong tập hữu hạn các ràng buộc của hệ thống, chúng ta có thể đưa chúng về lại là các hằng nguyên. Một thể hiện ν được gọi là thoả ràng buộc ϕ nếu thay mọi biến x trong ϕ bởi ν(x) ta nhận được một công thức đúng, và kí hiệu ν |= ϕ, ngược lại ta kí hiệu ν |= ϕ.
Tập các ràng buộc thời gian ϕ trên X được kí hiệu bởi Φ(X). Từ đây trở đi ta qui ước sử dụng kí hiệu a |= α và a |= α để chỉ quan hệ a thoả α và a không thoả α. Ngữ nghĩa của quan hệ "thoả" (và từ đó kéo theo cũng "không thoả") sẽ được định nghĩa trong từng trường hợp cụ thể.2 Kỹ thuật phân vùng đồng hồ Cho tập đồng hồ X lấy giá trị trên tập số thực không âm R+ và một tập hữu hạn các ràng buộc đồng hồ φ ⊆ Φ(X). Việc duyệt tất cả các thể hiện thoả hay không thoả các công thức trong φ là không thể vì số lượng các thể hiện ν là vô hạn.
Do vậy trong [7], Alur và Dill đề xuất một kỹ thuật phân hoạch tập LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 16 các thể hiện đồng hồ thành các vùng đồng hồ (clock regions) bởi một quan hệ tương đương chỉ số hữu hạn hướng đến tập ràng buộc đồng hồ φ như sau. Xét đồng hồ x, gọi cx là số nguyên lớn nhất xuất hiện trong các ràng buộc đồng hồ của x trong tập các công thức φ. Với số thực t ta kí hiệu t và f r(t) lần lượt là phần nguyên và phần lẻ của t. Hai thể hiện ν và ν được gọi là tương đương (hướng đến tập các ràng buộc φ) và được kí hiệu ν ∼= ν nếu: 1.
∀x ∈ X, hoặc ν(x) = ν (x) hoặc cả hai cùng lớn hơn cx. ∀x ∈ X và ν(x) ≤ cx thì f r(ν(x)) = 0 khi và chỉ khi f r(ν (x)) = 0 Gọi k là số đồng hồ trong X. Quan hệ ∼ = có các tính chất sau. ∼ = là một quan hệ tương đương trên tập các thể hiện đồng hồ.
Rõ ràng mọi thể hiện trong cùng một vùng sẽ cùng thoả hoặc không thoả một ràng buộc đồng hồ trong φ. Từ đó ta có tính chất: Tính chất 2. Mỗi vùng đồng hồ được đặc trưng bởi một ràng buộc đồng hồ. Số vùng đồng hồ là hữu hạn và bị chặn bởi k! 2k (2cx + 2).
x∈X Chứng minh chi tiết của các tính chất trên được gặp nhiều trong các tài liệu tham khảo (ví dụ [7, 64]), vì vậy ở đây chúng tôi không trình bày lại các chứng minh đó. Xét φ là lớp các ràng buộc trên tập đồng hồ {x, y} trong đó cx = 2 và cy = 1. Khi đó tập gồm 28 vùng đồng hồ hướng tới φ được cho trong hình 2. Trong đó lớp các vùng thoả ràng buộc x ≤ 2 ∧ y ≤ 1 là tất cả trừ 4 vùng không bị chặn, tức trừ các vùng có chứa ít nhất một ràng buộc x > 2 hoặc y > 1.
Tương tự thoả ràng buộc x ≥ 2 ∧ y ≥ 1 có hai vùng [(2, 1)] và [x > 2 ∧ y > 1]. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.1: Các vùng với cận đồng hồ cx = 2, cy = 1.2 Ôtômat thời gian Ôtômat thời gian là một công cụ hữu hiệu để mô hình và kiểm chứng các chức năng đúng đắn của các hệ thời gian thực được Alur và Dill đề xuất trong [7]. Các thành tựu nội tại của lý thuyết ôtômat thời gian đã được công bố trong rất nhiều công trình. Có thể liệt kê một cách ngắn gọn về các thành tựu này như khả năng biểu diễn của ôtômat thời gian trong [9, 39], hay khả năng biểu diễn đối với các ôtômat thời gian mở rộng trong [30, 41, 20, 12], hoặc các rút gọn không gian trạng thái của ôtômat thời gian như trong [27, 61].