đại học quốc gia hà nội
trường đại học công nghệ
Phạm Hồng Thá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
luận án tiến sĩ toán học
Hà Nội - 2005
đại học quốc gia hà nội
trường đại học công nghệ
Phạm Hồng Thá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
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ố : 1.01.10
luận án tiến sĩ toán học
người hướng dẫn khoa học
1 : TS. Đặng Văn Hưng
2 : PGS. TS. Đinh Mạnh Tuờng
Hà Nội - 2005
Mục lục
Lời cam đoan iv
Lời cảm ơn v
Mục lục vi
Danh mục từ viết tắt vii
Danh mục bảng và thuật toán viii
Danh mục hình vẽ ix
Tóm tắt nội dung x
1 Kiểm chứng mô hình và hệ thời gian thực 1

4.1.1 Tập mô hình DC của ôtômat thời gian 53
4.1.2 Khái niệm -nguyênhoávàmộtvàitínhchất 56
4.1.3 Tính rời rạc hoá được của các công thức LDP, LDI . . . 60
4.1.4 Đồthịvùngđạtđượcnguyên 61
4.2 Kiểm chứng công thức LDP 66
4.2.1 Tính tương đương của M(A) và M
uv
(A) đối với LDP . 66
4.2.2 Đồ thị trọng số G phục vụ kiểm chứng LDP 68
4.2.3 Thuật toán kiểm chứng LDP 70
4.3 Kiểm chứng công thức LDI 72
4.3.1 Quan hệ giữa lớp mô hình M
uv
(A) và đồ thị đạt được
RG hướngtớiLDI 73
4.3.2 Đồ thị trọng số G phục vụ kiểm chứng LDI 76
4.3.3 Thuật toán kiểm chứng LDI 81
4.3.4 Kiểm chứng tính an toàn của hệ chắn tàu bằng rời rạc hoá 84
Kết luận 85
Danh mục công trình của tác giả 88
Tài liệu tham khảo 89
Phụ lục 95
Phụ lục A. Bộ kiểm chứng mô hình LDP, LDI 95
Phụ lục B. Công thức và kí hiệu 118
Phụ lục C. Thuật ngữ Anh - Việt 119
Danh mục từ viết tắt
BDD : Binary Decision Diagram (Sơ đồ biểu diễn nhị phân)
CTL : Computational Tree Logic (Lôgic cây tính toán)
DC : Duration Calculus (Lôgic khoảng)
FTA : Finitary Timed Automaton (Ôtômat thời gian hữu hạn)

x
=2, c
y
=1 17
2.2 Ôtômatthờigian 19
2.3 Một mô hình của DC. 23
3.1 Hệchắntàu 30
3.2 Một dáng điệu của hệ chắn tàu. 32
4.1 Mô hình DC của ôtômat thời gian. 54
4.2 Các lớp mô hình của ôtômat thời gian A 55
4.3 Một trường hợp nguyên hoá mô hình σ với b

= b và e

= e . 60
4.4 Đồ thị vùng đạt được nguyên RG 66
4.5 Đồ thị trọng số G phục vụ kiểm chứng LDP. 69
4.6 Đồ thị trọng số G từ đồ thị vùng đạt được RG. 78
4.7 Đường đi trong đồ thị trọng số G 79
4.8 Ôtômatđạtđượccủahệchắntàu. 84
xi
Tóm tắt nội dung
Với những thành công của đặc tả hình thức, kiểm chứng mô hình thời gian
thực đã đóng góp nhiều phương pháp, thuật toán, cấu trúc dữ liệu và trên cơ
sở đó cung cấp nhiều bộ công cụ kiểm chứng mô hình cho phép kiểm tra tự
động tính đúng đắn của hệ thống. Tuy nhiên cho đến hiện nay, các thuật toán
phục vụ kiểm chứng tính chất thời khoảng vẫn còn rời rạc và hạn chế, chủ yếu
chỉ đối với các lớp con của ôtômat thời gian và các công thức khoảng được xét
với ngữ nghĩa thu hẹp.
Từ đó, luận án này đặt vấn đề quan sát và thiết kế các thuật toán kiểm

