Divide & Conquer Approach to Model Checking
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.jpPresented online at the 34
th
International Conference on Software Engineering
& Knowledge Engineering
July 1 - 10, 2022 – Pittsburgh, USA
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
1
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.
2
Kripke structure
3
Path notations
4
Path notations
5
Linear temporal logic (LTL)
The syntax of linear temporal logic (LTL) is as follows:
6
n
ext connective (or operator)
u
ntil connective (or operator)
Linear temporal logic (LTL)
Some other connectives (or operators) are defined as
follows:
7
eventually connective
always
connective
leads-to connective
Linear temporal logic (LTL)
8
9
Core idea
10
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.
Core idea
11
Core idea
1st layer
12
A divide & conquer approach to
until model checking
A divide & conquer approach to
until stable model checking
13
14
A divide & conquer approach to
until stable model checking
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.
15
Conclusion & future work
Thank you for your attention!
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.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
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.
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.
