Tổng quan luận án

Luận án tiến sĩ toán học với đề tài "Một số phương pháp kiểm chứng tính đúng đắn của hệ thời gian thực bằng thuật toán" được thực hiện bởi nghiên cứu sinh Phạm Hồng Thái tại Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội vào năm 2005. Công trình thuộc chuyên ngành Đảm bảo toán học cho máy tính và các hệ thống tính toán (mã số chuyên ngành: 1.10), dưới sự hướng dẫn khoa học của TS. Đặng Văn Hưng và PGS. Đinh Mạnh Tường. Nghiên cứu được triển khai trong khuôn khổ dự án DeTfoRS (Design Techniques for Real-Time Systems) do Viện Công nghệ Phần mềm Quốc tế thuộc Đại học Liên hợp quốc (UNU/IIST, Macau) tài trợ và đề tài nghiên cứu trọng điểm cấp quốc gia "Các phương pháp đặc tả và kiểm chứng trong công nghệ phần mềm" do PGS. Hồ Sĩ Đàm chủ trì.

Về tính cấp thiết, sự phát triển của các hệ thống tính toán thời gian thực (cả phần cứng và phần mềm) đòi hỏi mức độ chính xác tuyệt đối, bởi vì một sai sót nhỏ có thể dẫn tới sự cố phá hủy nghiêm trọng (điển hình như vụ nổ tên lửa Ariane 5 vào ngày 4 tháng 6 năm 1996 xuất phát từ lỗi phần mềm tính toán chuyển động). Kiểm chứng mô hình (Model Checking) ra đời nhằm tự động hóa việc kiểm tra tính đúng đắn của hệ thống trên không gian trạng thái. Tuy nhiên, đối với hệ thời gian thực, việc tham số thời gian được xác định trên tập số thực trù mật $\mathbb{R}^+$ đã gây ra sự bùng nổ không gian trạng thái vô hạn. Hơn nữa, trong khi các tính chất thời điểm (point properties) đã có nhiều công cụ hỗ trợ, các tính chất thời khoảng (duration properties) – tức các yêu cầu liên quan đến khoảng thời gian tích lũy mà hệ thống lưu lại ở các trạng thái – lại gặp trở ngại lớn do phần lớn các công thức trong Lôgic khoảng (Duration Calculus - DC) là không quyết định được (undecidable).

Khoảng trống nghiên cứu được tác giả xác định là: các thuật toán kiểm chứng tính chất thời khoảng đã công bố trước thời điểm nghiên cứu còn rời rạc, chủ yếu chỉ áp dụng cho một số lớp con hạn chế của ôtômat thời gian, ràng buộc các hệ số trong tập số nguyên $\mathbb{Z}$, hoặc sinh ra số lượng bài toán quy hoạch tuyến tính quá lớn. Đặc biệt, các kết quả tiền nhiệm chỉ khảo sát các quan sát xuất phát từ thời điểm ban đầu ($t = 0$), tức áp dụng với ngữ nghĩa thu hẹp. Luận án đặt mục tiêu mở rộng việc kiểm chứng trên hệ thống tổng quát và xem xét các tính chất thời khoảng trong ngữ nghĩa tổng quát, tức trên các khoảng quan sát thời gian $[b, e]$ bất kỳ ($0 \le b \le e < \infty$).

Mục tiêu và các kết quả nghiên cứu chính của luận án được đánh số cụ thể như sau:

  1. Đề xuất biểu diễn dáng điệu của lưới ôtômat thời gian thực bằng biểu thức chính quy thời gian (Timed Regular Expression - TRE), 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 (Linear Duration Properties - LDP) và bất biến khoảng tuyến tính (Linear Duration Invariants - LDI) bằng quy hoạch tuyến tính.
  2. Chứng minh tính rời rạc hoá được (discretisability) với ngữ nghĩa tổng quát của hai lớp công thức LDP và LDI.
  3. Xây dựng đồ thị đạt được có trọng số hướng đến LDP, từ đó đề xuất thuật toán kiểm chứng LDP bằng cách áp dụng thuật toán tìm đường đi ngắn nhất Warshall-Floyd.
  4. Đề xuất đồ thị đạt được nguyên (đồ thị đã rời rạc hoá) và chứng minh tính quyết định được của lớp công thức LDI bằng thuật toán duyệt đồ thị này.