là hết sức khó khăn, đặc biệt là đối với các hệ thống thời gian thực mà việc
kiểm tra chúng (một cách chặt chẽ) chỉ mới được phát triển trong khoảng hơn
10 năm trở lại đây. Phần lớn các khó khăn trong kiểm tra đến từ việc chưa
có một phương pháp nhất quán để mô tả hệ thống, dẫn tới cách hiểu về hệ
thống một cách chung chung, mơ hồ, không tạo được nền tảng để xây dựng
những kỹ thuật kiểm tra thống nhất và từ đó dẫn tới cách thức kiểm tra không
hữu hiệu, thiếu tính thuyết phục. Do vậy gần đây, các phương pháp hình thức
đã ra đời và được phát triển ngày càng mạnh mẽ, đạt được nhiều thành tựu.
Trên nền tảng đó các ngôn ngữ đặc tả hệ thống cũng như các phương pháp,
1
Ví dụ nguyên nhân vụ nổ tên lửa Arian 5 vào ngày 4 tháng 6 năm 1996 đã được xác
định do một lỗi nhỏ của phần mềm tính toán chuyển động của tên lửa ([24]).
1
2
kỹ thuật kiểm tra đã được xây dựng và ngày càng chứng minh tính hiệu quả
của chúng. Đặc biệt, một trong các phương pháp kiểm tra như vậy được gọi
là kiểm chứng mô hình đã sản sinh ra các bộ kiểm chứng cho phép tiến hành
kiểm tra hệ thống một cách hoàn toàn tự động. Từ đó, các bộ kiểm chứng
ngày càng đóng vai trò quan trọng, được sử dụng rộng rãi và phục vụ đắc lực
cho công việc kiểm tra, vốn nhiều khó khăn, đòi hỏi nhiều thời gian trở nên
ngày càng dễ dàng, nhanh, chính xác và hiệu quả hơn.
Trong chương này - thay cho lời nói đầu - chúng tôi tóm tắt một cách ngắn
gọn các kết quả, phương pháp đã có cũng như một số hạn chế còn tồn tại
trong lĩnh vực kiểm chứng mô hình của các hệ thời gian thực, từ đó đưa đến
cái nhìn ban đầu về mục đích và những lý giải về tính cần thiết của đề tài.
Phần cuối cùng của chương chúng tôi trình bày về nội dung chính của luận
án, và các kết quả luận án đã đạt được trong việc giải quyết mục tiêu đề ra.
1.1 Đặc tả và kiểm tra hệ thống
Để kiểm tra tính đúng đắn của hệ thống, trước hết hệ thống phải được đặc tả
một cách rõ ràng và nhất quán. Đặc tả là quá trình mô tả hệ thống và các tính

của hệ thống và về mặt nguyên tắc bài toán coi như đã được giải quyết.
Có thể phân biệt 2 hướng tiếp cận nêu trên bằng ví dụ nhỏ là bài toán
SAT, tức kiểm tra tính thoả của một công thức f trong lôgic mệnh đề. Bằng
phương pháp chứng minh định lý từ hệ tiên đề của lôgic mệnh đề và các luật
dẫn ta có thể dẫn được về ¬f hoặc không để kết luận tính thoả của f.Cách
giải quyết thứ hai là dùng kiểm chứng mô hình liệt kê từng bộ giá trị của các
biến mệnh đề sơ cấp có trong f, qua mỗi bộ giá trị được liệt kê này tính đúng,
sai của f sẽ được kiểm chứng để quyết định tính thoả của công thức.
Qua ví dụ nêu trên có thể thấy được ưu điểm của phương pháp kiểm chứng
mô hình so với phương pháp chứng minh định lý. Thứ nhất, một phương pháp
kiểm chứng như vậy có thể được thể hiện thành các bộ kiểm chứng mô hình
với các đầu vào là hệ thống S, tính chất P và đầu ra là câu trả lời "đúng"
4
hoặc "sai" (hình 1.1), từ đó việc kiểm tra được tự động hoá hoàn toàn. Thứ
hai, một bộ kiểm chứng mô hình là có khả năng chỉ ra bộ giá trị thoả mãn
công thức f, điều này ở một mặt khác cũng đồng nghĩa kiểm chứng mô hình
có thể chỉ ra nơi xảy ra lỗi của hệ thống. Vì vậy, ngoài câu trả lời đúng/sai
mà bộ kiểm chứng mô hình cung cấp, chúng ta cũng thường dùng chúng như
công cụ phát hiện, phục vụ cho gỡ lỗi trong quá trình thiết kế.
Hình 1.1: Sơ đồ bộ kiểm chứng mô hình.
Thách thức về mặt kỹ thuật trong kiểm chứng mô hình chính là thuật toán
và cấu trúc dữ liệu để giải quyết bài toán bùng nổ không gian trạng thái, tức
số lượng trạng thái thường tăng theo hàm mũ đối với số thành phần hợp thành
của hệ thống. Để khắc phục, một số kỹ thuật đã ra đời như on-the-fly
2
, cùng
với cấu trúc dữ liệu hợp lý, đã tỏ ra rất hiệu quả đối với các hệ hữu hạn trạng
thái và hiện nay nhiều bộ kiểm chứng đã cho phép chúng ta điều khiển được
các hệ thống với không gian trạng thái rất lớn
Tóm lại, trong khoảng hơn hai thập kỷ trở lại đây các phương pháp hình

