Fuzzy linear temporal logic and fuzzy branching temporal logic

Abstract

Complex reactive systems, such as discrete-event systems, real-time computer systems and communication protocols change their properties as time passes. Proper model of a reactive system should include the possible states of the system and relationships among the states. Also, a proper tool for analyzing the model should be provided. Temporal logic systems have been widely used for reactive system modelling and analysis, meeting the need for modelling and analysis. Many kinds of temporal logic systems have been proposed and used in areas as software specification and validation, especially for real-time systems and communication protocols. Some temporal logic systems are qualitative, that only states and their relationships are described, and their sequences are analyzed for various properties as logical value of propositions. Other temporal logic systems are quantitative, which include properties handled in qualitative modelling, as well as the length of time associated with states and events, represented in time metric. Although many reactive systems can be modelled with qualitative temporal logic, most real-time systems need quantitative model to reveal their mission-critical properties. On the other hand, some kind of temporal uncertainty may present itself in building a quantitative temporal model of a real-time system. Some kind of temporal uncertainty arises from abstract specification of early design stages, since a conservative abstraction needs to specify a temporal property as an upper bound and/or lower bound. Especially, it has been argued that real-valued time domain is needed to model this kind of abstraction. Other kind of temporal uncertainty arises from limited knowledge about temporal properties of modelled system. For example, it has been argued that one of the most difficult temporal property to obtain is the knowledge about environmental data input, since most sensory inputs include some kind of noise signal. To alleviate this problem, ...