Đối tượng nghiên cứu của luận án là các hệ thời gian thực được mô hình hóa bởi ôtômat thời gian (Timed Automata - TA), lưới ôtômat thời gian thực, biểu thức chính quy thời gian, cùng các đặc tả tính chất thời khoảng trong Lôgic khoảng (LDP và LDI). Phạm vi nghiên cứu giới hạn ở lớp ôtômat thời gian không Zeno (non-Zeno), các đồng hồ có tốc độ tăng tuyến tính đồng đều; xét trên mô hình thời gian thực liên tục $\mathbb{R}^+$ và mô hình thời gian rời rạc $\mathbb{N}$; khảo sát các khoảng quan sát $[b, e]$ bất kỳ với $0 \le b \le e < \infty$.

Tổng quan tài liệu và vị trí của luận án

Trong chương tổng quan, tác giả điểm lại lịch sử phát triển của các phương pháp hình thức trong đặc tả và kiểm chứng hệ thống qua các giai đoạn:

  • Giai đoạn chứng minh định lý hình thức (thập niên 1970): Các công trình của Dijkstra, Floyd, Gries, Hoare, Owicki, Manna, Pnueli ([23]) sử dụng hệ tiên đề và luật dẫn toán học để chứng minh tính đúng đắn của chương trình. Phương pháp này đòi hỏi thao tác suy luận thủ công phức tạp. Các ngôn ngữ đặc tả hình thức sử dụng cấu trúc toán học tập hợp, hàm, quan hệ gồm Z, VDM, RAISE ([60, 31]).
  • Giai đoạn kiểm chứng mô hình cổ điển (từ năm 1981): E. Emerson ([22]) đưa ra thuật ngữ Model Checking. Hướng tiếp cận duyệt không gian trạng thái được nghiên cứu độc lập bởi Clarke & Emerson ([22]) và Queille & Sifakis ([50]), phát triển trên các hệ lôgic thời gian tuần tự như Lôgic cây tính toán (Computational Tree Logic - CTL) và Lôgic thời gian tuyến tính mệnh đề (Propositional Linear Temporal Logic - PLTL) ([24]). Hướng tiếp cận dựa trên bài toán kiểm tra tính rỗng của ngôn ngữ được đề xuất bởi Alur & Dill ([7]), Kurshan ([46]), Vardi & Wolper ([42]). Năm 1992, Clarke và McMillan xây dựng bộ kiểm chứng ký hiệu SMV (Symbolic Model Verifier) sử dụng sơ đồ biểu diễn nhị phân BDD (Binary Decision Diagram), cho phép kiểm chứng hệ thống có không gian trạng thái lên tới $10^{20}$ trạng thái ([48]), cùng công cụ SPIN của Holzmann ([34]).
  • Kiểm chứng mô hình cho hệ thời gian thực (từ đầu thập niên 1990): Alur và Dill ([7, 8]) đề xuất công cụ ôtômat thời gian và kỹ thuật phân vùng đồng hồ (clock regions). Alur, Courcoubetis, Dill ([5]) phát triển Lôgic cây tính toán theo thời gian (TCTL). Nhiều công cụ kiểm chứng thời gian thực ra đời như HyTech ([38]), KRONOS ([16, 26]), UPPAAL ([13]), hoặc nghiên cứu tích hợp trên SPIN ([21]). Kỹ thuật tối ưu hóa không gian trạng thái gồm hợp vùng thành miền (zones) dựa trên mô phỏng và trừu tượng hóa ([55, 61]), phương pháp thứ tự bộ phận (partial orders) ([49]), cùng các kỹ thuật ký hiệu và on-the-fly ([14, 40]).
  • Kiểm chứng tính chất thời khoảng và Lôgic khoảng: Xuất phát từ bài toán đạt được trong khoảng thời gian bị chặn của Alur, Courcoubetis, Dill ([6]). Hệ Lôgic khoảng (DC) được giới thiệu lần đầu bởi Zhou Chaochen, C.A.R. Hoare, A.P. Ravn năm 1991 ([18]) trong dự án ProCoS (ESPRIT BRA 3104), tiếp tục phát triển tại UNU/IIST ([1, 43]). Khảo sát về tính quyết định được của các lớp công thức DC được nghiên cứu bởi Pandya ([53, 54]), Rabinovich ([51]), Hansen và Zhou Chaochen ([35]). Zhou Chaochen, Zhang Jingzhong, Yang Lu, Đặng Văn Hưng (1994) ([45]) chứng minh tính quyết định được của các ràng buộc tuyến tính trên ôtômat thời gian hữu hạn (FTA) bằng cách đưa về quy hoạch nguyên, nhưng hạn chế ở các hệ số nguyên $\mathbb{Z}$. Đặng Văn Hưng và các cộng sự ([28, 29, 56]) mở rộng kiểm chứng LDI cho ôtômat lai và lưới ôtômat bằng TRE, nhưng gặp hạn chế bùng nổ số lượng bài toán quy hoạch tuyến tính phụ thuộc vào độ lớn cận đồng hồ và cận trên khoảng quan sát. Đặng Văn Hưng và Vương Cát (Wang Ji) ([44]) đề xuất phương pháp rời rạc hóa cho LDP. Đặng Văn Hưng ([63]) đề xuất thuật toán cho tính chất khoảng thời gian tuần tự (TDP), được Phạm Hồng Thái và Đặng Văn Hưng ([2, 57]) mở rộng cho lưới ôtômat thời gian.

