Trình bày phương pháp sử dụng qui hoạch tuyến tính để phục vụ kiểm chứng, trong đó hệ thống được biểu diễn bởi biểu thức chính quy theo thời gian và đưa ra thuật toán kiểm chứng dựa trên lớp các biểu thức chính quy mở rộng. Luận án chỉ ra những ưu điểm và mặt hạn chế của phương pháp qui hoạch tuyến tính, từ đó đề nghị sử dụng phương pháp duyệt đồ thị vùng đạt được, bằng cách khôi phục lại khoảng cách thời gian của các phép chuyển. Trên cơ sở đồ thị đạt được, và tính rời rạc hoá được của các công thức, các đồ thị trọng số sẽ được xây dựng và thuật toán duyệt được tiến hành trên các đồ thị này. Phương pháp này tỏ ra hữu hiệu khi tiến hành kiểm chứng LDP, và cung cấp câu trả lời về tính quyết định được của tính chất LDI
