A Divide & Conquer Approach to Leads-to Model Checking. (1st February 2021)

• Record Type: Journal Article
• Authors: Phyo, Yati; Minh Do, Canh; Ogata, Kazuhiro
• Is Part Of: Computer journal. Volume 65:Number 6(2022)
• Page Start: 1353
• Page End: 1364
• Publication Date: 2021-02-01
• Subjects: leads-to properties -- liveness properties -- model checking -- Maude -- state explosion; Computers -- Periodicals; 005.1
• DOI: 10.1093/comjnl/bxaa183
• Languages: English
• ISSNs: 0010-4620

Abstract

Abstract: The paper proposes a new technique to mitigate the state explosion in model checking. The technique is called a divide & conquer approach to leads-to model checking. As indicated by the name, the technique is dedicated to leads-to properties. It is known that many important systems requirements can be expressed as leads-to properties, thus it is worth focusing on leads-to properties. The technique divides an original leads-to 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 leads-to model checking problem. We conduct two case studies demonstrating the power of the proposed technique.