Vị trí của luận án: Luận án khắc phục nhược điểm cốt lõi của các công trình đi trước (vốn chỉ xét quan sát bắt đầu từ thời điểm $t = 0$) bằng cách thiết lập phương pháp kiểm chứng cho công thức LDP và giải quyết câu hỏi về tính quyết định được của LDI trong ngữ nghĩa tổng quát với khoảng quan sát $[b, e]$ bất kỳ.

Cơ sở lý thuyết và phương pháp nghiên cứu

Luận án xây dựng trên các khung lý thuyết hình thức sau:

  • Mô hình thời gian và ràng buộc đồng hồ: Sử dụng tập biến thời gian $X$ gồm $k$ đồng hồ nhận giá trị trong $\mathbb{R}^+$, tăng đều cùng vận tốc. Thể hiện đồng hồ $\nu: X \to \mathbb{R}^+$. Cú pháp ràng buộc thời gian $\phi \in \Phi(X)$ có dạng: $$\phi := x \le c \mid c \le x \mid x - y \le c \mid c \le x - y \mid \phi \wedge \phi \quad (x, y \in X, c \in \mathbb{N})$$
  • Kỹ thuật phân vùng đồng hồ của Alur và Dill: Thiết lập quan hệ tương đương chỉ số hữu hạn $\nu \cong \nu'$ dựa trên cận nguyên lớn nhất $c_x$ của từng đồng hồ $x \in X$. Số lượng vùng đồng hồ là hữu hạn và bị chặn trên bởi: $$k! \cdot 2^k \prod_{x \in X} (2c_x + 2)$$ Ví dụ với 2 đồng hồ ${x, y}$, $c_x = 2, c_y = 1$, số vùng đồng hồ tạo thành là 28 vùng.
  • Ôtômat thời gian (TA): Cấu trúc $\mathcal{A} = \langle S, s_0, \Sigma, X, I, E \rangle$, trong đó $S$ là tập hữu hạn vị trí; $s_0$ là vị trí ban đầu; $\Sigma$ là bảng chữ cái; $X$ là tập đồng hồ; $I: S \to \Phi(X)$ là bất biến gán cho vị trí; $E \subseteq S \times \Phi(X) \times \Sigma \times 2^X \times S$ là tập phép chuyển vị trí $e = \langle s, \phi, a, \lambda, s' \rangle$. Hệ thống có hai loại phép chuyển trạng thái: chuyển liên tục $q = (s, \nu) \xrightarrow{\delta} q' = (s, \nu + \delta)$ và chuyển rời rạc $q = (s, \nu) \xrightarrow{a} q' = (s', \nu[\lambda := 0])$. Luận án chỉ xét lớp ôtômat non-Zeno.
  • Hợp song song của ôtômat thời gian: $\mathcal{A}_1 \parallel \mathcal{A}_2$ có tập vị trí $S_1 \times S_2$, tập đồng hồ $X_1 \cup X_2$, thực hiện đồng bộ hóa trên các nhãn chung $a \in \Sigma_1 \cap \Sigma_2$ và xen kẽ trên các nhãn riêng.
  • Lôgic khoảng (DC): Trạng thái $s \in S$ được xem như hàm bool theo thời gian $s: \text{TIME} \to {0, 1}$. Mô hình DC là cặp $\sigma = (I, [b, e])$ với $0 \le b \le e < \infty$. Khoảng thời gian tích lũy của trạng thái $s$ trên $[b, e]$ được xác định bởi tích phân $\int s = \int_b^e s(t)dt$, độ dài quan sát $\ell = e - b = \int 1$.
  • Hai lớp công thức khoảng:
    • Tính chất khoảng tuyến tính (LDP): $\sum_{i=1}^m c_i \int s_i \le M$.
    • Bất biến khoảng tuyến tính (LDI): $A \le \ell \le B \implies \sum_{i=1}^m c_i \int s_i \le M$.