công trình khác đã được thực hiện trên các lôgic mở rộng của lôgic thời gian
tuần tự như Computational Tree Logic (CTL), Propositional Linear Temporal
Logic (PLTL) ([24]).
Hướng tiếp cận thứ hai là dựa vào bài toán kiểm tra tính rỗng của ngôn
ngữ ([7, 46]). Theo hướng tiếp cận này, tính chất P cũng được thể hiện bởi
một ôtômat. Nếu ngôn ngữ L(S) được sinh bởi S là chứa trong ngôn ngữ L(P)
3
chúng tôi tạm dịch từ "temporal" là "thời gian tuần tự", cũng như "real-time" là "thời
gian thực", vì khái niệm "temporal" chỉ cung cấp ý nghĩa thứ tự (về mặt thời gian) xảy ra
của các trạng thái thay vì thời điểm chính xác xảy ra các trạng thái đó như trong khái niệm
"real-time".
6
được sinh bởi P thì S thoả P. Mặt khác, do L(S) ⊆L(P) ⇔L(S ׬P)=∅
nên có thể chuyển bài toán trên về bài toán kiểm tra tính rỗng của ngôn ngữ
và nó đã được giải quyết trong [42] đối với ôtômat không thời gian.
Một kỹ thuật quan trọng trong kiểm chứng mô hình là kỹ thuật biểu diễn
bằng kí hiệu (symbolic model checking), với đặc trưng chính là biểu diễn mọi
thành phần của bài toán (trạng thái, phép chuyển, tính chất) thông qua các
kí hiệu đại diện. Kỹ thuật này cho phép sử dụng các sơ đồ biểu diễn nhị phân
(Binary Decision Diagram - BDD) với dữ liệu được cài đặt tốn rất ít bộ nhớ
và các phép toán trên nó được thực hiện một cách rất hữu hiệu. Trên cơ sở
này năm 1992 Clarke và McMillan đã xây dựng bộ kiểm chứng mô hình SMV
(Symbolic Model Verifier) cho phép kiểm chứng các hệ thống với số lượng trạng
thái lên đến 10
20
trạng thái ([48]).
Một số bộ kiểm chứng mô hình ra đời trong giai đoạn đầu điển hình như
SMV, SPIN ([48, 34]) với các tính chất được đặc tả bởi lôgic thời gian tuần tự
được chúng tôi tạm gọi là kiểm chứng mô hình cổ điển để phân biệt với hướng
kiểm chứng mô hình thời gian thực sau này.

