We devised the L+1-layer divide & conquer approach to leads-to model checking (L+1-DCA2L2MC) and its parallel version, and developed sequential and parallel tools for L+1-DCA2L2MC. In a temporal logic called UNITY, designed by Chandy and Misra, the leads-to temporal connective plays an important role and many case studies have been conducted in UNITY, demonstrating that many systems requirements can be expressed as leads-to properties. Hence, it is worth dedicating to these properties. Counterexample generation is one of the main tasks in the L+1-DCA2L2MC technique that can be optimized to improve its running performance. This article proposes a technique to find all counterexamples at once in model checking with a new model checker. Furthermore, layer configuration selection is essential to make the best use of the L+1-DCA2L2MC technique. This work also proposes an approach to finding a good layer configuration for the technique with an analysis tool. Some experiments are conducted to demonstrate the power and usefulness of the two optimization techniques, respectively. Moreover, our sequential and parallel tools are compared with SPIN and LTSmin model checkers, showing a promising way to mitigate the state space explosion and improve the running performance of model checking when dealing with large state spaces.
@article{CanhTosem23,author={Do, Canh Minh and Phyo, Yati and Riesco, Adri\'{a}n and Ogata, Kazuhiro},title={Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way},year={2023},issue_date={November 2023},publisher={Association for Computing Machinery},address={New York, NY, USA},volume={32},number={6},issn={1049-331X},journal={ACM Transactions on Software Engineering and Methodology},month=sep,articleno={151},numpages={38},keywords={state space explosion, master-worker model, Leads-to properties, parallel model checking, Maude}}
Information
A Layered and Parallelized Method of Eventual Model Checking
Termination or halting is an important system requirement that many systems should satisfy and can be expressed in linear temporal logic as eventual properties. We devised a divide-and-conquer approach to eventual model checking in order to reduce the state space explosion in model checking. The idea of the technique is to split an original model checking problem for eventual properties into multiple smaller model checking problems and handle each smaller one. Due to the nature of the divide-and-conquer approach, each smaller model checking problem can essentially be tackled independently. Hence, this paper proposes a parallel technique/tool based on a master–worker pattern for the divide-and-conquer approach to model checking eventual properties. We carry out some experiments to show the effectiveness of our parallel technique/tool, which can somewhat enhance the running performance to a certain extent when conducting model checking for eventual properties.
@article{YatiInfo23,author={Phyo, Yati and Aung, Moe Nandi and Do, Canh Minh and Ogata, Kazuhiro},title={A Layered and Parallelized Method of Eventual Model Checking},journal={Information},volume={14},year={2023},number={7},article-number={384},url={https://www.mdpi.com/2078-2489/14/7/384},issn={2078-2489}}
2022
DSA
A Tool for Model Checking Eventual Model Checking in a Stratified Way
@inproceedings{MoeDsa22,author={Aung, Moe Nandi and Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},title={A Tool for Model Checking Eventual Model Checking in a Stratified
Way},booktitle={9th International Conference on Dependable Systems and Their Applications,
{DSA} 2022},pages={270--279},publisher={{IEEE}},year={2022},timestamp={Mon, 26 Jun 2023 20:48:49 +0200},biburl={https://dblp.org/rec/conf/dsa/AungPDO22.bib},bibsource={dblp computer science bibliography, https://dblp.org}}
SEKE
A divide and conquer approach to until and until stable model checking
@inproceedings{CanhSeke22,author={Minh Do, Canh and Phyo, Yati and Ogata, Kazuhiro},editor={Peng, Rong and Pantoja, Carlos Eduardo and Kamthan, Pankaj},title={A divide and conquer approach to until and until stable model checking},booktitle={34th International Conference on Software Engineering and Knowledge
Engineering, {SEKE} 2022},pages={388--393},publisher={{KSI} Research Inc.},year={2022},timestamp={Mon, 26 Jun 2023 20:48:16 +0200},biburl={https://dblp.org/rec/conf/seke/DoPO22.bib},bibsource={dblp computer science bibliography, https://dblp.org}}
IEEE Access
Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way
@article{Canh2Access22,author={Minh Do, Canh and Phyo, Yati and Ogata, Kazuhiro},title={Sequential and Parallel Tools for Model Checking Conditional Stable
Properties in a Layered Way},journal={{IEEE} Access},volume={10},pages={133749--133765},year={2022},timestamp={Mon, 26 Jun 2023 20:53:40 +0200},biburl={https://dblp.org/rec/journals/access/DoPO22.bib},bibsource={dblp computer science bibliography, https://dblp.org}}
2021
COMPSAC
A support tool for the L + 1-layer divide & conquer approach to leads-to model checking
@inproceedings{YatiIctac21,author={Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},editor={Cerone, Antonio and {\"{O}}lveczky, Peter Csaba},title={A Divide {\&} Conquer Approach to Conditional Stable Model Checking},booktitle={Theoretical Aspects of Computing - 18th International
Colloquium, ICTAC 2021},series={Lecture Notes in Computer Science},volume={12819},pages={105--111},publisher={Springer},year={2021},timestamp={Wed, 01 Sep 2021 12:53:42 +0200},biburl={https://dblp.org/rec/conf/ictac/PhyoDO21.bib},bibsource={dblp computer science bibliography, https://dblp.org}}
ISSSR
A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties
Canh Minh Do, Yati Phyo, Adrián Riesco, and Kazuhiro Ogata
In 7th International Symposium on System and Software Reliability, ISSSR 2021, Sep 2021
@inproceedings{CanhIsssr21,author={Minh Do, Canh and Phyo, Yati and Riesco, Adrián and Ogata, Kazuhiro},title={A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties},booktitle={7th International Symposium on System and Software Reliability, ISSSR 2021},year={2021},volume={},number={},pages={155-166},}
Computer Journal
A Divide & Conquer Approach to Leads-to Model Checking
@article{YatiCJ21,author={Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},title={A Divide \& Conquer Approach to Leads-to Model Checking},journal={The Computer Journal},publisher={Oxford University Press},year={2021},}
Mathematics
A Divide & Conquer Approach to Eventual Model Checking
@article{MoeMath21,author={Aung, Moe Nandi and Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},title={A Divide \& Conquer Approach to Eventual Model Checking},journal={Mathematics},year={2021},volume={9},number={4},article-number={368},url={https://www.mdpi.com/2227-7390/9/4/368},issn={2227-7390}}
2019
ICAIT
Toward development of a tool supporting a 2-layer divide & conquer approach to leads-to model checking
@inproceedings{YatiIcait19,author={Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},divide\&conquerapproachtoleads-tomodelchecking},booktitle={3rd International Conference on Advanced Information Technologies, ICAIT 2019},pages={250-255},year={2019},}