Phương pháp nghiên cứu thực tế:

  • Phương pháp quy hoạch tuyến tính: Sử dụng biểu thức chính quy thời gian (TRE) tích hợp toán tử hợp song song $\otimes$ để mô hình hóa hành vi hệ thống; khử toán tử lặp $*$ và phép hoặc $\oplus$ để phân rã TRE thành tập các TRE đơn giản; thiết lập hệ ràng buộc tuyến tính $C(R)$ và giải bài toán tối ưu hàm mục tiêu $\max \theta(R)$ trên miền ràng buộc.
  • Phương pháp rời rạc hóa và lý thuyết đồ thị: Chứng minh sự tương đương giữa kiểm chứng trên miền thời gian thực $\mathbb{R}^+$ và miền thời gian rời rạc $\mathbb{N}$; xây dựng đồ thị vùng đạt được nguyên $RG$ lưu trữ khoảng cách thời gian cực tiểu và cực đại giữa các bước chuyển; ánh xạ sang đồ thị trọng số $G$; áp dụng thuật toán Warshall-Floyd và các thuật toán duyệt đồ thị có trọng số.
  • Nguồn tư liệu, dữ liệu thực nghiệm: Sử dụng các mô hình hệ thống kinh điển gồm Hệ bếp ga (Gas Burner) với các công thức $Des1, Des2, Req$ và Hệ điều khiển chắn tàu (Railroad Crossing) với các tham số thời gian $a, b, c$; tập dữ liệu kiểm thử thực nghiệm DATA1 và mô hình hệ chắn tàu với $a = b = c = 1$ được cài đặt trong bộ công cụ kiểm chứng mô hình tại Phụ lục A.

Nội dung chính theo từng chương

Chương 1: Kiểm chứng mô hình và hệ thời gian thực

Chương 1 giới thiệu tổng quan về lý thuyết đặc tả hình thức và vai trò của việc kiểm tra hệ thống. Tác giả phân tích sự khác biệt bản chất giữa phương pháp chứng minh định lý toán học truyền thống (nặng nhọc, yêu cầu chứng minh tổng quát) và phương pháp kiểm chứng mô hình (tự động hóa hoàn toàn bằng thuật toán trên không gian trạng thái, cung cấp vết lỗi phục vụ gỡ lỗi). Phân tích sự chuyển dịch từ kiểm chứng mô hình cổ điển sang kiểm chứng mô hình thời gian thực với công cụ nền tảng là ôtômat thời gian. Luận án chỉ ra tính chất thời khoảng (đo lường độ dài thời gian xuất hiện trạng thái) có độ phức tạp vượt trội so với tính chất thời điểm (chỉ kiểm tra sự xuất hiện trạng thái) vì tính chất khoảng phụ thuộc vào vô hạn các đoạn quan sát bất kỳ $[b, e]$. Tác giả tổng kết các kết quả của dự án DeTfoRS (UNU/IIST) và xác định bốn mục tiêu nghiên cứu cụ thể của đề tài.

Chương 2: Đặc tả hệ thống và tính chất

Chương 2 trình bày chi tiết cú pháp và ngữ nghĩa của các công cụ hình thức được sử dụng xuyên suốt luận án:

  • Mô hình thời gian và phân vùng đồng hồ: Định nghĩa thể hiện đồng hồ $\nu$, phép tịnh tiến thời gian $\nu + \delta$, cú pháp ràng buộc thời gian $\Phi(X)$. Trình bày định nghĩa quan hệ tương đương $\nu \cong \nu'$ của Alur và Dill; chứng minh số vùng đồng hồ là hữu hạn và bị chặn bởi công thức chứa cận nguyên lớn nhất $c_x$.
  • Ngữ nghĩa ôtômat thời gian: Định nghĩa bộ $\mathcal{A}$, trạng thái $(s, \nu)$, phép chuyển liên tục, phép chuyển rời rạc, đường chạy $r$ và dáng điệu $\rho = (s_0, t_0)(s_1, t_1)\dots$ với $t_0 = 0$, $\delta_i = t_i - t_{i-1}$. Định nghĩa tích đồng bộ $\mathcal{A}_1 \parallel \mathcal{A}_2$. Quy ước xét lớp ôtômat non-Zeno.
  • Lôgic khoảng (DC): Trình bày ngữ nghĩa mô hình $\sigma = (I, [b, e])$, toán tử tích phân $\int s$ và độ dài $\ell$. Minh họa qua hệ bếp ga gồm hai trạng thái $Leak$ (rò ga) và $Nonleak$ (không rò ga) với hai quyết định thiết kế:
    • $Des1$: Thời gian rò ga không quá 1 giây ($\ell \le 1$).
    • $Des2$: Khoảng cách giữa hai lần rò ga liên tiếp không dưới 30 giây. Yêu cầu an toàn $Req$ được biểu diễn bằng công thức LDI: $$60 \le \ell < \infty \implies 19 \int Leak - \int Nonleak \le 0$$
  • Bài toán kiểm chứng: Định nghĩa hình thức quan hệ $\sigma \models D$ và $\mathcal{A} \models D$ cho hai lớp công thức LDP và LDI, xác lập bài toán tìm thuật toán quyết định $\mathcal{A} \models D$.

