A Divide and Conquer Approach to Eventual Model Checking

Mathematics

MoeNandi Aung¹  Yati Phyo²  Kazuhiro Ogata²  CanhMinh Do² 

[1] Faculty of Information Science, University of Information Technology (UIT), Hlaing Township, Yangon PO 11052, Myanmar;School of Information Science, Japan Advanced Institite of Science and Technology (JAIST), Nomi, Ishikawa 923-1292, Japan;

关键词: eventual property;    model checking;    Maude;   

DOI  :  10.3390/math9040368

来源: DOAJ

【 摘 要 】

The paper proposes a new technique to mitigate the state of explosion in model checking. The technique is called a divide and conquer approach to eventual model checking. As indicated by the name, the technique is dedicated to eventual properties. The technique divides an original eventual model checking problem into multiple smaller model checking problems and tackles each smaller one. We prove a theorem that the multiple smaller model checking problems are equivalent to the original eventual model checking problem. We conducted a case study that demonstrates the power of the proposed technique.

【 授权许可】

Unknown