On Improvement of Assume-Guarantee Verification Method for Timed Component-Based Software

The Assume-guarantee verification using TL* algorithm implemented in Learner is an important method to alleviate the state space explosion problem in model checking of timed systems, thanks to its divide and conquer strategy. This paper presents an improvement for TL* learning algorithm of Learner by removing the first phase from the verification process and starting learning assumption from λ. This improvement reduces the time complexity and covers a number of cases where assumptions exist while the original TL* algorithm cannot. Besides, this paper adds a kind of bound to the candidate query answering algorithm of Teacher for it to return “don't know” result and prevent Learner from running endlessly. We give some discussions related to both of original algorithms and the improved ones in the paper.