Chương 3: Kiểm chứng mô hình với kỹ thuật qui hoạch tuyến tính

Chương 3 xây dựng kỹ thuật kiểm chứng bằng cách đưa về giải một họ các bài toán quy hoạch tuyến tính:

  • Biểu thức chính quy thời gian (TRE): Định nghĩa đệ quy TRE với phần tử nguyên thủy $(s, [a, b])$, các toán tử nối, cộng $\oplus$, lặp $*$, và toán tử hợp song song $\otimes$ (yêu cầu $state(R_1) \cap state(R_2) = \emptyset$). Minh họa qua hệ chắn tàu gồm Bộ giám sát (trạng thái $A, B, C, P$) và Bộ điều khiển (trạng thái $U, MD, Dn, MU$). Với điều kiện tàu qua giao lộ mất ít nhất $a$ đơn vị thời gian ($B \to C$), khoảng cách giữa hai đoàn tàu ít nhất $b$ đơn vị thời gian ($P$), thời gian hạ cổng không quá $c$ đơn vị thời gian ($MD$), hệ thống được mô tả bằng biểu thức chính quy song song $R_{CM}$. Điều kiện an toàn $c \le a$ tương ứng với kiểm chứng LDI: $0 \le \ell < \infty \implies \int C - \int Dn \le 0$.
  • Xây dựng bài toán quy hoạch tuyến tính: Định nghĩa TRE hữu hạn (không chứa $*$) và TRE đơn giản (hữu hạn và không chứa $\oplus$). Với mỗi TRE đơn giản $R$, xây dựng hệ ràng buộc tuyến tính $C(R)$ và hàm mục tiêu $\theta(R)$. Chứng minh tồn tại song ánh giữa tập mô hình $\mathcal{M}(R)$ và tập nghiệm của $C(R)$. Kiểm chứng $R \models D$ tương đương với việc giải bài toán cực đại hóa $\max \theta(R)$ thỏa mãn $C(R)$ và $A \le \ell(R) \le B$, sau đó so sánh giá trị tối ưu với $M$.
  • Thuật toán chuyển đổi: Định nghĩa các hàm cận thời gian $m(R), M(R)$ và cận ngữ cảnh $m(R', R), M(R', R)$. Thiết lập các định lý về tính $D$-tương đương ($R_1 \equiv_D R_2$). Đưa ra thuật toán khử toán tử lặp $*$ và khử biểu thức rỗng $\Lambda$, chuyển một TRE vô hạn về hợp hữu hạn của các TRE đơn giản.
  • Đánh giá phương pháp: Phương pháp giải quyết được cho lưới ôtômat song song nhưng có nhược điểm là làm bùng nổ số lượng bài toán quy hoạch tuyến tính khi cận đồng hồ và cận trên khoảng quan sát lớn, đồng thời vẫn bị giới hạn trong ngữ nghĩa quan sát từ thời điểm $t = 0$.

Chương 4: Kỹ thuật rời rạc hoá và duyệt đồ thị đạt được