thời gian. Tuy vậy, hiện nay nhiều bộ kiểm chứng mô hình thời gian thực cũng
đã ra đời mà tiêu biểu là HyTech, KRONOS, UPPAAL ([38, 16, 13]), hoặc áp
dụng các bộ kiểm chứng không thời gian (như SPIN) để phục vụ kiểm chứng
tính chất thời gian thực ([21]) cũng đang được nghiên cứu.
Tư tưởng phổ biến của các bộ kiểm chứng thời gian thực về cơ bản là duyệt
trên đồ thị vùng (region graph) để kiểm tra tính đạt được của các trạng thái
nào đó của ôtômat thời gian ([7, 8]). Vì số lượng các vùng là rất lớn nên một
số biện pháp thu gọn đã được đề nghị. Ví dụ, có thể kết hợp nhiều vùng tạo
thành miền (zones) dựa trên các kỹ thuật mô phỏng (simulation), trừu tượng
hoá (abstract) [55, 61], hoặc phương pháp thứ tự bộ phận (partial orders) [49]
lược bỏ bớt các phép chuyển đan xen thừa trong hợp các thành phần, kết
hợp song song với tối ưu hoá cấu trúc dữ liệu [47]. Các kỹ thuật symbolic và
on-the-fly cũng được áp dụng ([14, 40]), từ đó các bộ kiểm chứng thời gian
thực thường xuyên được cải tiến và ngày càng hữu hiệu hơn.
8
Kiểm chứng mô hình với các tính chất khoảng
Các tính chất thời gian của một hệ thống có thể xuất hiện dưới nhiều dạng
khác nhau, trong đó các tính chất thời điểm là những tính chất chỉ quan tâm
đến sự xuất hiện của các trạng thái còn các tính chất thời khoảng là những
tính chất quan tâm không những đến việc xuất hiện mà còn cả khoảng thời
gian xuất hiện của những trạng thái này. Ví dụ tính đạt được của một trạng
thái p hay các tính chất được biểu diễn trong lôgic TCTL là các tính chất
thời điểm còn các tính chất như "tổng thời gian xảy ra của trạng thái p không
được lớn hơn tổng thời gian xảy ra của trạng thái q" như đã được nhắc đến ở
trên, là một trong những tính chất khoảng như vậy.
Để dễ hình dung, chúng ta nhắc lại một ví dụ kinh điển đã được nghiên
cứu vào đầu thập kỷ trước, đó là hệ bếp ga. Một thiết kế bếp ga được gọi là
an toàn nếu khoảng thời gian rò ga của nó là không quá dài. Mô hình đơn giản
của bếp được xét với 2 trạng thái rò ga và không rò ga và yêu cầu về tính an
toàn của hệ thống được phát biểu: "tỉ lệ thời gian rò ga không quá một phần

đặt ra với các công thức khoảng được viết trong DC. Tuy nhiên, ở đây đã gặp
một khó khăn lớn đó là tính quyết định được của lớp các công thức khoảng là
rất thấp. Như đã chỉ ra trong [35], nhiều lớp công thức đơn giản trong lôgic
là không quyết định được, từ đó thậm chí việc tìm ra các lớp công thức quyết
định được là có ý nghĩa. Ví dụ các tác giả trong [51] đã chỉ ra tính quyết định
được của một lớp công thức mở rộng trong DC với mô hình thời gian rời rạc.
Một yếu tố dẫn đến tính quyết định được thấp của các công thức trong
DC, cũng như tính bùng nổ không gian trạng thái trong kiểm chứng tính chất
khoảng đó là các quan sát hệ thống phải được tiến hành trong những khoảng
thời gian bất kỳ. Nói cách khác, bản chất của các tính chất thời điểm trong
khi có thể được quyết định bởi toàn bộ đường chạy xuất phát từ thời điểm ban
đầu (0) và kết thúc tại một thời điểm chuyển trạng thái nào đó thì tính chất
khoảng lại được quyết định bởi vô hạn khoảng quan sát bất kỳ trên đường
chạy này. Đặc trưng này góp phần làm tăng cao độ phức tạp của hệ thống và
gây nhiều khó khăn trong việc thiết kế thuật toán kiểm chứng chúng.
4
ProCoS: Provably Correct Systems. Dự án thuộc chương trình ESPRIT được tài trợ bởi
Cộng đồng Châu Âu (CEC), nghiên cứu về đặc tả hình thức các hệ thời gian thực.
10
Với những khó khăn nêu trên, cho đến hiện nay kết quả về kiểm chứng
tính chất thời khoảng là vẫn còn hạn chế. Hầu hết các kết quả trong thập kỷ
vừa qua kể từ lần đầu tiên Zhou Chaochen (1991) giới thiệu về DC ([18]) cho
đến nay đều tập trung trên các hạn chế của lớp các ràng buộc tuyến tính.
Đây là lớp tính chất quan trọng hay gặp trong thực tế và được nhiều tác giả
quan tâm. Ví dụ trong [45] các tác giả đã chứng minh bài toán kiểm chứng các
tính chất này là quyết định được đối với ôtômat thời gian hữu hạn (Finitary
Timed Automata - FTA) bằng việc đưa bài toán kiểm chứng về việc giải một
tập các bài toán qui hoạch nguyên. Tuy nhiên, trong bài báo này các tác giả
đã phải hạn chế chỉ xét lớp công thức với các hệ số ràng buộc lấy giá trị trên
tập số nguyên (Z). Trong [19], các tác giả đã xét công thức dưới dạng tổng

