Speaker: Miaomiao Zhang
Abstract: Assume guarantee reasoning (AGR), is a kind of technique to address the state explosion problem associated with model checking. However, obtaining the appropriate assumption for AGR is always a challenge, especially in the case of timed systems. In this work, we propose a learning-based compositional verification framework for deterministic timed automata. Within the framework, a modified learning algorithm is employed to automatically construct the assumption in the form of a deterministic one-clock timed automaton, and an effective scheme is implemented to obtain the clock reset information for the assumption learning. We prove the correctness and termination of the framework and present two kinds of improvements to speed up the verification.