Chương 4 trình bày đóng góp lý thuyết quan trọng nhất của luận án:

  • Tính rời rạc hoá được và phép nguyên hóa: Tác giả xây dựng khái niệm nguyên hóa mô hình, chuyển đổi mô hình liên tục $\sigma$ trên $\mathbb{R}^+$ thành mô hình nguyên $\sigma'$ trên $\mathbb{N}$. Chứng minh định lý nền tảng: với công thức LDP và LDI trong ngữ nghĩa tổng quát (khoảng $[b, e]$ bất kỳ), hệ thống thỏa mãn công thức trên tập mô hình liên tục $\mathcal{M}(\mathcal{A})$ khi và chỉ khi nó thỏa mãn trên tập mô hình nguyên $\mathcal{M}_{uv}(\mathcal{A})$.
  • Đồ thị vùng đạt được nguyên ($RG$): Xây dựng cấu trúc đồ thị $RG$ từ kỹ thuật phân vùng đồng hồ, bổ sung việc khôi phục khoảng cách thời gian nguyên cực tiểu và cực đại trên các cung chuyển tiếp, bảo toàn tính chất thời khoảng.
  • Kiểm chứng LDP: Chứng minh tính tương đương giữa $\mathcal{M}(\mathcal{A})$ và $\mathcal{M}_{uv}(\mathcal{A})$ đối với LDP. Thiết lập đồ thị trọng số $G$ từ $RG$. Thuật toán 4.2 chuyển bài toán kiểm chứng LDP về bài toán tìm đường đi ngắn nhất (hoặc dài nhất) trên đồ thị trọng số $G$ thông qua thuật toán Warshall-Floyd. Độ phức tạp tính toán của thuật toán này tương đương với độ phức tạp của kiểm chứng các tính chất thời điểm thông thường.
  • Kiểm chứng LDI và tính quyết định được: Xây dựng đồ thị trọng số $G$ phục vụ LDI. Thiết kế Thuật toán 4.3 (kiểm chứng LDI với đỉnh xuất phát cố định) và Thuật toán 4.4 (kiểm chứng LDI tổng quát). Từ thuật toán duyệt trên đồ thị hữu hạn này, tác giả chứng minh khẳng định: lớp công thức bất biến khoảng tuyến tính (LDI) đối với ôtômat thời gian là quyết định được (decidable) trong ngữ nghĩa tổng quát.
  • Kiểm chứng thực nghiệm: Áp dụng kiểm chứng tính an toàn của hệ chắn tàu và mô hình thử nghiệm DATA1; kết quả được lượng hóa qua các bảng số liệu thực nghiệm.
Thuật toán / Dữ liệu thực nghiệm Tên gọi và vị trí trong luận án Nội dung kỹ thuật và chức năng
Thuật toán 4.1 Xây dựng đồ thị đạt được nguyên Khôi phục khoảng cách thời gian nguyên cực tiểu và cực đại của các phép chuyển từ đồ thị vùng
Thuật toán 4.2 Kiểm chứng tính thoả của $G$ đối với LDP Ứng dụng thuật toán Warshall-Floyd tìm đường đi có trọng số trên đồ thị $G$ để quyết định LDP
Thuật toán 4.3 Kiểm chứng LDI với đỉnh xuất phát cố định Duyệt đồ thị trọng số phục vụ kiểm chứng bất biến khoảng tuyến tính từ một đỉnh xác định
Thuật toán 4.4 Kiểm chứng LDI tổng quát Duyệt toàn diện đồ thị đạt được nguyên; chứng minh tính quyết định được của LDI tổng quát
DATA1 Mô hình thử nghiệm (Bảng A.1 – A.5) Mô hình kiểm thử thực nghiệm đồ thị vùng đạt được nguyên và bảng kết quả kiểm chứng LDP, LDI
Hệ chắn tàu Kiểm chứng thực nghiệm (Bảng A.6 – A.8) Đồ thị vùng và bảng kết quả kiểm chứng an toàn cho hệ chắn tàu với các tham số $a=b=c=1$

Kết quả và những đóng góp mới

Luận án tự xác định các đóng góp học thuật mới về mặt lý thuyết và thực tiễn như sau:

  1. Biểu diễn và kiểm chứng lưới ôtômat bằng quy hoạch tuyến tính: Đề xuất phương pháp mô hình hóa dáng điệu song song của lưới ôtômat thời gian thực bằng biểu thức chính quy thời gian (TRE) có toán tử hợp song song $\otimes$. Xây dựng thuật toán khử toán tử lặp $*$ và toán tử $\oplus$ để đưa biểu thức vô hạn về hợp hữu hạn của các TRE đơn giản, từ đó quy bài toán kiểm chứng LDP và LDI về việc giải họ hữu hạn các bài toán quy hoạch tuyến tính.
  2. Chứng minh tính rời rạc hoá được trong ngữ nghĩa tổng quát: Chứng minh toán học khẳng định lớp công thức tính chất khoảng tuyến tính (LDP) và bất biến khoảng tuyến tính (LDI) có tính rời rạc hoá được đối với khoảng quan sát thời gian $[b, e]$ bất kỳ ($0 \le b \le e < \infty$). Kết quả này phá vỡ rào cản của các nghiên cứu trước đây vốn chỉ áp dụng cho quan sát bắt đầu từ gốc thời gian $t = 0$.
  3. Thuật toán kiểm chứng LDP hiệu quả: Xây dựng cấu trúc đồ thị trọng số hướng đến LDP và đề xuất thuật toán kiểm chứng dựa trên thuật toán tìm đường đi Warshall-Floyd. Phương pháp này đạt độ phức tạp tính toán tương đương với các thuật toán kiểm chứng tính chất thời điểm đã có.
  4. Khẳng định tính quyết định được của LDI: Đề xuất cấu trúc đồ thị vùng đạt được nguyên và thiết kế thuật toán duyệt đồ thị hữu hạn (Thuật toán 4.4), qua đó chứng minh lớp công thức bất biến khoảng tuyến tính (LDI) là quyết định được trong ngữ nghĩa tổng quát đối với ôtômat thời gian.
  5. Đóng góp thực tiễn: Cài đặt thành công bộ chương trình kiểm chứng mô hình thử nghiệm (mô tả trong Phụ lục A), thực nghiệm kiểm chứng tính đúng đắn trên mô hình hệ bếp ga và hệ thống điều khiển chắn tàu với các bộ tham số cụ thể ($a = b = c = 1$).

