TY - GEN
T1 - Formal verification of a fuzzy rule-based classifier using the prototype verification system
AU - Gebreyohannes, Solomon
AU - Karimoddini, Ali
AU - Homaifar, Abdollah
AU - Esterline, Albert
N1 - Publisher Copyright:
© Springer International Publishing AG, part of Springer Nature 2018.
PY - 2018
Y1 - 2018
N2 - This paper presents the formal specification and verification of a Type-1 (T1) Fuzzy Logic Rule-Based Classifier (FLRBC) using the Prototype Verification System (PVS). A rule-based system models a system as a set of rules, which are either collected from subject matter experts or extracted from data. Unlike many machine learning techniques, rule-based systems provide an insight into the decision making process. In this paper, we focus on a T1 FLRBC. We present the formal definition and verification of the T1 FLRBC procedure using PVS. This helps mathematically verify that the design intent is maintained in its implementation. A highly expressive language such as PVS, which is based on a strongly-typed higher-order logic, allows one to formally describe and mathematically prove that there is no contradiction or false assumption in the procedure. We show this by (1) providing the formal definition of the T1 FLRBC in PVS and then (2) formally proving or deducing rudimentary properties of the T1 FLRBC from the formal specification.
AB - This paper presents the formal specification and verification of a Type-1 (T1) Fuzzy Logic Rule-Based Classifier (FLRBC) using the Prototype Verification System (PVS). A rule-based system models a system as a set of rules, which are either collected from subject matter experts or extracted from data. Unlike many machine learning techniques, rule-based systems provide an insight into the decision making process. In this paper, we focus on a T1 FLRBC. We present the formal definition and verification of the T1 FLRBC procedure using PVS. This helps mathematically verify that the design intent is maintained in its implementation. A highly expressive language such as PVS, which is based on a strongly-typed higher-order logic, allows one to formally describe and mathematically prove that there is no contradiction or false assumption in the procedure. We show this by (1) providing the formal definition of the T1 FLRBC in PVS and then (2) formally proving or deducing rudimentary properties of the T1 FLRBC from the formal specification.
KW - Formal verification
KW - Fuzzy rule-based classifier
KW - Prototype verification system
UR - https://www.scopus.com/pages/publications/85051030674
U2 - 10.1007/978-3-319-95312-0_1
DO - 10.1007/978-3-319-95312-0_1
M3 - Conference contribution
SN - 9783319953113
T3 - Communications in Computer and Information Science
SP - 1
EP - 12
BT - Fuzzy Information Processing - 37th Conference of the North American Fuzzy Information Processing Society, NAFIPS 2018, Proceedings
A2 - Barreto, Guilherme A.
A2 - Coelho, Ricardo
PB - Springer Verlag
T2 - 37th Conference of the North American Fuzzy Information Processing Society, NAFIPS 2018
Y2 - 4 July 2018 through 6 July 2018
ER -