ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
NGUYỄN TÀI TUẤN
KIỂM CHỨNG CÁC TÍNH CHẤT THỜI GIAN THỰC
CHO HỆ THỐNG ĐỒNG THỜI BẰNG RT - SPIN
LUẬN VĂN THẠC SĨ NGÀNH CÔNG NGHỆ THÔNG TIN Hà Nội, 2013 ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Lời cảm ơn i
Lời cam đoan ii
MỤC LỤC iii
Danh mục hình vẽ v
Danh mục ký hiệu, từ viết tắt vi
Chƣơng 1: Mở đầu 1
Chƣơng 2 Cơ sở kiểm chứng mô hình 3
2.1 Kiểm chứng dựa trên mô hình 3
2.1.1 Khái niệm 3
2.1.2 Các bƣớc thực hiện 5
2.2 Ngôn ngữ Promela và Spin 5
2.2.1 Ngôn Ngữ Promela 5
2.2.2 Spin 7
2.3 Giới thiệu về hệ thống thời gian thực 11
2.3.1 Khái niệm 11
2.3.2 Đặc điểm của hệ thống thời gian thực 12
2.3.3 Cấu tạo hệ thời gian thực 13
2.3.4 Vì sao chọn hệ thời gian thực 13
2.4 Kết luận 13
Chƣơng 3 - Otomat thời gian 15
3.1 Giới thiệu 15
3.2 Otomat ω 16
3.3 Otomat thời gian 18
3.3.1 Ngôn ngữ thời gian 19
3.3.2 Bảng chuyển trạng thái với các ràng buộc thời gian 20
3.3.3 Các ràng buộc đồng hồ và đồng hồ biên dịch 22
3.3.4 Các bảng chuyển trạng thái thời gian 22
3.3.5 Ngôn ngữ hình thức thời gian 23
iv
v
Danh mục bảng biểu
Bảng 2.1: Khả năng thực hiện của các câu lệnh trong Promela
Bảng 3.1: Các loại Otomat thời gian
Bảng 3.2: Các loại otomat ω
Danh mục hình vẽ
Hình 2.1 : Vấn đề với kiểm thử
Hình 2.2 : Kiểm thử mô hình
Hình 3.1 : Otomat Buchi chấp nhận (a+b)
*
a
ω
Hình 3.2 : Otomat Muller xác định chấp nhận (a+b)
*
a
ω
Hình 3.3 : Ví dụ bảng chuyển trạng thái thời gian
Hình 3.4 : Bảng chuyển trạng thái thời gian với 2 đồng hồ (đồng hồ)
Hình 3.5 : Otomat Buchi thời gian chấp nhận L
crt
Hình 3.6 : Otomat thời gian mô hình hóa hành vi lặp định kỳ
Hình 3.7 : Otomat thời gian chấp nhận ngôn ngữ L
converge
Spin tích hợp thời gian rời rạc
RtSpin
Real Time Spin
Spin tích hợp thời gian thực
LTL
Linear time logic
Logic thời gian tuyến tính
TS
Transition system
Hệ thống chuyển trạng thái
RTS
Real Time System
Hệ thống thời gian thực
TBA
Timed Buchi Automata
Otomat Buchi thời gian
MTA
Muller Timed Automata
Otomat Muller thời gian
DTMA
Deterministic Timed Muller
Automata
Otomat Muller thời gian xác định
DTBA
Deterministic Timed Buchi
Automata
Otomat Buchi thời gian xác định
TTS
Timed transition system
Hệ thống chuyển trạng thái theo
tƣơng thích với thuật toán giảm số lƣợng không gian trạng thái của hệ thống. Tuy
nhiên DtSpin chỉ mở rộng với thời gian rời rạc.
Nội dung nghiên cứu: Tìm hiểu Spin, hệ thống thời gian thực, lý thuyết Otomat thời
gian và tích hợp thời gian với công cụ Spin.
Phần đầu của luận văn ta nghiên cứu về Spin, hệ thống thời gian thực và lý thuyết mô
hình kiểm chứng. Ta cũng đƣa ra những khái niệm cơ bản về kiểm chứng mô hình và
hệ thống thời gian thực là cơ sở nên tảng để thực hiện tích hợp và các công cụ tích hợp
thời gian thực với Spin nhằm định lƣợng khoảng thời gian giữa các sự kiện và các
ràng buộc về thời gian. Hai công cụ này dựa trên lý thuyết Otomat thời gian. Trong đó
RtSpin dựa trên mô hình thời gian liên tục, DtSpin dựa trên mô hình thời gian rời rạc.
Cuối cùng ta đƣa ra một số thực nghiệm với công cụ RtSpin và DtSpin bao gồm: mô
2
hình train-gate-controller đƣợc đặc tả trong phần lý thuyết Otomat thời gian, bài toán
này là bài toán kinh điển và là tiền đề để kiểm chứng các hệ thổng điều khiển giao
thông. Tiếp đến ta cũng kiểm chứng giáo thức truyền nhận song song dựa trên các
kênh truyền và gửi thông thông báo có thể mất mát thông tin. Cuối cùng mô hình Sapi
là mô hình có giá trị thực tiễn của hệ thống tính cƣớc của G-Mobile
Cấu trúc luận văn: Luận văn gồm các phần: 4 chƣơng, kết luận và tài liệu tham
khảo. Các phần còn lại của luận văn có cấu trúc nhƣ sau:
Chƣơng 2: Đầu tiên ta tìm hiểu Cơ sở lý thuyết cho kiểm chứng mô hình, một
công nghệ tự động trong đó mô hình với tập trạng thái hữu hạn của hệ thống và một
tính chất logical, hệ thống sẽ kiểm tra xem tính chất đó. Spin một công cụ kiểm chứng
mô hình. Spin là công cụ nhằm phân tích tính logic của hệ thống đồng thời, các giao
thức giao tiếp dữ liệu. Hệ thống đƣợc mô hình hóa bởi ngôn ngữ Promela. Tiếp đến ta
cũng trình bày các hệ thống thời gian thực.
Chƣơng 3: Atomat thời gian mô hình hóa các hành vi hệ thống thời gian thực.
Cung cấp các định nghĩa, đồ thị chuyển trạng thái với ràng buộc thời gian sử dùng
nhiều đồng hồ giá trị thực. Otomat thời gian chấp nhận chấp nhận từ ký tự và thời gan
– trình tự vô hạn với giá trị thời gian liên kết với ký tự vào. Chúng ta cung xem xét
Gries, Hoare, Owicki, Manna and Plueni. Kiểm chứng là một mô hình lý thuyết và
đƣợc thực hiện dựa trên khả năng tính toán của máy tính [4].
Trong quá trình phát triển phần mềm, càng phát hiện ra lỗi sớm thì việc phát
triển sẽ dễ dàng hơn. Tuy nhiên, việc phát hiện lỗi nhờ kiểm chứng thƣờng rất muộn.
Một giải pháp nhằm cải thiện, chúng ta nên thực hiện kiểm chứng để có thể phát hiện
lỗi sớm hơn. Hình 2.1: Vấn đề với kiểm chứng
Requirement
Analyis
System
Design
Operation
And Mantenance
Acceptance
Testing
System
Testing
Program Design
Unit and Integration
thiết kế. Mô hình không chỉ tốt trong gỡ lỗi mà còn tìm lỗi bugs rất sớm trong việc
thiết kế một hệ thống mới.
Các bƣớc thực hiện xây dƣng Kiểm chứng mô hình. Đầu tiên ta mô hình hóa hệ
thống (xây dựng mô hình M cho hệ thống). Tiếp đến ta xây dựng yêu cầu dƣới dạng
Mô hình M
Byte n
Property anp()
do
od
Property Φ
[] (n <5)
Model Checker
YES
Tính chất
thỏa mãn
No +
Vêt lỗi
5
biểu thức Ф. Cuối cùng ta quyết định (deciding) và các thuật toán kiểm tra (đƣợc thực
hiện trong các công cụ kiểm chứng mô hình).
2.1.2 Các bước thực hiện
Quá trình kiểm chứng dựa trên mô hình đƣợc bắt đầu bằng việc xác định yêu
cầu của hệ thống từ đó xây dựng mô hình dựa vào các yêu cầu và chức năng của hệ
thống. Việc xây dựng mô hình còn phải dựa trên các yếu tố dữ liệu đầu vào và đầu ra.
Mô hình này đƣợc sử dụng để sinh ra các ca kiểm thử. Chúng ta có thể biết kết quả
đầu ra mong đợi từ mô hình hoặc từ quy định chuẩn (oracle). Khi chạy kịch bản và kết
quả thu đƣợc sẽ đƣợc so sánh với kết quả mong đợi. Từ đó quyết định hành động tiếp
theo nhƣ sửa đổi mô hình hoặc dừng kiểm thử,…
Các bƣớc để thực hiện kiểm thử dựa trên mô hình. Xây dựng mô hình dựa trên
ngay lập tức hoặc không thực hiện đƣợc. Tất cả các câu lệnh là nguyên tử và khi thực
hiện không giao với các tiến trình khác. Để kiểm chứng các tính chất chắc chắn đúng
trong chƣơng trình thƣờng dùng lệnh assert (expr) trong mô hình Promela. Lệnh này
luôn thực hiện đƣợc và nếu biểu thức trả vê 0 thì Spin thông báo một lỗi “has been
violated” [12].
mtype = {MSG, ACK}
chan toS = …
chang toR = …
bool flag;
proctype Sender() {
…
}
Init {
…
}
Hình 2.3: Mô hình promela.
Phần thân tiến trình
Khởi tạo các tiến trình
7
Cú pháp của promela tổng kết nhƣ Bảng sau:
Lệnh
Thực thi
n=1;
printf("Process P, n=%d\n",n);
}
active proctype Q()
{
n=2;
printf("Process Q, n=%d\n",n);
}
Spin là công cụ kiểm tra mô hình kiểm thử tính chất trong dó M là mô hình của
hệ thống với số trạng thái hữu han và Φ là tính chất cần kiểm thử đƣợc quy định dƣới
dạng một số ký hiệu hình thức.
8
Với Spin có thể kiểm tra những loại tính chất: khóa chết (Deadlocks) là trạng
thái có một tiến trình chiếm hữu tài nguyên lâu dài làm cho các tiến trình có nhu cầu
sử dụng tài nguyên này luôn ở trạng thái đợi mãi mãi hay còn gọi trạng thái kết thúc
không hợp lệ, tính khẳng định (assertions) là cách đơn giản để kiểm tra chƣơng trình.
Một assertion là một mệnh đề đƣợc đặt trong 1 chƣơng trình mà ta cho rằng mệnh đề
sẽ luôn đúng tại vị trí đó. Spin sẽ tính toán các assertion trong quá trình tìm kiếm phản
ví dụ trong không gian trạng thái của chƣơng trình, code không đạt đƣợc (unreachable
code) là cách kiểm tra có những đoạn mã lệnh trong tiến trình nhƣng không bao giờ
đƣợc thực hiện, công thức LTL, tính chất sống động (liveness properties). Tính chất
sống động bao gồm: không có vòng lặp tiến trình (non-progress cycles) và vòng lặp
chấp nhận đƣợc (acceptance cycles). Khi kiểm tra tính chất không có vòng lặp tiến
trình, bộ kiểm chứng sẽ cảnh báo nếu có một thực hiện không đi qua vô hạn lần trạng
thái tiến trình. Trong đó trạng thái tiến trình là trạng thái hệ thống mà một số tiến trình
đang thực hiện lệnh đƣợc gán nhãn với tiền tố "progress". Khi kiểm tra tính chất có
vòng lặp chấp nhận đƣợc, bộ kiểm chứng sẽ cảnh báo nếu có một thực hiện đi qua vô
hạn lần trạng thái chấp nhận đƣợc. Trong đó trạng thái chấp nhận đƣợc là trạng thái hệ
thống mà một số tiến trình đang thực hiện lệnh đƣợc gán nhãn với tiền tố
- Nhiệt độ của phản ứng không bao giờ quá 100 độ C.
- Bất kì lúc nào chìa khóa xe chƣa vặn tới vị trí khởi động, xe sẽ không nổ
máy.
Liveness (tính sống động): Tính liveness của một chƣơng trình đảm bảo rằng
nó có thể thực thi đƣợc một chức năng “tốt” nào đó đã đặt ra. (“something
good will happen eventually”).
Thuộc tính liveness có thể đƣợc biểu diễn bằng các phép kết hợp AF hoặc F
trong temporal logic:
F done
G (req → F grant)
G F tick
trong LTL.
Ví dụ:
- Khi chìa khóa xe vặn tới vị trí khởi động, xe sẽ nổ máy.
- Bóng đèn sẽ chuyển sang màu xanh
Fairness (tính công bằng) Tính công bằng đảm bảo rằng nếu một sự kiện nào
đó ở trạng thái sẵn sàng đƣợc thực thi thì đến một lúc nào đó nó sẽ đƣợc thực
thi.
Thuộc tính công bằng có thể đƣợc biểu diễn bằng các toán tử AF và phép suy
ra:
AG (san_sang=0 → AF thuc_thi=0)
AG (san_sang=1→ AF thuc_thi =1)
10
Một ví dụ cho tính công bằng trong một hệ thống truyền-nhận tin là khi một
gói tin đƣợc gửi đi thì đến một lúc nào đó nó sẽ đến đƣợc đích.
Trong Spin ta chỉ cần biểu diễn tính chất của hệ thống dƣới dạng một biểu thức
LTL sau đó đƣa vào Spin với lênh spin và tham số -f, Spin sẽ tự động chuyển biểu
thức LTL sang cấu trúc never claim của Promela dùng vào việc kiểm chứng.
Chẳng hạn
nhãn “accept” thì bộ kiểm chứng sẽ cảnh bảo mã lỗi “never claim”. Ở ví dụ trên hệ
thống cần thỏa mãn rằng biến divisor luôn phải lớn hơn 0, do vậy trƣờng hợp ngƣợc
lại không bao giờ đƣợc xảy ra hay !(a)luôn phải nhận giá trị false.
11
Nhãn To_init đảm bảo trong khi chƣơng trình đƣợc chạy (và sinh ra các trạng
thái), cho đến khi nào A còn đúng, lệnh goto thứ hai luôn luôn đƣợc chọn và Spin sẽ
liên tục.
Nhƣng nếu chƣơng trình tính toán đến một trạng thái mà ở đó A sai, Spin nhảy
tới nhãn accept_all và kết thúc chƣơng trình.
SPIN sử dụng thuật toán tìm kiếm theo độ sâu (depth first search algorithm DFS)
để tạo và thực hiên không gian trạng thái đầy đủ [11].
Procedure dfs(s: state) {
If error(s)
ReportError();
Foreach (successor t of s) {
If (t not in Statespace)
Dfs(t);
} Hình 2.4: Thuật toán tìm kiếm không gian trạng thái trong Spin
Mỗi trạng thái đƣợc biểu diễn bởi một vector trạng thái là thông tin nhằm xác
định trạng thái hệ thống, bao gồm: Các biến toàn cục, nội dung của các kênh. Trong
đó với mỗi kênh trong hệ thống chứa Các biến cục bộ và Bộ đếm tiến trình.
2.3 Giới thiệu về hệ thống thời gian thực
2.3.1 Khái niệm
Trong các tài liệu cũng nhƣ trong thực tế, khái niệm thời gian thực và hệ thống
thời gian thực không phải lúc nào cũng đƣợc hiểu một cách thống nhất. Nhiều ngƣời
thuật xử lý ngắt của hệ thống phần cứng.
Một hệ thống realtime đƣợc hiểu là một hệ thống làm việc với các sự kiện tức
thời (realtime). Tuy nhiên không phải mọi hệ thống đều có thể thực hiện đƣợc những
qui định tức thời hay đáp trả lại sự kiện một cách tức thời nhƣ chúng ta mong muốn.
Khi bắt tay xây dựng các ứng dụng phần mềm chúng ta luôn mong muốn thời gian trễ
để đƣa ra một lệnh hay một quyết định là nhỏ nhất, hay khi xây dựng các ứng dụng
phần cứng chúng ta lại muốn thời gian đƣa ra một tín hiệu đáp trả một sự kiện là phải
gần nhƣ tức thời, nhƣng sự thực không đƣợc nhƣ vậy vì các hệ thống đáp ứng sự kiện
bao giờ cũng có một thời gian trễ nhất định. Khái niệm “hệ thống thời gian thực”,ở
đây hiểu ngầm nhƣ một hệ thống đáp ứng sự kiện với một thời gian trễ chấp nhận
đƣợc hay nói cách khác, hệ thời gian thực là hệ thống có các ràng buộc về thời gian
đối với các hành động của hệ thống.
2.3.2 Đặc điểm của hệ thống thời gian thực
Tính bị động: hệ thống phải phản ứng với các sự kiện xuất hiện vào các thời
điểm thƣờng không biết trƣớc. Ví dụ: Sự vƣợt ngƣỡng của một giá trị đo, sự thay đổi
trạng thái của một thiết bị quá trình phải dẫn đến các phản ứng trong bộ điều khiển.
Tính nhanh nhạy: Hệ thống phải xử lý thông tin một cách nhanh chóng để có thể đƣa
ra kết quả phản ứng một cách kịp thời. Tuy tính nhanh nhạy là một đặc điểm tiêu biểu
nhƣng một hệ thống có tính năng thời gian thực không nhất thiết phải có đáp ứng thật
nhanh mà quan trọng hơn là phải có phản ứng kịp thời đối với các yêu cầu, tác động
bên ngoài.
Tính đồng thời: hệ thống phải có khả năng phản ứng và xử lý đồng thời nhiều sự
kiện diễn ra. Có thể cùng một lúc bộ điều khiển đƣợc yêu cầu thực hiện nhiều vòng
13
điều chỉnh, giám sát ngƣỡng giá trị nhiều đầu vào, cảnh giới trạng thái làm việc của
một số động cơ.
Tính tiền định: Dự đoán đƣợc thời gian phản ứng tiêu biểu, thời gian phản ứng
chậm nhất cũng nhƣ trình tự đƣa ra các phản ứng. Nếu một bộ điều khiển phải xử lý
đồng thời nhiều nhiệm vụ ta phải tham gia quyết định đƣợc về trình tự thực hiện các
trạng thái và kiểm tra có thể đƣợc thực hiện một cách tự động bằng phần mềm và Spin
là một trong những bộ kiểm chứng (model checker) đƣợc sử dụng rộng rãi. Các bộ
kiểm chứng không kiểm tra trực tiếp chƣơng trình mà kiểm tra một mô hình là thể
hiện mức cao của hệ thống. Mô hình này mô tả hành vi của hệ thống. Để áp dụng
đƣợc các công cụ kiểm chứng mô hình, việc đầu tiên là phải xây dựng mô hình của hệ
thống. Các mô hình này cùng với đặc tả của thuộc tính cần kiểm tra là đầu vào của các
bộ kiểm chứng.
Chƣơng này ta cũng giới thiệu về hệ thống thời gian thực. Ở phần sau chúng ta
sẽ tìm hiểu sâu về otomat thời gian để mô hình hóa và kiểm chứng hệ thống thời gian
thực. 15
Chương 3 - Otomat thời gian
3.1 Giới thiệu
Chúng ta giới thiệu otomat thời gian để mô hình hóa hành vi của hệ thống thời
gian thực theo thời gian. Các định nghĩa đƣợc cung cấp một cách đơn giản nhƣng
mạnh mẽ, chú giải đồ thị chuyển trạng thái với các ràng buộc thời gian sử dụng các
đồng hồ giá trị thực. Otomat thời gian chấp nhận các từ ký tự theo thời gian – thời
gian với giá trị thực đƣợc liên kết với mỗi kí tự [1].
Trong mô hình thời gian tuyến tính với giả thiết một thực hiện hoàn toàn có thể
đƣợc mô hình hóa bởi trình tự các trạng thái của các sự kiện của hệ thống hay còn gọi
là excution trace (hoặc trace). Hành vi của hệ thống là tập trình tự thực hiên. Hơn nữa
tập các trình tự là ngôn ngữ hình thức nên dẫn đến sử dụng otomat trong việc đặc tả và
kiểm chứng hệ thống. Nếu hệ thống là hữu hạn trạng thái sẽ tƣơng ứng với otomat hữu
dày đặc (dense-time) otomat hữu hạn không thích hợp. Thay thế ta phát triển lý thuyết
ngôn ngữ hình thức thời gian và otomat thời gian nhằm ứng dụng cho hệ thống nhƣ
vậy.
Otomat thời gian chấp nhận các từ thời gian (timed words) – trình tự vô hạn các
sự kiện, mỗi sự kiện tƣơng ứng với một ký tự và thời gian giá trị thực. Otomat thời
gian là otomat với tập hữu hạn các đồng hồ giá trị thực (real-valued đồng hồs). Đồng
hồ có thể đƣợc thiết lập lại 0 với các bƣớc chuyển trạng thái của otomat hay theo dõi
thời gian trôi kể từ lần cuối đƣợc thiết lập. Các bƣớc chuyển của otomat bao gồm ràng
buộc giá trị đồng hồ (clock values): một thực hiện có thể đạt đƣợc nếu giá trị hiện tại
của đồng hồ thỏa mãn các ràng buộc liên kết. Vì vậy ta có thể mô hình tính chất thời
gian chẳng hạn “kênh chuyển tiếp thông báo trong 3 đên 5 đơn vị thời gian kể từ khi
nhận”. Otomat thời gian mô hình hóa hệ thống thời gian thực và duy trì các tính chất
thời gian thực: đặc điểm tính chất nhƣ tính sống động, tính công bằng và không xác
định; đặc điểm số lƣợng nhƣ : tính tuần hoàn, biên và độ trễ thời gian
Ta xem xét tính xác định và không xác định với otomat Buchi và otomat Muller.
Ta cũng chỉ ra otomat thời gian không xác định đóng với phép hợp và giao nhƣng
không đóng với phép bù. Tính chất đóng cho lớp otomat thời gian xác định tƣơng tự
với otomat không chứa thời gian: otomat Muller thời gian xác định đóng với tất các
phép boolean trong khi đó otomat Buchi thời gian xác định đóng chỉ với các phép
Boolean tích cực. Vì vậy otomat Muller thời gian xác định khả năng diễn đạt ngôn
ngữ kém hơn so với otomat không xác định.
Cuối cúng ta áp dụng lý thuyết otomat thời gian để chứng minh tính đúng đắn
của các hệ thống thời gian thực với trạng thái hữu hạn.
3.2 Otomat ω
Trong phần này ta giới thiệu các khía cạnh liên quan của lý thuyết ngôn ngữ hình
thức ω.
Định nghĩa quen thuộc của ngôn ngữ hình thức là một tập các từ hữu hạn bởi các
chữ cái, ngƣợc với hữu hạn là các từ không hữu hạn. Vì vậy ngôn ngữ ω qua tập các
ký tự hữu hạn ∑ tà tập hơn con của ∑
ω
Các loại Otomat ω khác nhau đƣợc định nghĩa bằng cách thêm điều kiện chấp
nhận đƣợc đến định nghĩa của các bảng chuyển trạng thái (transition tables). Otomat
Buchi A là một bảng chuyển (∑,S,S
0
, E) với tập thêm vào F S là các trạng thái
chấp nhận đƣợc. Một thực hiện r của Otomat A trên từ σ Є ∑
ω
là thực hiện chấp nhận
đƣợc nếu nhƣ inf(r) Λ F Ø. Mặt khác một thực hiện r đang chấp nhận nếu một số
trạng thái từ tập F xuất hiện vô hạn lần trên thực hiện r. Ngôn ngữ L(A) của Otomat A
bao gồm các từ σ Є ∑
ω
để A có một thực hiện chấp nhận đƣợc trên từ σ
Ví dụ 3.1: Xem xét Otomat bao gồm 2 trạng thái của Hình 3.1 qua ký tự {a,b}.
Trạng thái s
0
là trạng thái khởi tạo, s1 là trạng thái chấp nhận. Tất cả các thực hiện của
Otomat có dạng
r: s0
1
s1
2
s2
3
Lớp các ngôn ngữ hình thức ω là đóng dƣới dạng phép toán Boolean. Ngôn ngữ
đƣợc thực hiện bởi xây dựng Otomat Buchi.
Buchi Otomat đƣợc sử dụng để mô hình các tiến trình đồng thời hữu hạn trạng
thái. Vấn đề kiểm thử suy dẫn đến vấn đề ngôn ngữ. Để kiểm tra liệu ngôn ngữ của
Otomat đƣợc chứa trong Otomat kia, chúng ta kiểm tra có phải là tập rỗng giao của
a
a
a,b
S0
S1
18
hai Otomat gồm Otomat gốc và Otomat bù. Kiểm tra tính rỗng là đơn giản, ta chỉ cần
tìm kiếm một chu kỳ đạt đƣợc từ trạng thái khởi tạo và bao gồm ít nhất một trạng thái
chấp nhận đƣợc. Tuy nhiên bổ sung cho Otomat Buchi là vấn đề bùng nổ tăng đột
biến số trạng thái. Liệu ngôn ngữ của Otomat đƣợc chứa trong ngôn ngữ của Otomat
đa định có thể đƣợc thực hiện trên thời gian đa thức.
Một bảng chuyển A = bộ (∑,S,S
0
, E) là đơn định nếu (i) có trạng thái khởi tạo
duy nhất |S
0
| = 1 và (ii) số các cung đƣợc gán nhãn a bắt đầu tại s nhiều nhất là 1 cho
tất cả các trạng thái s Є S và cho tất cả các ký tự a Є ∑ , Vì vậy bảng chuyển xác định,
trạng thái hiện tại và ký tự đầu vào kế tiếp xác định duy nhất trạng thái kế tiếp. Kết
quả Otomat đơn định có nhiều nhất một thực hiện cho một từ. Không giống nhƣ
Otomat với từ hữu hạn, lớp các ngôn ngữ đƣợc đƣợc chấp nhận bởi Otomat Buchi xác
định sẽ ít hơn lớp các ngôn ngữ hình thức ω. Trong ví dụ 2.1 không có Otomat Buchi
chấp nhận ngôn ngữ L
0.
Trong phần này ta định nghĩa các từ thời gian (timed word) bằng cách nhóm giá
trị thời gian thực với mỗi ký tự trong từ. Khi đó ta định nghĩa Otomat ω để chấp nhận
a
a
b
b
S0
S1
19
từ thời gian và sử dụng chúng để phát triển lý thuyết ngôn ngữ hình thức thời gian đến
lý thuyết của ngôn ngữ hình thức ω.
3.3.1 Ngôn ngữ thời gian
Ta định nghĩa từ thời gian cho một hành vi của hệ thống thời gian thực tƣơng
ứng với từ thời gian trên các ký tự của sự kiện. Nhƣ trong trƣờng hợp mô hình của
thời gian liên tục, tập các số thực dƣơng, R, đƣợc chọn là miền thời gian. Một từ σ
đƣợc nhóm với trình tự thời gian đƣợc định nghĩa nhƣ sau [6].
Định nghĩa 3.1: Trình tự thời gian = 12 . là một trình tự vô hạn các giá trị
thời gian với >0 và thỏa mãn các ràng buộc sau:
1. Tính đơn điệu: tăng đơn điệu nghĩa là
i
<
i+1
2. Tiến trình: cho mọi t Є R thì tồn tại i 1 để
i
> t
Một từ thời gian với các ký tự (σ, ) đƣợc xem nhƣ đầu vào của Otomat biểu
diễn σ
i
đƣợc cho nhƣ sau
L2 ={((ab)
ω
, ) | . ((
2i
-
2i-1
) < (
2i+2
-
2i+1
)) (3.2)
Các toán tử lý thuyết ngôn ngữ chẳng hạn phép giao, hợp, bù đƣợc định nghĩa
cho ngôn ngữ thời gian áp dụng nhƣ ngôn ngữ không có thời gian. Thêm vào đó ta
định nghĩa toán tử Untime. Phép toán này lƣợc bỏ thời gian đƣợc liên kết với các ký
tự, hay phép chiếu của vết thời gian (σ, ) trên thành phần σ
Định nghĩa 3.2 Cho một ngôn ngữ thời gian L trên ∑, Untime(L) là ngôn ngữ ω
bao gồm σ Є ∑
ω
sai cho (σ, ) Є L theo trình tự thời gian .
Copyright: Tài liệu đại học ©