Divide & Conquer Approach to Model Checking
Addressing the state space explosion issue in model checking, this work by Canh Minh Do, Yati Phyo, and Kazuhiro Ogata introduces a divide & conquer approach focusing on until and until stable properties. The research extends techniques to handle these properties effectively, emphasizing mitigation of state space explosion. Concepts like Kripke structures, path notations, and Linear Temporal Logic (LTL) are discussed to enhance understanding.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
A Divide & Conquer Approach to Until and Until Stable Model Checking Canh Minh Do, Yati Phyo and Kazuhiro Ogata Japan Advanced Institute of Science and Technology (JAIST) {canhdominh,yatiphyo,ogata}@jaist.ac.jp Presented online at the 34th International Conference on Software Engineering & Knowledge Engineering July 1 - 10, 2022 Pittsburgh, USA
1 Outline Introduction Background Core idea A divide & conquer approach to until model checking A divide & conquer approach to until stable model checking Conclusion & future work
2 Introduction Model checking is one of the most successful formal verification techniques to verify that a finite-state system satisfies its desired properties. However, the state space explosion is the most annoying problem in model checking. To mitigate the problem, our research group has proposed a divide & conquer approach to model checking leads-to, conditional stable, and eventual properties. In this work, we extend our technique to handle until and until stable properties.
3 Kripke structure
4 Path notations
5 Path notations
6 Linear temporal logic (LTL) The syntax of linear temporal logic (LTL) is as follows: where ? ?. next connective (or operator) until connective (or operator)
7 Linear temporal logic (LTL) Some other connectives (or operators) are defined as follows: eventually connective always connective leads-to connective
8 Linear temporal logic (LTL)
9 Core idea We have proposed a divide & conquer approach to until and until stable model checking that aim at mitigating the state space explosion in model checking as: until properties expressed as ?1 ? ?2 until stable properties expressed as ?1 ? ?2 where ?1 and ?2are state propositions.
10 Core idea The techniques divide the reachable state space from each initial state into multiple layers, generating multiple sub-state spaces, and checking a smaller model checking problem for each sub-state space. If each sub-state space is much smaller than the original reachable state space, the state space explosion problem may be mitigated.
11 Core idea For each initial state ??0 ?, an infinite tree is made by using ?. ??0 1st layer ??1 The infinite tree is split into ? + 1 layers. Let ? be the function defined as follows: ? 0 = 0 ? ? is a non-zero natural number (the depth of layer ?) for ? = 1, ,? ? ? + 1 = ??? 1 ?th layer ??? ??= ? 0 + + ?(?) is the depth of states located at layer ? for ? = 0,1, ,?. ??? ?? is the Kripke structure obtained from ? by doing as follows: deleting all transitions from each state adding the self-transition to each state at the depth ?? for ? = 1, ,?. ?+1st layer
12 A divide & conquer approach to until model checking
13 A divide & conquer approach to until stable model checking
14 A divide & conquer approach to until stable model checking
15 Conclusion & future work Conclusion: We have described a divide & conquer approach to until and until stable model checking that aim at mitigating the state space explosion in model checking. Future work: Developing a support tool for the technique. Conducting experiments for real-time and hybrid systems specified in RT- Maude to demonstrate the usefulness of the technique/tool.
