A Divide and Conquer Approach to Eventual Model Checking

Autor: Moe Nandi Aung, Yati Phyo, Canh Minh Do, Kazuhiro Ogata
Jazyk: angličtina
Rok vydání: 2021
Předmět:
Zdroj: Mathematics, Vol 9, Iss 4, p 368 (2021)
Druh dokumentu: article
ISSN: 2227-7390
DOI: 10.3390/math9040368
Popis: 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.
Databáze: Directory of Open Access Journals