This paper presents a new temporal logic for fuzzy logic systems, fuzzy computation tree logic (FzCTL), based on previous work on Kripke structures for fuzzy logic systems, that is, fuzzy program graph (FzPG) [1]. The motivation for providing a new temporal logic is to reduce state explosion, which is worse in fuzzy systems than in regular model checking. This is achieved by using ordered binary decision diagram (OBDD) techniques to represent the FzPG Kripke structure and to effectively evaluate FzCTL temporal formulas.

The authors evaluate performance in different ways. I found the table comparing different maximum OBDD heights to be the most interesting. Their implementation is tested with a couple of useful examples, showing how the choice of fuzzy variables may have an important impact on determining model stability and on evaluating different temporal formulas.

My only concern is typographical errors; they may not stop the reader from understanding the content, but do prevent a fluid and enjoyable reading experience.