án.
Hầu hết các kết quả được nhắc đến ở trên đều được thực hiện từ dự án
DeTfoRS
5
được hỗ trợ bởi Viện Công nghệ phần mềm quốc tế của trường Đại
học Liên hợp quốc tại Macau (UNU/IIST) và luận án này được hoàn thành
trên cơ sở các phương pháp được nghiên cứu tại UNU/IIST dưới sự hướng dẫn
tận tình của TS. Đặng Văn Hưng - một thành viên của dự án - cũng như sự
giúp đỡ nhiệt tình của các thành viên khác. Ngoài ra luận án còn nhận được
sự hổ trợ của đề tài 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" dưới sự chủ trì của PGS. TS. Hồ Sĩ Đàm,
Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội.
1.3 Mục đích và kết quả của luận án
Mục đích của luận án
Với tình hình kiểm chứng mô hình như đã được trình bày tóm tắt ở trên, một
vấn đề hiện nay vẫn còn đang được tiếp tục giải quyết đó là xây dựng các bộ
kiểm chứng cho các tính chất thời khoảng của các hệ thời gian thực. Như đã
biết hầu hết các công thức khoảng là không quyết định được nên sẽ không
5
DeTfoRS: Design Techniques for Real-Time Systems.
/>12
thể xây dựng được một bộ kiểm chứng mô hình cho toàn bộ mà chỉ có thể
xây dựng các bộ kiểm chứng mô hình bộ phận cho một số lớp công thức đặc
trưng của hệ lôgic. Các lớp công thức như vậy đã được kể đến như các bất biến
khoảng tuyến tính, tính chất khoảng tuyến tính và một vài lớp con khác. Tuy
nhiên, chúng tôi cũng nhận thức được rằng việc xây dựng một bộ kiểm chứng
hoàn chỉnh (hữu hiệu, độ phức tạp thấp) đòi hỏi nhiều thời gian và là công
sức của cả một tập thể nghiên cứu mạnh. Vì vậy luận án cũng chỉ đặ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ơ 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.
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].
2.1 Mô hình thời gian
2.1.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

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 | ϕ ∧ ϕ
ởđâyx, 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ượclạitakí
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.1.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
16

3. ∀x ∈ X và ν(x) ≤ c
x
thì fr(ν(x)) = 0 khi và chỉ khi fr(ν

(x)) = 0
Gọi k là số đồng hồ trong X. Quan hệ
∼
=
có các tính chất sau.
Tính chất 1.
∼
=
là một quan hệ tương đương trên tập các thể hiện đồng hồ.
Kí hiệu [ν] là lớp tương đương của ν xác định bởi quan hệ
∼
=
và được gọi
là vùng đồng hồ (chứa ν). 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ừđótacótínhchấ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ồ.
Tính chất 3. Số vùng đồng hồ là hữu hạn và bị chặn bởi k!2
k

x∈X
(2c
x
+2).
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 đó.