A divide and conquer approach to until and until stable model checking
Canh Minh, Yati Phyo, Kazuhiro Ogata · Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge Engineering · 2022
The paper describes a technique to mitigate the notorious state space explosion in model checking.The technique is called a divide & conquer approach to until and until stable model checking.As indicated by the name, the technique is dedicated to until and until stable properties that are expressed as φ1 U φ2 and φ1 U □φ2, respectively, where φ1, φ2 are state propositions.For real-time system analysis, some interesting systems requirements are expressed as until and until stable properties.For example, a clock is running and shows a correct time until a certain time has passed or until the clock stops due to an empty battery or other failures.Therefore, it is worth focusing on the properties.For each property, we prove a theorem that the proposed technique is correct and design an algorithm based on the theorem to support the technique.Index Terms-until properties,