Hạn chế và hướng nghiên cứu tiếp

Hạn chế của luận án:

  • Phương pháp quy hoạch tuyến tính ở Chương 3 làm phát sinh số lượng bài toán tối ưu hóa rất lớn khi cận đồng hồ của ôtômat hoặc cận thời gian của công thức khoảng có giá trị lớn.
  • Kỹ thuật xây dựng đồ thị vùng đạt được nguyên ở Chương 4 tuy đã thu hẹp không gian trạng thái so với miền liên tục nhưng vẫn chịu ảnh hưởng của hiện tượng bùng nổ không gian trạng thái khi số lượng đồng hồ $k$ tăng lên (số vùng bị chặn bởi hàm giai thừa $k! \cdot 2^k$).
  • Hệ thống chỉ khảo sát trên các ôtômat thời gian có đồng hồ tăng đều cùng vận tốc; chưa mở rộng cho các hệ thống lai (hybrid automata) có vận tốc biến thiên phức tạp.

Hướng nghiên cứu tiếp được tác giả đề xuất:

  • Tối ưu hóa cấu trúc dữ liệu cho đồ thị đạt được nguyên bằng cách kết hợp kỹ thuật biểu diễn ký hiệu BDD và kỹ thuật kiểm chứng trực tiếp trong quá trình sinh trạng thái (on-the-fly).
  • Nghiên cứu mở rộng các thuật toán kiểm chứng dựa trên tính rời rạc hóa cho các hệ thống thời gian thực phức tạp hơn như ôtômat lai hoặc mạng Petri thời gian thực.
  • Hoàn thiện và nâng cấp bộ chương trình thử nghiệm trong Phụ lục A thành công cụ kiểm chứng mô hình hoàn chỉnh, tối ưu hóa bộ nhớ để xử lý các hệ thống thực tế có quy mô công nghiệp.

Giá trị tham khảo

Luận án là tài liệu tham khảo chuyên sâu phục vụ các đối tượng:

  • Nghiên cứu sinh, học viên cao học và giảng viên: Chuyên ngành Khoa học máy tính, Đảm bảo toán học cho máy tính và hệ thống tính toán, và Phương pháp hình thức (Formal Methods). Các chương 2, 3, 4 cung cấp hệ thống chứng minh toán học hoàn chỉnh về mối liên hệ giữa lý thuyết ôtômat, biểu thức chính quy và Lôgic khoảng.
  • Kỹ sư thiết kế hệ thống thời gian thực và hệ thống nhúng an toàn cao: Trong các lĩnh vực điều khiển giao thông đường sắt, hàng không, viễn thông và thiết bị y tế. Luận án cung cấp quy trình mô hình hóa hình thức từ khâu đặc tả yêu cầu an toàn thời gian đến khâu kiểm chứng tự động bằng thuật toán.
  • Phần nội dung có giá trị tham khảo cao nhất: Kỹ thuật phân rã và khử toán tử trong biểu thức chính quy thời gian (Chương 3); chứng minh toán học tính rời rạc hóa được và các thuật toán duyệt đồ thị trọng số nguyên 4.1 – 4.4 (Chương 4); tài liệu thuật ngữ đối chiếu Anh – Việt và kiến trúc cài đặt bộ kiểm chứng (Phụ lục A).

Câu hỏi thường gặp

