Fuzzy Temporal Logic
The aim of this project, a minor project in fulfillment of the PhD duties at Politecnico di Milano, is to investigate the possibility to apply fuzzy temporal logic to the model checking domain....
The following is the initial project definition:
The main purpose of this research is designing a fuzzy temporal logic language by extending a temporal logic language like Linear Temporal Logic (LTL) or Computational Tree Logic (CTL) to specify users’ requirements and also to generate action plans by doing model checking. The motivation comes from the problem that in developing software systems and especially while eliciting and modeling requirements, people naturally use natural languages, which is usually ambiguous for a machine. For example, user walks around with his PDA in a pervasive environment, looking for a high-speed Internet service to get connected to. Another user searches a highly available GPS service with a reasonable price. However, the challenge is that software underlying cannot understand the meaning of high-speed, highly available, and reasonable. On the other hand, sometimes requirements specification represents the needs of different users, but it is clear that the concept of high-speed and reasonable is different for different people. Thus, it is needed to use complementary specification to quantify and personalize a specification for each user, which can be done by using fuzzy variables and personal membership functions. Note that a real requirements specification can include a lot of statements with various timing constraints between them. Interestingly the timing relations may be expressed ambiguous in natural language, for instance ‘slightly before’, ‘around 3:00’, and so on. How can we represent these concepts in a requirements specification? However software can only reason about numbers. The solution can be a new temporal logic language with fuzzy operators to handle uncertainty and ambiguity. To formalize a requirements specification, it is common to use LTL or other temporal logic languages, which are based on Boolean logic. Specifying requirements by using LTL means that a typical requirement is completely satisfied or not! Conversely, in the real world it is likely to happen that users accept even partial satisfaction, so designing fuzzy LTL can help specify requirements with different satisfaction levels. To do so, it is required to redefine LTL operators (Next, Until, Always,…) On the other hand, requirements are supposed to be satisfied by system. To get each of them done, system needs to generate a plan that can be represented in terms of states and actions. One option to perform the task of planning is model checking of requirements. In fact, a fuzzy LTL formula is fed into a fuzzy model checker, which generates all reachable states from an initial state. An action plan is a set of actions on a path between initial state and a satisfactory state that formula holds in. To wrap it up, the main idea of this research is to design a fuzzy temporal logic and also implement a model checker to verify fuzzy formulas and generate action plans.
Further commnts in the discussion tab
