A Divide and Conquer Approach to Eventual Model Checking

Moe Nandi Aung, Yati Phyo, Canh Minh Do and Kazuhiro Ogata
Additional contact information
Moe Nandi Aung: Faculty of Information Science, University of Information Technology (UIT), Hlaing Township, Yangon PO 11052, Myanmar
Yati Phyo: School of Information Science, Japan Advanced Institite of Science and Technology (JAIST), Nomi, Ishikawa 923-1292, Japan
Canh Minh Do: School of Information Science, Japan Advanced Institite of Science and Technology (JAIST), Nomi, Ishikawa 923-1292, Japan
Kazuhiro Ogata: School of Information Science, Japan Advanced Institite of Science and Technology (JAIST), Nomi, Ishikawa 923-1292, Japan

Mathematics, 2021, vol. 9, issue 4, 1-16

Abstract: 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.

Keywords: eventual property; model checking; Maude (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2021
References: View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
https://www.mdpi.com/2227-7390/9/4/368/pdf (application/pdf)
https://www.mdpi.com/2227-7390/9/4/368/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:9:y:2021:i:4:p:368-:d:498448

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().