1. Điểm khác biệt bản chất giữa tính chất thời điểm và tính chất thời khoảng trong kiểm chứng hệ thời gian thực là gì?
Tính chất thời điểm (point property) chỉ xem xét việc hệ thống có đạt tới một trạng thái nào đó tại một thời điểm cụ thể hay không (ví dụ tính đạt được kiểm tra qua TCTL). Ngược lại, tính chất thời khoảng (duration property) xem xét tổng thời gian tích lũy mà hệ thống lưu lại ở một hoặc nhiều trạng thái trong suốt một đoạn quan sát (ví dụ tỷ lệ thời gian rò rỉ của bếp ga hoặc hiệu số thời gian giữa tàu qua đường ngang và cổng hạ). Việc kiểm chứng tính chất thời khoảng phức tạp hơn do phải kiểm tra trên vô hạn các khoảng thời gian quan sát $[b, e]$ khác nhau.

2. Tại sao phương pháp quy hoạch tuyến tính ở Chương 3 bị hạn chế khi áp dụng cho hệ thống lớn?
Phương pháp quy hoạch tuyến tính yêu cầu phân rã biểu thức chính quy thời gian vô hạn về hợp của các biểu thức chính quy đơn giản bằng cách khử toán tử lặp $*$ và toán tử $\oplus$. Quá trình này sinh ra một số lượng rất lớn các bài toán quy hoạch tuyến tính phụ thuộc trực tiếp vào độ lớn của cận đồng hồ và cận trên độ dài quan sát trong công thức, dẫn tới bùng nổ khối lượng tính toán.

3. Ý nghĩa lý thuyết của việc chứng minh "tính rời rạc hoá được" trong Chương 4 là gì?
Tính rời rạc hoá được chứng minh rằng một công thức LDP hoặc LDI đúng trên mô hình thời gian thực liên tục $\mathbb{R}^+$ khi và chỉ khi nó đúng trên mô hình thời gian rời rạc $\mathbb{N}$. Kết quả này cho phép chuyển bài toán kiểm chứng từ không gian trạng thái vô hạn trên miền thực về duyệt trên đồ thị vùng đạt được nguyên hữu hạn trạng thái mà vẫn bảo toàn tính đúng đắn của kết luận.

4. Yêu cầu an toàn của hệ chắn tàu (Railroad Crossing) được kiểm chứng bằng công thức nào?
Hệ chắn tàu an toàn khi thời gian đoàn tàu chiếm dụng đoạn đường giao nhau không vượt quá thời gian cổng chắn ở vị trí đóng. Yêu cầu này được đặc tả bằng công thức bất biến khoảng tuyến tính (LDI): $$0 \le \ell < \infty \implies \int C - \int Dn \le 0$$ Hệ thống được chứng minh là an toàn khi và chỉ khi tham số thời gian hạ cổng $c$ nhỏ hơn hoặc bằng thời gian tối thiểu tàu chạy từ vị trí cảnh báo tới điểm giao cắt $a$ ($c \le a$).

5. Luận án đã giải quyết câu hỏi mở nào về mặt lý thuyết đối với Lôgic khoảng?
Trước thời điểm luận án công bố, tính quyết định được (decidability) của lớp công thức bất biến khoảng tuyến tính (LDI) trên ôtômat thời gian đối với ngữ nghĩa quan sát tổng quát $[b, e]$ bất kỳ vẫn chưa có lời giải. Luận án đã trả lời khẳng định câu hỏi này bằng việc đề xuất thuật toán duyệt đồ thị đạt được nguyên (Thuật toán 4.4) có khả năng kết thúc sau số hữu hạn bước để quyết định tính thỏa mãn của công thức LDI.

Kết luận

Luận án của tác giả Phạm Hồng Thái đã giải quyết trọn vẹn bài toán kiểm chứng tự động các tính chất thời khoảng của hệ thời gian thực trong ngữ nghĩa tổng quát thông qua hai hướng tiếp cận: quy hoạch tuyến tính trên biểu thức chính quy thời gian và duyệt đồ thị vùng đạt được nguyên dựa trên tính rời rạc hóa được. Công trình đã đóng góp các kết quả lý thuyết có giá trị học thuật cao, tiêu biểu là việc chứng minh tính quyết định được của lớp bất biến khoảng tuyến tính (LDI) và đề xuất thuật toán kiểm chứng tính chất khoảng tuyến tính (LDP) với độ phức tạp tối ưu. Các thuật toán đề xuất đều được kiểm chứng tính đúng đắn thông qua việc cài đặt bộ công cụ phần mềm thực nghiệm trên các bài toán an toàn kinh điển. Luận án là công trình nghiên cứu hoàn chỉnh, đặt nền tảng phương pháp luận vững chắc cho hướng nghiên cứu kiểm chứng mô hình hệ thời gian thực tại Việt Nam.