A Divide and Conquer Approach to Eventual Model Checking

A Divide and Conquer Approach to Eventual Model Checking

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 che...

Full description

Bibliographic Details
Main Authors: Moe Nandi Aung, Yati Phyo, Canh Minh Do, Kazuhiro Ogata
Format: Article
Language:English
Published: MDPI AG 2021-02-01
Series:Mathematics
Subjects:
eventual property
model checking
Maude
Online Access:https://www.mdpi.com/2227-7390/9/4/368
id doaj-b2e79946cc4e4e11af32e12ed4108c80
record_format Article
spelling doaj-b2e79946cc4e4e11af32e12ed4108c802021-02-13T00:04:03ZengMDPI AGMathematics2227-73902021-02-01936836810.3390/math9040368A Divide and Conquer Approach to Eventual Model CheckingMoe Nandi Aung0Yati Phyo1Canh Minh Do2Kazuhiro Ogata3Faculty of Information Science, University of Information Technology (UIT), Hlaing Township, Yangon PO 11052, MyanmarSchool of Information Science, Japan Advanced Institite of Science and Technology (JAIST), Nomi, Ishikawa 923-1292, JapanSchool of Information Science, Japan Advanced Institite of Science and Technology (JAIST), Nomi, Ishikawa 923-1292, JapanSchool of Information Science, Japan Advanced Institite of Science and Technology (JAIST), Nomi, Ishikawa 923-1292, JapanThe 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.https://www.mdpi.com/2227-7390/9/4/368eventual propertymodel checkingMaude
collection DOAJ
language English
format Article
sources DOAJ
author Moe Nandi Aung
Yati Phyo
Canh Minh Do
Kazuhiro Ogata
spellingShingle Moe Nandi Aung
Yati Phyo
Canh Minh Do
Kazuhiro Ogata
A Divide and Conquer Approach to Eventual Model Checking
Mathematics
eventual property
model checking
Maude
author_facet Moe Nandi Aung
Yati Phyo
Canh Minh Do
Kazuhiro Ogata
author_sort Moe Nandi Aung
title A Divide and Conquer Approach to Eventual Model Checking
title_short A Divide and Conquer Approach to Eventual Model Checking
title_full A Divide and Conquer Approach to Eventual Model Checking
title_fullStr A Divide and Conquer Approach to Eventual Model Checking
title_full_unstemmed A Divide and Conquer Approach to Eventual Model Checking
title_sort divide and conquer approach to eventual model checking
publisher MDPI AG
series Mathematics
issn 2227-7390
publishDate 2021-02-01
description 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.
topic eventual property
model checking
Maude
url https://www.mdpi.com/2227-7390/9/4/368
work_keys_str_mv AT moenandiaung adivideandconquerapproachtoeventualmodelchecking
AT yatiphyo adivideandconquerapproachtoeventualmodelchecking
AT canhminhdo adivideandconquerapproachtoeventualmodelchecking
AT kazuhiroogata adivideandconquerapproachtoeventualmodelchecking
AT moenandiaung divideandconquerapproachtoeventualmodelchecking
AT yatiphyo divideandconquerapproachtoeventualmodelchecking
AT canhminhdo divideandconquerapproachtoeventualmodelchecking
AT kazuhiroogata divideandconquerapproachtoeventualmodelchecking
_version_ 1724272504294342656

Similar Items