CTL Symbolic Model Checking Based on Fuzzy Logic
Pengzhan Nie, Jiulei Jiang, Zhanyou Ma · 2020
The problem of state space explosion is often encountered in model checking, and the fuzzy uncertainty information in the system also needs to be processed. We have proposed a new calculation method of model checking. Unlike the classical symbolic model checking, CTL based on fuzzy logic is symbolized, and quasi-Boolean functions that can be represented by multiple terminal binary decision diagrams (MTBDD) are used to represent system models and attribute specifications. Combining the operation rules between quasi-Boolean functions with classic symbol model checking formulas and verifying them, a quasi-Boolean function formula is finally obtained. By putting the state code into the formula, the corresponding probability value can be obtained.