Chương 1. TỔNG QUAN Hoạt động của một hệ thống máy tính, cũng như của bất kỳ một hệ thống nào trong các lĩnh vực khác như sinh học, hóa học, vật lý, … đều là chuyển đổi giữa các trạng thái khác nhau của hệ thống. Nhà toán học người Nga Andrei Andreevich Markov (1856-1922) đã nghiên cứu một loại phân bổ xác suất quan trọng trong không gian trạng thái, đặt nền tảng cho một lớp các bài toán, mô hình chuyển trạng thái được gọi chung là không gian trạng thái Markov, hoặc các quá trình có tính chất Markov (Markov properties).Các quá trình có tính chất Markov được áp dụng rộng rãi trong các nghiên cứu cơ bản về hệ thống máy tính, cơ chế làm việc của các ô tô mát, hoặc việc mô hình hóa các hệ thống trong các lĩnh vực khác như sinh học, kinh tế, giao thông. Để bổ sung thêm giá trị thời gian, cũng như các ràng buộc thời gian đối với việc chuyển giữa các trạng thái trong thời gian thực, các nghiên cứu bổ sung sau này đã hoàn thiện các mô hình biểu diễn các ô tô mát thời gian, thực hiện bởi[1]với các giả thiết đồng hồ thời gian chính xác tuyệt đối và các hoạt động xảy ra ngay tức thì (độ trễ bằng 0 tuyệt đối).
Các yếu tố xác suất được nghiên cứu và bổ sung trong biểu diễn ô tô mát thời gian, mở rộng thành mô hình biểu diễn ô tô mát thời gian xác suất, được định nghĩa bằng các phân bố thời gian rời rạc và các lựa chọn ngẫu nhiên cho các nhánh trong ô tô mát thời gian. Mô hình biểu diễn ô tô mát thời gian xác suất giúp có thể mô hình hóa các hệ thống ngoài đời thực, sử dụng các công cụ kiểm chứng để kiểm chứng các đặc tính của các hệ được biểu diễn. Phạm vi đề tài nhằm nghiên cứu các tính chất của ô tô mát thời gian thực xác suất và thực hiện kiểm chứng tự động các tính chất đó bằng công cụ. Có thể phát biểu bài toán kiểm chứng mà đề tài cần giải quyết như sau: Cho hệ thống thời gian thực xác suất M.
Thực hiện kiểm chứng tự động bằng công cụ xem M có thỏa mãn tính chất P hay không. Để có thể giải quyết bài toán kiểm chứng tự động bằng công cụ, phạm vi nghiên cứu của đề tài sẽ tập trung vào các nội dung chính bao gồm: 1. Mô hình hóa hệ xác suất thời gian thực bằng ô tô mát thời gian thực xác suất PTA. Hình thức hóa các tính chất xác suất cần kiểm chứng bằng cây lô gic tính toán xác suất PCTL.
Nghiên cứu công cụ hỗ trợ cài đặt PTA và biểu diễn tính chất để thực hiện kiểm chứng tự động. LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Áp dụng với nghiên cứu với giao thức Alternating Bit Protocol: Mô hình hóa hệ giao thức bằng PTA, hình thức hóa các tính chất bằng PCTL và thực hiện cài đặt hệ giao thức trên công cụ PRISM. Cấu trúc trình bày của đề tài gồm sáu phần chính.
Phần đầu là giới thiệu tổng quan về đề tài, phần hai là cơ sở khoa học của đề tài, nêu các biểu diễn và tính chất các quá trình Markov. Phần ba trình bày việc kiểm chứng tự động các ô tô mát thời gian thực xác suất, gồm các cú pháp và ngữ nghĩa các PTA, đặc tả tính chất cho PTA và các phương pháp kiểm chứng tự động đối với PTA. Phần bốn giới thiệu công cụ kiểm chứng mô hình PRISM, là công cụ có khả năng kiểm chứng tự động các tính chất của các hệ mô hình hóa khác nhau trong đó có PTA. Phần năm trình bày một trường hợp áp dụng PTA để mô hình hóa hệ giao thức Alternating Bit Protocol và hình thức hóa các tính chất của ABP, cài đặt bằng công cụ PRISM và kiểm chứng tự động các tính chất của ABP.
Phần cuối cùng là phần kết luận, đề xuất các hướng nghiên cứu mở rộng của đề tài. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 11 Chương 2. CƠ SỞ KHOA HỌC CỦA ĐỀ TÀI Giới thiệu chung về chuỗi Markov Chuỗi Markov (Markov chain hay Markov process) là một quá trình ngẫu nhiên với các đặc tính Markov. Thuật ngữ “chuỗi Markov” (hay “xích Markov”, “quá trình Markov”) dành để chỉ trình tự các biến ngẫu nhiên mà một tiến trình trải qua, với đặc tính Markov được định nghĩa là khả năng xuất hiện của các biến ngẫu nhiên tiếp theo chỉ phụ thuộc vào biến hiện tại (tạo thành 1 chuỗi).
Khi áp dụng trong không gian trạng thái, nó có thể được dùng để mô tả các hệ thống có các chuỗi trạng thái liên kết với nhau, và những biến đổi sang trạng thái tiếp theo chỉ phụ thuộc trạng thái hiện tại của hệ thống. Quá trình có tính chất Markov Một quá trình là một ô tô mát (hay quá trình, hoặc một chuỗi trạng thái) bắt đầu với một trong các trạng thái này và dịch chuyển từ trạng thái này sang trạng thái khác. Nếu ô tô mát đang ở trạng thái si, sau đó chuyển sang trạng thái sj ở bước tiếp theo với xác suất được biểu diễn bằng pij, và giá trị này không phụ thuộc vào các trạng thái ô tô mát trước khi chuyển sang trạng thái hiện tại. Các giá trị xác suất pij được gọi là các xác suất chuyển (transition probability).
Ô tô mát có thể ở trạng thái hiện tại, với xác suất được ghi nhận là pii. Việc phân bố xác suất các trạng thái ban đầu được định nghĩa bởi S. Thông thường các trạng thái ban đầu được xác định bởi một hoặc một số trạng thái, trong đó nếu các phân bố xác suất chuyển từ trạng thái hiện tại sang các trạng thái tiếp theo chỉ phụ thuộc vào trạng thái hiện tại thì quá trình như vậy được gọi là có tính chất Markov, gọi ngắn gọn là Quá trình Markov. pn+1 = Pr(sn+1 = x | s1 = x1, s2 = x2, ., sn = xn) = Pr(sn+1 = x | sn = xn) 2.1 Xích Markov thời gian rời rạc (DTMC) Định nghĩa Hình 2.1 là minh họa cho một xích Markov (hay một chuỗi Markov) đơn giản, với 3 trạng thái s0, s1, s2 và xác suất chuyển giữa các trạng thái thể hiện trên các đường nối giữa các trạng thái.
DTMClà quá trình biến đổi trạng thái rời rạc, thuần nhất theo thời gian. Khái niệm thuần nhất theo thời gian được hiểu là xác suất pij chuyển trạng thái từ si sang sj của chuỗi Markov là giá trị không phụ thuộc thời LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Nói cách khác tại mọi thời điểm được xét, giá trị xác suất pij không thay đổi.1: Markov chain Khái niệm tập không gian trạng thái trong chuỗi Markov không được thống nhất về phạm vi giới hạn trong các tài liệu khác nhau, không gian trạng thái có thể dùng để biểu diễn quá trình xảy ra với bất kỳ dạng biến đổi nào, do vậy có thể là không gian hữu hạn hoặc vô hạn, đếm được hoặc không đếm được. Tuy nhiên, phần lớn các ứng dụng chuỗi Markov chỉ sử dụng tập không gian trạng thái hữu hạn, hoặc tập không gian trạng thái vô hạn đếm được, có các đặc điểm phân tích thống kê đơn giản hơn.
Vector xác suất Vector xác suất với r thành phần là một vector dòng với các giá trị không âm, và tổng các giá trị là 1. Gọi u là vector xác suất biểu diễn trạng thái ban đầu của chuỗi Markov, khi đó thành phần thứ i của u biểu thị xác suất chuỗi Markov sẽ bắt đầu ở trạng thái si. Ma trận xác suất (còn gọi là ma trận chuyển – transition matrix) Giá trị pij cho biết xác suất chuyển từ trạng thái i sang trạng thái j. Do xác suất là giá trị không âm, và hệ sẽ phải chuyển đến một trạng thái nào đó, ta có: pij≥ 0, i, j ≥ 0; = 1, i = 0, 1, ….
r Ma trận P kích thước r x r gồm các phần tử pij là ma trận chuyển của chuỗi Markov có r+1 trạng thái. LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 13 … … … … … … … Chuỗi Markov hấp thụ (absorbing Markov chain) Một trạng thái si của chuỗi Markov được gọi là trạng thái hấp thụ (absorbing) nếu chuỗi không thể thoát ra khỏi trạng thái đó (pii = 1). Một chuỗi Markov là hấp thụ nếu nó có ít nhất một trạng thái hấp thụ, và từ một trạng thái bất kỳ nó có thể chuyển về trạng thái hấp thụ (có thể qua nhiều bước). Trong một chuỗi Markov hấp thụ, một trạng thái không phải là trạng thái hấp thụ được gọi là trạng thái trung gian hay trạng thái chuyển (transient state).
Dạng chuẩn của ma trận chuyển (canonical form) Xét một chuỗi Markov hấp thụ bất kỳ. Đánh số lại các trạng thái để các trạng thái trung gian đứng trước. Giả sử có r trạng thái hấp thụ và t trạng thái trung gian, ma trận chuyển sẽ có dạng chuẩn như sau: Trong đó I là ma trận đơn vị r-r, 0 là ma trận 0 cho các xác suất chuyển r-t, R là ma trận chuyển t-r (khác 0) và Q là ma trận chuyển t-t. Trong dạng này, t trạng thái đầu tiên là trạng thái trung gian, và r trạng thái cuối cùng là trạng thái hấp thụ.
TR thể hiện các dòng/cột ứng với trạng thái trung gian (gồm t dòng/cột), ABS thể hiện các dòng/cột ứng với trạng thái hấp thụ (gồm r dòng/cột). Ma trận cơ sở N (fundamental matrix) Với một chuỗi Markov hấp thụ với ma trận chuyển P, ma trận nghịch đảo của I-Q:N = (I-Q)-1 được gọi là ma trận cơ sở của P. Giá trị nij của N cho biết con số kỳ vọng mà chuỗi Markov sẽ ở trạng thái trung gian sj nếu xuất phát từ trạng thái trung gian si. Chuỗi Markov liên thông (ergodic chain) LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 14 Một chuỗi Markov được gọi là liên thông nếu nó có thể chuyển sang mọi trạng thái từ bất kỳ trạng thái nào (không nhất thiết phải trong 1 lần chuyển).
Trong nhiều sách, chuỗi Markov như vậy còn được gọi là chuỗi Markov tối giản (irreducible chains) Thời gian chu kỳ của trạng thái Nếu một chuỗi Markov liên thông xuất phát từ trạng thái si, số lượt chuyển kỳ vọng để đạt đến trạng thái sj lần đầu tiên được gọi là thời gian lần đầu tiên đi từ si đến sj. Giá trị này được biêu diễn bởi mij. Theo quy ước mii = 0. Nếu một chuỗi Markov liên thông xuất phát từ trạng thái si, số lượt chuyển kỳ vọng của chuỗi đến khi quay về si lần đầu tiên được gọi là thời gian chu kỳ cho trạng thái si.
Biểu diễn giá trị này là ri.