Skip to main content
SpringerLink
Log in

Formal Verification of a Fuzzy Rule-Based Classifier Using the Prototype Verification System

  • Conference paper
  • First Online:
Fuzzy Information Processing (NAFIPS 2018)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 831))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Grosan, C., Abraham, A.: Rule-based expert systems. In: Grosan, C., Abraham, A. (eds.) Intelligent Systems. ISRL, vol. 17, pp. 149–185. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21004-4_7

    Chapter  MATH  Google Scholar 

  2. Mendel, J.M.: Uncertain Rule-Based Fuzzy Logic Systems: Introduction and New Directions. Prentice Hall PTR, Upper Saddle River (2001)

    MATH  Google Scholar 

  3. Mendel, J.M.: Uncertain Rule-Based Fuzzy Logic Systems: Introduction and New Directions. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-51370-6

    Book  MATH  Google Scholar 

  4. Jaworska, T.: Application of fuzzy rule-based classifier to CBIR in comparison with other classifiers. In: 2014 11th International Conference on Fuzzy Systems and Knowledge Discovery (FSKD), pp. 119–124. IEEE (2014)

    Google Scholar 

  5. Beke, A., Yuceler, A.A., Kumbasar, T.: A rule based fuzzy gesture recognition system to interact with Sphero 2.0 using a smart phone. In: 2017 International Artificial Intelligence and Data Processing Symposium (IDAP), pp. 1–4. IEEE (2017)

    Google Scholar 

  6. Wu, H., Mendel, J.M.: Classification of battlefield ground vehicles using acoustic features and fuzzy logic rule-based classifiers. IEEE Trans. Fuzzy Syst. 15(1), 56–72 (2007)

    Article  Google Scholar 

  7. Jefferson, C., Liu, H., Cocea, M.: Fuzzy approach for sentiment analysis. In: 2017 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE), pp. 1–6. IEEE (2017)

    Google Scholar 

  8. Stavrakoudis, D.G., Theocharis, J.B.: A genetic fuzzy rule-based classifier for land cover image classification. In: 2009 IEEE International Conference on Fuzzy Systems, FUZZ-IEEE 2009, pp. 1677–1682. IEEE (2009)

    Google Scholar 

  9. Angelov, P.P., Gu, X.: A cascade of deep learning fuzzy rule-based image classifier and SVM. IEEE (2017)

    Google Scholar 

  10. Nawaz, M.S., IkramUllah Lali, M., Pasha, M.A.: Formal verification of crossover operator in genetic algorithms using prototype verification system (PVS). In: 2013 IEEE 9th International Conference on Emerging Technologies (ICET), pp. 1–6. IEEE (2013)

    Google Scholar 

  11. Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217

    Chapter  Google Scholar 

  12. The B method. http://www.methode-b.com/en/

  13. Gordon, M.J.C., Melham, T.F.: Introduction to HOL a theorem proving environment for higher order logic (1993)

    Google Scholar 

  14. Coq Development Team: The Coq proof assistant (2012). https://coq.inria.fr/distrib/current/refman/

  15. Butler, R.: An elementary tutorial on formal specification and verification using PVS. NASA Technical Memorandum 108991, September 1993

    Google Scholar 

  16. Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. In: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April, Updated June 1995

    Google Scholar 

  17. Butler, R.: An introduction to requirements capture using PVS: specification of a simple autopilot. IEEE Trans. Softw. Eng. 24 (1996). NASA Technical Memorandum 110255

    Google Scholar 

  18. Crow, J., Di Vito, B.L.: Formalizing space shuttle software requirements. To be Presented at the ACM SIGSOFT Workshop on Formal Methods in Software Practice, San Diego, CA, January 1996

    Google Scholar 

  19. Enyinna, N., Karimoddini, A., Opoku, D., Homaifar, A., Arnold, S.: Developing an interval type-2 TSK fuzzy logic controller. In: 2015 Annual Conference of the North American Fuzzy Information Processing Society (NAFIPS) Held Jointly with 2015 5th World Conference on Soft Computing (WConSC), pp. 1–6, August 2015

    Google Scholar 

  20. Mamdani, E.H., Assilian, S.: An experiment in linguistic synthesis with a fuzzy logic controller. Int. J. Man Mach. Stud. 7(1), 1–13 (1975)

    Article  Google Scholar 

  21. Owre, S., Shankar, N.: PVS prelude library. CSL Technical Report SRI-CSL-03-01, SRI International, Computer Science Laboratory, March 2003

    Google Scholar 

  22. Owre, S., Shankar, N., Rushby, J., Stringer-Calvert, D.: PVS language reference. SRI International, Computer Science Laboratory, version 2.4 (2001)

    Google Scholar 

  23. Owre, S., Shankar, N., Rushby, J., Stringer-Calvert, D.: PVS prover guide. SRI International, Computer Science Laboratory, version 2.4 (2001)

    Google Scholar 

Download references

Acknowledgment

This research is supported by Air Force Research Laboratory and Office of the Secretary of Defense under agreement number FA8750-15-2-0116 as well as US ARMY Research Office under agreement number W911NF-16-1-0489.

Author information

Authors and Affiliations

  1. Department of Electrical and Computer Engineering, North Carolina A&T State University, 1601 East Market Street, Greensboro, NC, 27411, USA

    Solomon Gebreyohannes, Ali Karimoddini, Abdollah Homaifar & Albert Esterline

Authors
  1. Solomon Gebreyohannes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ali Karimoddini
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Abdollah Homaifar
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Albert Esterline
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ali Karimoddini .

Editor information

Editors and Affiliations

  1. Department of Teleinformatics Engineering, Federal University of Ceará, Fortaleza, Ceará, Brazil

    Guilherme A. Barreto

  2. Department of Statistics & Applied Mathematics, Federal University of Ceará, Fortaleza, Ceará, Brazil

    Ricardo Coelho

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Gebreyohannes, S., Karimoddini, A., Homaifar, A., Esterline, A. (2018). Formal Verification of a Fuzzy Rule-Based Classifier Using the Prototype Verification System. In: Barreto, G., Coelho, R. (eds) Fuzzy Information Processing. NAFIPS 2018. Communications in Computer and Information Science, vol 831. Springer, Cham. https://doi.org/10.1007/978-3-319-95312-0_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95312-0_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95311-3

  • Online ISBN: 978-3-319-95312-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation