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, several fuzzy temporal logic systems and reasoning networks have been proposed. However, many of them are not suitable to model dynamic behavior of state-transition reactive systems because they only model static causal relationships among temporal entities as time points or events. Other fuzzy temporal logic systems do capable of modelling reactive systems which includes temporal uncertainty, but they have limited capability in representation of temporal information. Especially, few fuzzy temporal logic system includes branching temporal model.
In this paper, fuzzy temporal entities, namely fuzzy temporal event and fuzzy temporal state are defined. By defining events as a fuzzy number, fuzzy temporal events alleviate the Divided Instant Problem of interval representation while captures temporal uncertainty in appropriate manner. Fuzzy temporal states are represented as the half-open interval between two fuzzy temporal events. Retaining conventional meaning of states as interval between two events, fuzzy temporal states are capable of representing uncertain state boundaries.
Using fuzzy temporal events and states within the logical model, Fuzzy Linear Temporal Logic (FLTL) is defined. FLTL has a linear sequence of fuzzy temporal states as its temporal model. FLTL subsumes Propositional Linear Temporal Logic (PLTL). Hence FLTL can be used in areas where PLTL have been used, with advantages of quantitative modelling and uncertainty representation.
A counterpart to FLTL, with branching temporal model, is defined as Fuzzy Branching Temporal Logic (FBTL). FBTL can model a tree-like branching temporal model with fuzzy temporal measures. FBTL subsumes Concurrent Tree $Logic^* (CTL^*)$, which has been frequently used in modelling concurrent systems.
In this paper, the syntax and interpretation of FLTL and FBTL is represented, and the fact that FLTL subsumes PLTL and that FBTL subsumes $CTL^*$ are proved. A limited deductive system for FBTL is also proposed. As application examples, FLTL is used in analysis of a fuzzy-timed variant of Statecharts, and FBTL is used in modelling fuzzy job shop scheduling problem.
이산 사건 시스템, 실시간 컴퓨터 시스템, 그리고 통신 프로토콜과 같은 복잡한 반응적 시스템은 시간이 흐름에 따라 변하는 특성을 갖는다. 반응적 시스템의 타당한 모델은 그 시스템이 갖는 가능한 상태들과 각 상태들 간의 관계를 포함해야 한다. 또한 그 모델을 분석하는 도구가 제공되어야 한다.
시제 논리는 반응적 시스템 모델링과 분석에 널리 사용되어 왔다. 많은 종류의 시제 논리 시스템들이 제안되고 사용되어 왔으며, 특히 실시간 시스템 소프트웨어의 명세와 검증에 많이 사용되었다. 일부 시제 논리 시스템은 상태들과 그 사이의 관계를 정성적으로 모델링한다. 정성적 모델은 상태들과 그 관계들이 기술되고, 상태의 순서들이 갖는 여러가지 특성들을 논리 명제로 분석한다. 다른 시제 논리 시스템들은 정량적 모델링을 허용한다. 정량적 모델링은 정성적 모델이 표현하는 특성들을 포함하면서, 상태와 사건들에 연관된 시간의 길이를 시간 단위로 기술할 수 있다. 비록 많은 동적 시스템이 정성적 시제 논리로 모델링될수 있지만, 대부분의 실시간 시스템은 성능에 필수적인 특성들을 드러내기 위해 정량적 모델링을 필요로 한다.
한편, 일종의 시간적 모호함이 실시간 시스템의 정량적 모델을 만드는데 있어 나타날 수 있다. 어떤 종류의 시간적 모호함은 초기 설계 단계에서의 추상 명세에서 발생한다. 보수적인 추상화는 시간적 특성을 상한 내지 하한으로 기술해야 하므로, 이러한 모호함이 발생한다. 특히, 이러한 모호함을 모델링하기 위해서는 실수 시간 차원이 필요하다고 논의된 바 있다. 다른 시간적 모호함은 모델 대상 시스템의 시간적 특성에 대한 제한된 지식에서 생겨난다. 예를 들어 외부 입력으로 발생하는 사건들에 대한 시간적 특성에 대한 지식은 반드시 포함되는 잡음 신호들 때문에 가장 획득하기 어려운 종류라는것의 논의된 바 있다.
이러한 문제를 완화하기 위해 몇 가지 퍼지 시제 논리 또는 퍼지 시제 추론 시스템이 이미 제안된 바 있다. 그러나, 그 중 많은 시스템들은 시간 개체 즉 시점이나 사건들 사이의 정적 인과 관계만을 모델링하기 때문에 상태-변화 시스템의 동적 행동을 모델링하는데 어려움이 있다. 다른 퍼지 시제 논리 시스템들은 동적 시스템을 시간적 모호함과 함께 모델링 할 수 있으나, 모호한 시간 정보의 표현에 있어 제약을 갖고 있다. 특히 분기 시간 모델을 갖는 퍼지 시제 논리 프레임워크는 매우 드물다.
이 논문에서는, 퍼지 시제 사건과 퍼지 시제 상태라는 퍼지 시제 개체들을 정의한다. 퍼지 시제 사건들을 퍼지 숫자로 정의함으로서 구간으로 정의되었을때 일어나는 순간 확정 문제 (Divided Instant Problem: DIP)을 피하는 동시에, 시간적 모호함을 적절히 표현할 수 있다. 퍼지 시제 상태들은 두 퍼지 시제 사건 사이의 반개방 구간으로 정의된다. 두 사건 사이의 구간이라는 일반적인 상태의 의미를 유지하면서, 퍼지 시제 상태는 모호한 상태 경계를 표현할 수 있다.
퍼지 시제 사건과 퍼지 시제 상태를 논리 모델 안에서 사용하여, 퍼지 선형 시제 논리 (Fuzzy Linear Temporal Logic: FLTL)가 정의되었다. FLTL은 퍼지 시제 상태들의 선형 순서를 시제 모델로 하고 있다. FLTL은 명제 선형 시제 논리 (Propositional Linear Temporal Logic: PLTL) 을 포함한다. 따라서 FLTL 은 PLTL 이 사용되었던 분야에 적용가능하며, 정량적 모델링과 모호한 표현이 가능하다.
퍼지 선형 시제 논리의 대응으로서 분기 시간 모델을 갖는 퍼지 분기 시제 논리 (Fuzzy Branching Temporal Logic: FBTL) 가 정의되었다. 퍼지 분기 시제 논리는 트리 형태의 분기 시제 모델을 갖고 있으며 퍼지 시간 단위들을 포함한다. FBTL은 병행 시스템을 모델링하는데 자주 사용되어 온 $병행 트리 로직^* (Concurrent Tree Logic: CTL^*)$ 를 포함한다.
이 논문에서, FLTL, FBTL 의 문법과 해석방법을 각각 정의하였고, FLTL 이 PLTL 을, 그리고 FBTL 이 $CTL^*$ 를 포함한다는 것이 증명되었다. FBTL 의 제한된 추론 시스템도 제안되었다. 응용 분야로서, FLTL 이 퍼지 시간을 갖는 Statecharts 의 변종을 분석하는데 사용될 수 있다는 것을 보였으며, FBTL 이 퍼지 개별 공정 계획 문제 (fuzzy job shop scheduling) 를 모델링하는데 사용될 수 있다는 것을 보였다.
