Symbolic checking of Fuzzy CTL on Fuzzy Program Graph

Masoud Ebrahimi, Gholamreza Sotudeh, Ali Movaghar

Research output: Contribution to journalArticleResearchpeer-review

Abstract

Few fuzzy temporal logics and modeling formalisms are developed such that their model checking is both effective and efficient. State-space explosion makes model checking of fuzzy temporal logics inefficient. That is because either the modeling formalism itself is not compact, or the verification approach requires an exponentially larger yet intermediate representation of the modeling formalism. To exemplify, Fuzzy Program Graph (FzPG) is a very compact, and powerful formalism to model fuzzy systems; yet, it is required to be translated into an equal Fuzzy Kripke model with an exponential blow-up should it be formally verified. In this paper, we introduce Fuzzy Computation Tree Logic (FzCTL) and its direct symbolic model checking over FzPG that avoids the aforementioned state-space explosion. Considering compactness and readability of FzPG along with expressiveness of FzCTL, we believe the proposed method is applicable in real-world scenarios. Finally, we study formal verification of fuzzy flip-flops to demonstrate capabilities of the proposed method.
Original languageEnglish
JournalActa informatica
DOIs
Publication statusE-pub ahead of print - 3 Feb 2018

Fingerprint

Model checking
Temporal logic
Explosions
Flip flop circuits
Fuzzy systems

Cite this

Symbolic checking of Fuzzy CTL on Fuzzy Program Graph. / Ebrahimi, Masoud; Sotudeh, Gholamreza; Movaghar, Ali.

In: Acta informatica, 03.02.2018.

Research output: Contribution to journalArticleResearchpeer-review

@article{a09a729411e24b20935f3153ed665e89,
title = "Symbolic checking of Fuzzy CTL on Fuzzy Program Graph",
abstract = "Few fuzzy temporal logics and modeling formalisms are developed such that their model checking is both effective and efficient. State-space explosion makes model checking of fuzzy temporal logics inefficient. That is because either the modeling formalism itself is not compact, or the verification approach requires an exponentially larger yet intermediate representation of the modeling formalism. To exemplify, Fuzzy Program Graph (FzPG) is a very compact, and powerful formalism to model fuzzy systems; yet, it is required to be translated into an equal Fuzzy Kripke model with an exponential blow-up should it be formally verified. In this paper, we introduce Fuzzy Computation Tree Logic (FzCTL) and its direct symbolic model checking over FzPG that avoids the aforementioned state-space explosion. Considering compactness and readability of FzPG along with expressiveness of FzCTL, we believe the proposed method is applicable in real-world scenarios. Finally, we study formal verification of fuzzy flip-flops to demonstrate capabilities of the proposed method.",
author = "Masoud Ebrahimi and Gholamreza Sotudeh and Ali Movaghar",
year = "2018",
month = "2",
day = "3",
doi = "10.1007/s00236-018-0311-3",
language = "English",
journal = "Acta informatica",
issn = "1432-0525",
publisher = "Springer New York",

}

TY - JOUR

T1 - Symbolic checking of Fuzzy CTL on Fuzzy Program Graph

AU - Ebrahimi, Masoud

AU - Sotudeh, Gholamreza

AU - Movaghar, Ali

PY - 2018/2/3

Y1 - 2018/2/3

N2 - Few fuzzy temporal logics and modeling formalisms are developed such that their model checking is both effective and efficient. State-space explosion makes model checking of fuzzy temporal logics inefficient. That is because either the modeling formalism itself is not compact, or the verification approach requires an exponentially larger yet intermediate representation of the modeling formalism. To exemplify, Fuzzy Program Graph (FzPG) is a very compact, and powerful formalism to model fuzzy systems; yet, it is required to be translated into an equal Fuzzy Kripke model with an exponential blow-up should it be formally verified. In this paper, we introduce Fuzzy Computation Tree Logic (FzCTL) and its direct symbolic model checking over FzPG that avoids the aforementioned state-space explosion. Considering compactness and readability of FzPG along with expressiveness of FzCTL, we believe the proposed method is applicable in real-world scenarios. Finally, we study formal verification of fuzzy flip-flops to demonstrate capabilities of the proposed method.

AB - Few fuzzy temporal logics and modeling formalisms are developed such that their model checking is both effective and efficient. State-space explosion makes model checking of fuzzy temporal logics inefficient. That is because either the modeling formalism itself is not compact, or the verification approach requires an exponentially larger yet intermediate representation of the modeling formalism. To exemplify, Fuzzy Program Graph (FzPG) is a very compact, and powerful formalism to model fuzzy systems; yet, it is required to be translated into an equal Fuzzy Kripke model with an exponential blow-up should it be formally verified. In this paper, we introduce Fuzzy Computation Tree Logic (FzCTL) and its direct symbolic model checking over FzPG that avoids the aforementioned state-space explosion. Considering compactness and readability of FzPG along with expressiveness of FzCTL, we believe the proposed method is applicable in real-world scenarios. Finally, we study formal verification of fuzzy flip-flops to demonstrate capabilities of the proposed method.

U2 - 10.1007/s00236-018-0311-3

DO - 10.1007/s00236-018-0311-3

M3 - Article

JO - Acta informatica

JF - Acta informatica

SN - 1432-0525

ER -