Abstract

Recently, by defining suitable fuzzy temporal logics, temporal properties of dynamic systems are specified during model checking process, yet a few numbers of fuzzy temporal logics along with capable corresponding models are developed and used in system design phase, moreover in case of having a suitable model, it suffers from the lack of a capable model checking approach. Having to deal with uncertainty in model checking paradigm, this paper introduces a fuzzy Kripke model (FzKripke) and then provides a verification approach using a novel logic called Fuzzy Computation Tree Logic* (FzCTL*). Not only state space explosion is handled using well-known concepts like abstraction and bisimulation, but an approximation method is also devised as a novel technique to deal with this problem. Fuzzy program graph, a generalization of program graph and FzKripke, is also introduced in this paper in consideration of higher level abstraction in model construction. Eventually modeling, and verification of a multi-valued flip-flop is studied in order to demonstrate capabilities of the proposed models.

Introduction

Model checking is an automatic formal technique for investigating correctness properties of systems, more specifically model checking also known as property checking refers to the following problem: “Given a finite-state model and a formal property, model checking automatically checks whether this property holds for that model” [BK]. Temporal properties of reactive systems can only be checked by temporal model checking. In these models, time is considered as either concrete (real-time) or discrete. In order to check the majority of real-time models such as timed automata (TA) [AD94], it is necessary to convert these models into discrete time models and then perform model checking process employing simpler logics such as computation tree logic (CTL). It is because logics defined alongside concrete time models such as timed computation tree logic (TCTL) are incapable of participating in model checking process.