# Symbolic checking of Fuzzy CTL on Fuzzy Program Graph

- 820 Downloads

## Abstract

Few fuzzy temporal logics and modeling formalisms are developed such that their model checking is both effective and efficient. State-space explosion makes model checking of fuzzy temporal logics inefficient. That is because either the modeling formalism itself is not compact, or the verification approach requires an exponentially larger yet intermediate representation of the modeling formalism. To exemplify, Fuzzy Program Graph (FzPG) is a very compact, and powerful formalism to model fuzzy systems; yet, it is required to be translated into an equal Fuzzy Kripke model with an exponential blow-up should it be formally verified. In this paper, we introduce Fuzzy Computation Tree Logic (FzCTL) and its direct symbolic model checking over FzPG that avoids the aforementioned state-space explosion. Considering compactness and readability of FzPG along with expressiveness of FzCTL, we believe the proposed method is applicable in real-world scenarios. Finally, we study formal verification of fuzzy flip-flops to demonstrate capabilities of the proposed method.

## 1 Introduction

The real world phenomena will result in human assertions that are imprecise and uncertain; for instance, measuring quantities in the real world can lead to imprecise, fuzzy, or even vague assertions. One cannot simply cope with these types of fuzziness, vagueness, and uncertainties using classical logics; therefore, new types of theories and logics are invented to tackle the issues arising from uncertainties and imprecisions. Among these newly invented theories and logics, probabilistic theory and fuzzy logic together can cope with most of those issues. However, in order to understand what types of uncertainties can be dealt with probability theory and what aspects of uncertainties are best handled with fuzzy logic, it is best for one to know about the background of probability theory and fuzzy logic and their application domains.

Probability theory is defined to deal with uncertainties arising from random events while fuzzy logic is the theory to deal with the data demonstrating uncertainties other than randomness, like fuzziness and sometimes vagueness in expression. The late professor Lotfi Zadeh discussed some fundamental shortcomings in classical probability theory and took several issues with the inclusion of fuzzy logics by this theory. Finally, he specifically stated that the two concepts are complementary; yet, a perception-based probability theory is more general and more complex than probability theory, conceptually, mathematically, and computationally [29]. Consequently, throughout this paper we neither intend to elaborate on fuzzy models nor plan to advocate fuzzy logic; instead, we assume the importance of having fuzzy systems in parallel with probabilistic systems is already justified.

Model based design and formal verification are getting an ever-increasing attention in system development. It is common for a system design, should it be formally verified, to be represented by an appropriate mathematical model, while its behavior is expressed by a descriptive specification framework; thereupon, one is able to devise an algorithm to systematically analyze if the model and subsequently the system’s behavior guarantees certain properties. Since various stochastic phenomena are involved in reliability of a system, verifying if a system design absolutely guarantees certain properties is a rigid notion. Subsequently, focusing on absolute guaranties while verifying system’s behavior is not empirical.

System’s behavior can be considered uncertain if its reliability is susceptible to external stimuli that cannot be controlled or prevented. In order to have an empirical verification approach for systems with uncertain behavior, the mathematical model of the system must be adapted to grasp certain degrees of uncertainty. Meanwhile, the specification framework shall also possess correct understanding of uncertainty at the same level. Consequently, verification approaches are invented to verify certain aspects of systems that show stochastic, random, and uncertain behaviors.

Systems that are subject to or dealing with random phenomena are comprising both nondeterministic and probabilistic state transitions simultaneously. Markovian models typically represent these systems. A discrete-time finite state transition system whose transition to next state is distributed probabilistically is a discrete-time Markov Chain. A more sophisticated Markovian model in which nondeterministic and probabilistic transitions coexist is called a Markov Decision Process. In in any state of Markov decision process there exist a nondeterministic choice between probability distributions for the successors.

Probabilistic Computation Tree Logic (PCTL) is an extension of CTL such that it formulates conditions on a state of a Markov chain and Markov decision process [2, 4, 10]. In PCTL, a quantitative counterpart replaced path quantifiers \(\exists \) and \(\forall \) that is denoted as \(\mathbb {P}_J(\varphi )\), where *J* indicates a probabilistic bound on the number of paths satisfying property \(\varphi \) and yet the interpretation of a PCTL formula remains Boolean; that is, a state either satisfies or violates a PCTL formula. PCTL model checking for Markov chains is a natural extension of CTL model checking. A state *s* is considered in satisfaction set for a state formula only if the probability of *s* satisfying certain path property is in the probabilistic bound *J*. Unfortunately Markov chains and Markov decision processes are not powerful enough to model sophisticated dynamics of systems.

A more sophisticated, and comprehensive class of systems are hybrid systems that consist both discrete and continuous components. In order to model hybrid systems, Henzinger introduced Hybrid Automata [11]. Hybrid automata grasp the nature of systems that combine discrete and continuous dynamics by combining continuously evolving variables and finite state control graphs. The discrete components in hybrid automata are usually digital components that regulate and interact with analog components. Analog sampling and timing are important in hybrid systems and subsequently in hybrid automata for state transitions can occur discretely and instantaneously in the control graph or continuously as time passes by.

Although hybrid automata is very powerful in modeling hybrid systems, its verification problem is generally undecidable even for simple safety properties [12]. Therefore, studies on hybrid systems focus on classes of hybrid automata where the safety verification problem is decidable. Timed Automata are a subclass of hybrid automata whose reachability is decidable. Timed automata consist continuous variables called clocks that continuously evolve with constant slope 1. Clocks are frequently compared to constants and sometimes reset to 0. An extension of timed automata incorporates probabilistic theory to model systems that deal with random phenomena [18].

Probabilistic timed automata is also augmented with additional continuous variables in the form of costs or rewards; the resulting automata is often referred to as priced probabilistic timed automata. In this class of automata, all state and transitions are labeled with state and action rewards, respectively. PCTL is augmented with operators to reason about rewards by comprising a reward operator whose interpretation is Boolean; that is, whenever the expected value of a reward function on a reward/cost variable belongs to certain continuous bound it evaluates to 1 and otherwise to 0. A verification approach is also devised for this class of timed automata and proved to be useful in practice [18]; yet, it is only suitable in formal verification of probabilistic systems.

While modeling, specifying, and verifying probabilistic systems is well studied, verification problem for another subclass of hybrid/dynamic systems that incorporates fuzzy logic is overlooked. Hybrid automata can also model fuzzy logic controllers, as they are a class of hybrid systems. Fuzzy logic control systems can be cast in terms that human operators can understand and better relate to; thus, user’s experience can be used in design phase of the controller [23]. Consequently, fuzzy logic control systems are very popular because they mechanized most of tasks that humans can successfully perform. Meanwhile, numerous fuzzy logic models are developed to represent the underlying logic in fuzzy control systems; yet, few efforts are made to bridge the gap between system modeling and behavior specification, and from thereon to verification.

Seemingly, a scenario quite similar to the narrative of probabilistic system verification is also applicable in formal verification of fuzzy logic systems. It begins with formal verification of discrete-time fuzzy logic models of corresponding systems; then, higher-level abstractions and augmented models shall be built on top of discrete-time fuzzy logic models to address more sophisticated classes of systems. Finally yet importantly, formal verification of fuzzy logic systems shall encompass continuous time through models like fuzzy logic extended timed automata. Meanwhile, the specification framework shall also go through the same development cycle so that it corresponds to the modeling approach.

To this date, there are few efforts to define a suitable fuzzy temporal logic; among which, some used formal statement as the specification framework [9, 17] while others used linguistic statements [3, 27]. Some variety of fuzzy extended temporal logics considered the concept of time to be discrete [5, 21] while others presents events in continuous time [3, 17, 27]. In most cases, fuzzy extended temporal logics accompany a trace checking method instead of a formal verification approach. Fuzzy Branching Temporal Logic (FBTL) by Moon et al. [17] is by far the most notable effort towards a specification framework for fuzzy logic systems. Unfortunately, no one could devised an applicable model checking method for FBTL yet. If such an approach should happen to contrive then it will be based on a simpler fuzzy extended temporal logic defined in discrete time [26]. Therefore, in this paper, we are providing more comprehensive semantics in formal verification of discrete-time fuzzy systems.

Fuzzy Markov Chain is one of the notable discrete-time fuzzy logic models that has a finite convergence to a stationary solution [1]. It is also more robust with respect to small perturbations of the transition matrix compared to probabilistic Markov chains. Although fuzzy Markov chain is a good candidate to model discrete-time fuzzy logic systems, we simply believe this is a matter of preference. This paper neither aims nor intends to compare discrete-time fuzzy logic models but since semantics of our specification language is defined based on this structure [26] and we simply do not intend to reinvent the wheel, FzKripke structure is our choice of model for discrete-time fuzzy systems. FzKripke structure is capable of modeling fuzzy logic controllers, and fuzzy logic circuitry. It was even used for modeling fuzzy flip-flops, and a medical diagnosis and treatment example [22, 26].

Sotudeh also defined a higher-level abstraction of FzKripke structure that is more compact, and easier to manually manipulate called Fuzzy Program Graph (FzPG) [26]. Although FzPG is more efficient in modeling phase, its verification requires a direct translation to an equal FzKripke structure resulting in an exponential blow-up. Due to quantization of truth degrees, state-space explosion in a fuzzy extended model checking is more plausible compared to the classical model checking. Main contribution of this paper is a symbolic checking method for Fuzzy CTL (FzCTL) formulae over FzPG that avoids translation to an equal FzKripke structure. This saves an exponential blow-up, which is most effective in efficient model checking of complex fuzzy logic systems.

The rest of this paper is as follows: in Sects. 2 and 3, we study quantized FzKripke structure and FzCTL, respectively. Quantized FzPG and symbolic checking of FzCTL over FzPG are studied in Sects. 4 and 5, respectively. We analyze computational and memory complexity of proposed symbolic method; yet, an alternative symbolic checking method for FzCTL over FzPG is studied in Appendix A that is of lower memory complexity. Section 6 provides a case study on applicability of the proposed method in design and verification of fuzzy flip-flops. Finally, in Sect. 7 we conclude and plan our future research.

## 2 Quantized Fuzzy Kripke model

Fuzzy Kripke Model (FzKripke) Structure [26] is basically \(\upchi \)Kripke Model [6] whose quasi-boolean algebra is defined on infinite lattice of interval [0, 1]. Similarly the Quantized FzKripke (Q-FzKripke) can be defined over quantized [0, 1]. This model is quite similar to Fuzzy Graph previously introduced in [28]. There are multiple definitions of Fuzzy extended Kripke structure in the literature [22, 26], all of which are equal to some extent, but few of which are accompanied with a well-defined fuzzy extended temporal logic so that they can be used in modeling fuzzy control project and fuzzy logic circuitry.

### Definition 1

### Definition 2

*Quantized Fuzzy Kripke*) This is a tuple \(M = (S,X,\hbox {R},\hbox {L},\hbox {I})\) where \(S = \lbrace s_1,\ldots ,s_n \rbrace \) is a set of states, \(X = \langle x_1 ,\ldots ,x_m \rangle \) is a set of attributes, each of which are assigned with a truth degree in \([0,1]_\varDelta \). Function \({\text {Val}}_\varDelta (X)\) expresses different possible values for all attributes as a whole as follows:

### Definition 3

### Definition 4

Single-Source Quantized Fuzzy Kripke is a Q-FzKripke such that \(\hbox {I}(s_0)=1\) and \(\forall s \in S\setminus \{s_0\} \cdot \hbox {I}(s)=0\).

An arbitrary Q-FzKripke can be casted to a single-source one using the method presented for FzKripke in [26]. In order to model check proposition \(\varphi \) on a multi-source Q-FzKripke *M*, it is enough to check the proposition \({\text {AX}}(\varphi )\) on the equivalent single-source Q-FzKripke \(M'\).

The reason behind casting a multi-source FzKripke structure to a single-source one is that bisimulation equivalence among FzKripke structures is defined on single-source FzKripke structures [26]. As a reminder it is proved that any CTL\(^*\) formula evaluates to the same value on bisimilar Kripke structures [2]. Sotudeh and Movaghar also showed that given two bisimilar FzKripke structures an FzCTL\(^*\) formula is evaluated to a similar truth degree on both of them [26]. Later, we are going to use this property of bisimilar FzKripke structures in devising our symbolic model checking approach.

## 3 Fuzzy Computational Tree Logic

Throughout this section, we assume the reader has knowledgeable about temporal logics, specifically the Computational Tree Logic (CTL). For a thorough introduction on CTL, we suggest to see relevant chapters in [2].

A reactive system is described adequately only if its ongoing behavior in any time step is addressed. An infinite sequence of actions leaving from current, and leading to next states represents a behavior of the system. Temporal logic is a well-established concept capable of describing behaviors of reactive systems [24]. Given analogue inputs as continuous variables whose range is [0, 1], a fuzzy control system is a reactive system that controls complex and continuously varying systems. Consequently, if one aims to describe and study behaviors of fuzzy control systems a fuzzy extended temporal logic can ease the process.

Since in a fuzzy system we are uncertain about the direction of execution path in each time step, Linear Temporal Logic (LTL) is an immediate inadequacy for describing them. In order to describe the behavior of such systems, Sotudeh and Movaghar introduced FzCTL\(^*\) in [26] such that it preserves branching time and uncertainty simultaneously. In this section, we define *Fuzzy Computation Tree Logic (FzCTL)* by restricting FzCTL\(^*\).

A temporal logic is only as powerful as the logic it is built on top of which. The more powerful the underlying logic is the more powerful the temporal logic will be in expressing model’s behavior. A recent study by Haiyu Pan et al. [22] defined a more restricted Fuzzy Computation Tree Logic that only encompasses fuzzy-{negation, conjunction, disjunction, and implication} operators. Meanwhile, almost all fuzzy logic operators in FzCTL\(^*\) are also included in FzCTL making it more descriptive and easier to use. Following subsection refreshes and redefines some fuzzy logic operators previously seen in [26].

### 3.1 Fuzzy logic operators

*discrete-saturation*Open image in new window operator, please see (2).

### 3.2 Syntax

*bounded-add*Open image in new window ,

*discrete-saturation*Open image in new window , and

*scalar-multiplication*Open image in new window are not seen in \(\upchi \)CTL, they are determined by this logic. The full set of temporal operators can be defined using “Next” \(\hbox {X}\) and “Until” \(\hbox {U}\) as follows:We borrowed the definitions for

*quasi-comparison*\(\{ \prec \succ \preceq \succeq \approx \not \approx \}\) operators from [26]. Definitions for other comparison operators are also possible through the definition of \(\ge \) in conjunction with logical operators. Moreover, other auxiliary operators defined in [26] such as

*bounded-subtract*Open image in new window and “if” are defined by FzCTL.

### 3.3 Semantic

*M*represents an FzKripke model while

*s*represents a certain state in

*M*, and \(\pi \) is an infinite path defined on

*M*.Semantic of state formulae is defined as follows:where “\({\text {op}}\)” can be a binary logical operator, a comparison operator, a quasi-comparison operator, or the bounded-add/subtract; the result of comparison operators is either “0” or “1”.Semantic of path formulae can be defined as follows:Given model

*M*, satisfiability of proposition \(\varphi \) is defined asRegarding the semantic of FzCTL formulae, the following equations are in place:where \(\mu Z.f(x)\) and \(\nu Z.f(x)\) are greatest and smallest fixed points of

*f*, respectively.

### Example 1

Given an approximation error \(\varepsilon \) such that 1 is divisible by that, and an approximation function \(\tau _\varepsilon (x)\), it is shown that applying \(\tau _\varepsilon (x)\) on FzKripke *M* does not propagate the error while model checking an approximable FzCTL\(^*\) proposition on it [26]. Similarly, the quantization we defined on interval [0, 1] can be regarded as an immediate approximation of FzCTL and FzKripke with approximation error \(\frac{1}{\varDelta }\); which obviously does not propagate the error because FzCTL is a restricted version of FzCTL\(^*\) that preserves its approximability, and also due to our choice of fuzzy logic operators.

## 4 Quantized Fuzzy Program Graph

Fuzzy Program Graph (FzPG) provides higher-level abstraction of fuzzy systems and it that can be translated to an equivalent FzKripke model [26]. FzPG eases manual modelling process by providing a more scrutable semantics. We define Quantized Fuzzy Program Graph (Q-FzPG) quite similar to FzPG. In this section, we investigate Q-FzPG and its properties.

### Definition 5

*Quantized Fuzzy Program Graph*) This is a tuple \(G = (S, s_0, X, {\text {Init}}, {\text {Act}})\) where

*S*is a set of states, \(s_0\in S\) is the initial state, and “\({\text {Init}}\)” is a function that defines degree of entrance to initial state. “\({\text {Act}}\)” is a relation defining state transitions; each state transition has two parts: (1) a function that defines transition degree, and (2) a function that maps truth degrees from attribute-set of the source state to that of destination. The formal definitions for “\({\text {Init}}\)” and “\({\text {Act}}\)” are:

- 1.
The transition possibility of the new edge is zero.

- 2.
This edge assigns the possibility of the destination attributes by a list of zero values.

### Example 2

*f*,

*g*) is an edge of Q-FzPG where:

### 4.1 Semantic

*G*such that:

- 1.
\(S^\prime = S \times {\text {Val}}_\varDelta (X)\)

- 2.\(\forall \eta \in {\text {Val}}_\varDelta (X)\)
- (a)
if \(s \ne s_0\), then \(\forall s \in S \cdot \hbox {I}(s, \eta ) = 0\)

- (b)
if \(s = s_0\), then \(\forall s \in S \cdot \hbox {I}(s, \eta ) = {\text {Init}}(\eta )\)

- (a)
- 3.
\(\forall \eta \in {\text {Val}}_\varDelta (X), \forall s \in S \cdot \hbox {L}(s, \eta ) = \eta \)

- 4.\(\forall \eta , \eta ^\prime \in {\text {Val}}_\varDelta (X), \forall s, s^\prime \in S\)
- (a)
if \({\text {Act}}(s,s^\prime )\) is not defined, then \(\hbox {R}((s,\eta ),(s^\prime ,\eta ^\prime ))= 0\)

- (b)
if \(({\text {A}},{\text {B}})={\text {Act}}(s,s^\prime )\), and \(\eta ^\prime ={\text {B}}(\eta )\) then \(\hbox {R}((s,\eta ),(s^\prime ,\eta ^\prime ))={\text {A}}(\eta )\)

- (a)

When the equivalent Q-FzKripke accepts a proposition with a certain truth degree, we say that initial Q-FzPG also accepts the proposition with the same degree. Although there is an equivalent Q-FzPG denoted by \(G_K\) with the same number of states \(|S|\) to an arbitrary Q-FzKripke like *K*, it is against the purpose of Fuzzy Program Graph, which is to model the system in a highly compressed format, because for each state of \(G_K\) there is an equivalent state in *K*. To exemplify, an FzPG and an equivalent FzKripke are depicted in Fig. 2.

From this point onwards, for all Q-FzPGs we assume the “\({\text {Init}}\)” function returns “1” for initial state and “0” for all other states unless otherwise stated. In fact, we define a novel “\({\text {Init}}_\imath \)” function that returns “1” for a dummy source like \(\imath \); thereupon, by merging “\({\text {Init}}\)” and “\({\text {Act}}\)”, we obtain a Single-Source Q-FzPG that is referred to instead of the original Q-FzPG.

## 5 Symbolic checking of FzCTL on FzPG

Heretofore several symbolic methods are proposed to investigate satisfiability of propositions of multi-valued temporal logics, some of which use *ordered binary decision diagram* (OBDD), others use vectors of similar diagrams to store multi-valued Kripke models and investigate the satisfiability of propositions on that model [6, 7].

In order to check the temporal properties of a particular FzPG, initially, we translate it to an equivalent FzKripke; then, we check temporal properties on that FzKripke. This yields to an exponential blow-up in the state-space; thus, it is more appropriate to check the specification directly over the FzPG. To this purpose, we devised a symbolic checking method using OBDDs and vectors of OBDD.

Let \(\varDelta = 2^{-d}\), then since all numbers involved in model construction and model checking are multiples of \(\varDelta \), a data type with \(d+1\) bits is sufficient to store truth degrees, where the first bit of data type is the least significant bit and the \(d^{th}\) bit is the most significant one. In order to store a truth degree like \(\varepsilon \) in \(d+1\) bits, it is enough to store \(\varepsilon \times 2^d\) instead. For further readability, from this point forward we assume \(d^\prime = d+1\).

### Example 3

*W*is a vector of bit vectors representing the set of all attributes

*X*as follows:

*U*be union of variables used to encode model states

*S*; this union has a total number of \(\lceil \log _2{|S |} \rceil \) members. From this point forward, we repeatedly use copies of

*U*and

*W*denoted by \(U^\prime \) and \(W^\prime \) respectively.

### 5.1 Auxiliary OBDD operators

This subsection is devoted to describe the functionality of important vector operations, besides basic operations defined on OBDDs that are necessary to define the proposed method.

### Definition 6

*W*and

*U*, the OBDD of vector \({v}_{}\) is of maximum size \(2^h\) and maximum height

*h*as follows:

where \(n = |U |\), \(k = |X |\) and \(d^\prime \) is the length of *W*.

### Theorem 1

([16]) Logical combination of two OBDDs of size *m* and *n* is of time \(O(mn)\).

#### 5.1.1 \(\textsc {vConst}\) and \(\textsc {vVal}\)

*c*” its vector representation is returned by function \(\textsc {vConst}\). On the other side, function \(\textsc {vVal}\) returns integer representation of a vector like “

*v*”. We define constants “\(\textsc {True}\)” and “\(\textsc {False}\)” using \(\textsc {vConst}\) as follows:Similarly, in order to convert a truth degree like \(r \in [0,1]_\varDelta \), we have:

#### 5.1.2 \(\textsc {vIf}\)

When called like \(\textsc {vIf}(x, {v}_{1}, {v}_{2})\), this returns an OBDD vector whose \(i^\text {th}\) element equates to diagram \({\text {if}}(x, {v}_{1}[i], {v}_{2}[i])\). Parameter *x* is an OBDD, \({v}_{1}\) and \({v}_{2}\) are two vectors with \(d^\prime \) diagrams. \(\textsc {vIf}\) calculates the result iteratively in time \(O(d^\prime )\).

#### 5.1.3 Comparison

*h*. The iteration is of order \(d^\prime \) thus the computational complexity of a comparison operator is \(O(d^\prime 2^{2h})\)

#### 5.1.4 \(\textsc {vAdd}\) and \(\textsc {vSub}\)

Operators \(\textsc {vAdd}\) and \(\textsc {vSub}\) perform element-wise addition and subtraction of two vectors with similar length, the result is obviously a vector of same length. \(\textsc {vAdd}\) and \(\textsc {vSub}\) are also convertible to an iteration of order \(d^\prime \) of logical combination of OBDDs; therefore, they also run in time \(O(d^\prime 2^{2h})\). Similarly, bounded-add and bounded-subtract are permissible by comparison operations and \(\textsc {vIf}\); this indicates that they are of the same order as \(O(d^\prime 2^{2h})\).

#### 5.1.5 Logical connectives

#### 5.1.6 \(\textsc {vMul}\) and \(\textsc {vDiv}\)

Operators \(\textsc {vMul}\) (\(\textsc {vDiv}\)) multiplies (divides) elements of a vector \({v}_{1}\) by a constant factor like *c*. The result is obviously a vector of the same length.

#### 5.1.7 \(\textsc {Add}\) and \(\textsc {Mul}\)

### 5.2 Compiling FzCTL property to OBDD vector

### Property 1

*D*as a vector of variables like \(D = \langle z_d, \dots , z_0\rangle \). Following algorithm is the required procedure to convert OBDD vector \(\tau (\varphi )\), which is represented by \(\theta (U,W)\), into a decimal number to determine the truth degree of proposition \(\varphi \) over an FzPG. Depending on the algorithms certain preprocesses may be involved prior to evaluate truth degree of \(\tau (\varphi )\), some of which are referred later in this paper.

In line 2, we restrict members of vector \(\alpha \) to node \(s_0\) in time \(O(d^\prime 2^h)\), then we restrict members of \(\theta \) to nodes in \(\alpha \) (that is \(s_0\)) in line 4 to create vector \(\lambda \) in time \(O(d^\prime 2^h)\). In lines 6 and 7, the comparison operators are of time complexity of \(O(d^\prime 2^{2(h+d^\prime )})\) and results are of memory complexity of \(O(2^{h+d^\prime })\). In those lines, the universal and existential quantifiers are restriction operators each of which is of time complexity of \(O(2^{h+d^\prime })\). These quantifiers eliminate participant variables in diagrams and reduce the height of corresponding diagrams gradually by one. Conjunction over \(\beta _1\) and \(\beta _2\) forms \(\beta \) in time \(O(2^{2d^\prime })\).

According to properties of \(\sqcap \), \(\beta \) is a composition of minterms of variables \(z_0\) to \(z_d\). In line 10, expression *D*[*i*] represents \(z_i\), so when \(z_i\) participates in \(\beta \), expression \(\rho [i]\) evaluates to 1 otherwise to 0, the complexity of calculating vector \(\rho \) is \(O(2^{d^\prime })\). Finally, dividing \(\textsc {vVal}(\rho )\) by \(2^d\) results in the truth degree of \(\varphi \). This algorithm is of time complexity of \(O(d^\prime 2^{2(h+d^\prime )})\).

### 5.3 Temporal operators

*s*and

*t*. A disjunction over all transition implications forms relation \(\hbox {R}\). In order to add a transition edge to relation \(\hbox {R}\), we initially calculate and store vectors of \({\text {Act}}(s, t)\), then using implication operator we calculate the transition edge that eventually aggregates to \(\hbox {R}\) with a disjunction; please see Algorithm 3.

*B*are both vectors of

*k*rows and each row is consist of \(d^\prime \) elements, OBDDs for these variables is of height \(kd^\prime \). Accordingly, \(\textsc {vEql}(W^\prime _i, B_i)\) is of complexity of \(O(d^\prime 2^{2kd^\prime })\) and therefore \(\textsc {vEql}(W^\prime , B)\) is of time complexity of \(O(kd^\prime 2^{2kd^\prime })\). Line 3, calculates \(\alpha \) in time \(O(2^{2h+1})\) and line 4 runs in time \(O(d^\prime 2^{2h+1})\); subsequently, calculating relation \(\hbox {R}\) is of the following complexity:

#### 5.3.1 EX operator

*D*and vector \(\rho \) (i.e., a vector of diagrams in terms of

*U*and

*W*) as follows:where \(\oplus \) represents eXclusive-OR. In line 8 of algorithm 4, the expression \(\exists D \cdot (D[i] \wedge \psi )\) forms \(\rho [i]\), as for \(D^\prime = \langle z_d,\dots ,z_{i+1},z_{i-1},\dots ,z_0\rangle \) we have:

Bits in \(\theta \) are of height *h* and bits of \(\hbox {R}\) are of height 2*h*. Line 2 forms \(\theta ^\prime \) from \(\theta \) in time \(O(d^\prime 2^h)\). In line 3, \(\lambda \) is formed by applying \(\textsc {And}\) on two vectors of \(d^\prime \) bits which according to (4) is convertible to \(\textsc {vGeq}\) that takes \(O(d^\prime )\) times of conjunctive and disjunctive operations on corresponding bits. Composition of individual bits of \(\theta ^\prime \) and \(\hbox {R}\) is of order \(O(2^{3h})\) and the resulted bit is of height 2*h*. Conjunctive and disjunctive operations on diagrams of height 2*h* is of order \(O(2^{4h})\), which leads us to the computational complexity of \(O(d^\prime 2^{4h})\) and a result of height 2*h* for \(\textsc {vGeq}\). The \(\textsc {vIf}\) is of the same computational complexity therefore total complexity of line 3 is \(O(d^\prime 2^{4h})\).

*h*is required as shown in lines 4 and 5. These comparison operations result in diagrams of maximum height \(d^\prime + h\) in time complexity of \(O(d^\prime 2^{2(h+d^\prime )})\); through a similar reasoning that we used while computing \(\lambda \) in line 3. Universal and existential quantifiers in lines 4 and 5eliminate participant variables in diagrams and reduce the height of corresponding diagrams gradually by one, consequently all predicates in these lines (i.e., \(\lambda \ge D\) and \(\lambda \le D\)) are quantified in time complexity of \(O(2^{2h+d^\prime })\), because we have:

#### 5.3.2 EU operator

*U*and

*W*, consequently \(e=O(2^h)\) and \(g = O(2^{h+d^\prime })\). In practice the convergence happens quickly and this is the worst-case convergence time. Given the computational complexity of \(\textsc {Ex}\) operator, the computational complexity of \(\textsc {Eu}\) is of \(O(d^\prime 2^{5h+d^\prime })\).

#### 5.3.3 AU operator

#### 5.3.4 AX operator

### 5.4 Computational complexity analysis

*k*is naturally a small number and \(r=O(|S |^2) = O(2^{2n})\) then computational complexity of checking \(\varphi \) over a model is of computational complexity of \(O(|\varphi |\times d^\prime 2^{5h+d^\prime })\).

Please note that we are counting computational steps with different scaling parameters. Unlike the general convention of considering computational complexity by the size of state-space, we considered the computational complexity by the length of encoding. The reason for this unorthodox convention is simply that our applications of interest required a speed-accuracy trade-off. In other words, we simply calculated the willingness to respond slowly with fewer errors compared to quick response with relatively more errors.

*S*is the state-space of the FzPG. The computational complexity of our model checking approach with respect to state-space of equal FzKripke is \(S'\) is of \(O(\vert S' \vert ^5)\), which is by no means tight.

Nevertheless, in order to model check a given FzPG, we need to construct the complete state-space of an equal FzKripke including its whole transition edges so that we are able to model check the equal FzKripke structure using the approach in [22]. This is computationally expensive and eventually leads to an state-space explosion; yet, since our approach directly model checks the FzCTL formula on the FzPG, state space explosion is effectively avoided; Sects. 6.1 and Appendix A.2 provide intuitive assessments of our method by reporting practical execution time and memory consumption.

The memory complexity of model checking an FzKripke structure in both approaches is of \(O(\vert S' \vert ^ 2)\). Although simple operations like comparison are of computational complexity of \(O(d)\) while using OBDD, we believe OBDD provides a more compact and more efficient representation of our state-space. Further research is necessary to provide an insightful comparison of these two approaches in terms of expressiveness, applicability, and scalability.

## 6 Fuzzy flip-flops

### 6.1 Fuzzy D Flip-Flop

*p*is a positive integer. We also assume input

*D*is stable and the

*CLK*is a pulse in the following form:

where \(\alpha \) and \(\beta \) are integers. Great values of \(\alpha \) and \(\beta \) do not cause any problems except slowing down the circuit. On the other hand, if \(\alpha \) and \(\beta \) would be smaller than a limit there are no chance for the circuit to stabilize its output therefore it acts incorrectly. We can prove by model checking that this design requires the values of \(\alpha \) and \(\beta \) to be at least 7. Let us assume \(N=\frac{1}{T}\) be the maximum possible value for \(\alpha \) and \(\beta \) (obviously this is an assumption to simplify the modeling problem, greater values would not affect the circuit but slowing it down).

*T*time units; now it is easy to compute the output of each gate considering its inputs. From this point onward we denote

*CLK*as

*C*for further readability.

*CLK*is 0 and being in \(S_1\) conveys the opposite, please see Fig. 4. The attribute set

*X*is as follows:

*T*, therefore on the verge of entering a new state the value for this attribute is 0; whilst on a state, as soon as \(\varGamma \) changes the output of all gates will change accordingly. Attribute

*u*represents the raising edge of the clock pulse; it is set to 1 while the clock is pulse raised. Once

*u*is set it will preserve its value. Participating functions in graph

*G*are defined as:

#### 6.1.1 Properties of multi-valued D flip-flop

In order to verify Choi’s design of multi-valued D flip-flop, we defined its properties using FzCTL and then investigated their correctness using model checking.

### Property 2

*T*after the very first raising edge of clock pulse, we will have \(Q=D\) for the rest of time. This property is expressible in FzCTL as follows:

*D*is input, \({\text {AX}}^n\) denotes applying \({\text {AX}}\) operator

*n*consecutive times. This proposition evaluates to 0.

### Property 3

*T*after the very first raising edge of clock pulse, the possible values for

*Q*are

*D*, \({\overline{D}}\), and 0. This property is expressible in FzCTL as follows:

*T*emerged at time \(t+5T\). As can be observed if \(D<{\overline{D}}\) then on the verge of clock’s falling edge the next value for

*Q*is among

*D*, 0, or \({\overline{D}}\) otherwise if \(D>{\overline{D}}\) then

*Q*is either

*D*or 0. A short while after clock’s rising edge (i.e. less than 6

*T*) the state of circuit will be reverted to column

*t*. As long as clock pulse is high, the state is preserved.

Unstable condition of fuzzy D flip-flop

Time | | \(y_1\) | \(y_2\) | \(y_3\) | \(y_4\) | \(y_5\) | \(y_6\) | \(y_7\) | | |
---|---|---|---|---|---|---|---|---|---|---|

| 1 | 0 | 0 | | | | \({\overline{D}} \sqcup D\) | | | \({\overline{D}}\) |

\(t + T\) | 0 | 1 | 0 | 0 | | | \({\overline{D}} \sqcup D\) | | | \({\overline{D}}\) |

\(t + 2T\) | 0 | 1 | | 0 | 0 | | \({\overline{D}} \sqcup D\) | | | \({\overline{D}}\) |

\(t + 3T\) | 0 | 1 | | 0 | | | \({\overline{D}}\) | | 0 | \({\overline{D}}\) |

\(t + 4T\) | 0 | 1 | 0 | 0 | | | \({\overline{D}} \sqcup D\) | \({\overline{D}} \sqcap D\) | | 1 |

\(t + 5T\) | 0 | 1 | | 0 | 0 | | 1 | | \({\overline{D}} \sqcap D\) | \({\overline{D}}\) |

\(t + 6T\) | 0 | 1 | \({\overline{D}} \sqcap D\) | 0 | | \({\overline{D}} \sqcap D\) | \({\overline{D}}\) | | 0 | \({\overline{D}} \sqcup D\) |

\(t + 7T\) | 0 | 1 | 0 | 0 | \({\overline{D}} \sqcap D\) | | \({\overline{D}} \sqcup D\) | \({\overline{D}} \sqcap D\) | 0 | 1 |

\(t + 8T\) | 0 | 1 | | 0 | 0 | | 1 | | \({\overline{D}} \sqcap D\) | \({\overline{D}}\) |

\(t + 9T\) | 0 | 1 | \({\overline{D}} \sqcap D\) | 0 | | \({\overline{D}} \sqcap D\) | \({\overline{D}}\) | | 0 | \({\overline{D}} \sqcup D\) |

\(t + 10T\) | 0 | 1 | 0 | 0 | \({\overline{D}} \sqcap D\) | | \({\overline{D}} \sqcup D\) | \({\overline{D}} \sqcap D\) | | 1 |

\(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) |

#### 6.1.2 Experimental results

We ran the experiments on a laptop with 4GBytes of RAM with Intel\(^\circledR \) Core^{TM}2 Due (2.6 G.Hz.) CPU that runs Windows XP Professional (32bits). We used BuDDy library [16] to implement proposed algorithms because this library provides a near comprehensive set of tools and functions to work with OBDDs and their vectors. In this library nodes of all diagrams are stored and retrieved by a hashing method. The total size allocated for each node is 20 bytes and the upper bound for number of nodes is initialized by function “bdd_init” which we set it to 100,000,000; that is, a total memory of 2GBytes. Due to memory space constraints, as soon as 70% of the allocated memory is consumed, we reorder diagrams to reduce number of nodes as well as consumed memory.

*T*to any value ranging from \(2^{-6}\) to \(2^{-3}\) did not affect the results yet it affected memory consumption and execution time of the proposed model checker. Meanwhile, Table 3 presents the practical orders on computational power and memory space needed for our proposed method. As can be seen by reported computational and memory complexity are not tight.

Given \(h=5\) and considering different values of \(\alpha \) and \(\beta \), we recorded number of calls to \(\textsc {Ex}\) operator (\(\#\textsc {Ex}\)), execution time in milliseconds, and memory consumption in terms of BDD nodes

\(\alpha \) | \(\beta \) | \(\# \textsc {Ex}\) | Time (ms) | #Nodes |
---|---|---|---|---|

8 | 8 | 23 | 918 | 632,944 |

16 | 8 | 31 | 1639 | 1,040,096 |

8 | 16 | 31 | 1954 | 1,171,231 |

16 | 16 | 39 | 2441 | 1,314,031 |

24 | 8 | 39 | 2673 | 1,436,208 |

8 | 24 | 39 | 3046 | 1,613,500 |

32 | 8 | 47 | 3832 | 1,742,449 |

16 | 24 | 47 | 3924 | 1,882,932 |

24 | 16 | 47 | 3974 | 1,838,548 |

24 | 24 | 55 | 4645 | 1,969,160 |

32 | 16 | 55 | 5854 | 2,183,117 |

8 | 32 | 47 | 6365 | 2,090,664 |

32 | 24 | 63 | 7121 | 2,457,824 |

16 | 32 | 55 | 8082 | 2,390,179 |

24 | 32 | 63 | 10,430 | 2,622,073 |

32 | 32 | 71 | 13,006 | 2,652,580 |

Given \(\alpha T = \beta T = \frac{1}{2}\) we recorded the state-space size, number of calls to \(\textsc {Ex}\) operator (\(\#\textsc {Ex}\)), execution time in milliseconds, and memory consumption in terms of BDD nodes for different values of *h*

| State-space | \(\#\textsc {Ex}\) | Time (ms) | #Nodes |
---|---|---|---|---|

4 | \(2^{35}\) | 23 | 660 | 526,395 |

5 | \(2^{42}\) | 39 | 2441 | 1,314,031 |

6 | \(2^{49}\) | 71 | 21,206 | 2,821,965 |

7 | \(2^{56}\) | 135 | 129,730 | 5,715,114 |

8 | \(2^{63}\) | 263 | 431,222 | 11,358,475 |

9 | \(2^{70}\) | 519 | 1,530,087 | 22,485,129 |

\(O(2^{7h+7})\) | \(O(2^{h}+7)\) | \(O(2^{1.85h+4})\) | \(O(2^{h+15.44})\) |

### 6.2 Fuzzy J-K flip-flop

In this subsection we are destined neither to provide an on-chip fuzzy system nor their applications but a formal model realizing a fuzzy flip-flops.

#### 6.2.1 Fuzzy NAND gate

#### 6.2.2 Properties of fuzzy J-K flip-flop

Obviously, inputs and outputs of fuzzy \({\text {NAND}}\) gate are decimals from [0, 1]. Suppose numbers smaller or equal to 0.25 as low and numbers larger or equal to 0.75 as high and the numbers in-between these two bounds as invalid values. According to Fig. 5 the following properties holds for each fuzzy J-K flip-flop.

### Property 4

If *J* is high and *K* is low at the clock edge, then *Q* output is forced high and stays high while \({\overline{Q}}\) is forced low and stays low for sure. Note that at the beginning initial values of *Q* and \({\overline{Q}}\) are random and even may be invalid values like 0.5.

*G*there is a condition in which flip-flop works improperly (and that is when the initial state values for the

*Q*and \({\overline{Q}}\) are invalid) thus the property is incorrect and proposition \(P_1\) evaluates to 0; see Table 4 for traces and configuration of model. By substitution of \({\text {NAND}}_1\) with \({\text {NAND}}_2\), proposition \(P_1\) (for all \(\varepsilon \ge 0.25\)) evaluates to 1, and the property always holds.

Unstable condition of Fuzzy J-K flip-flop using \({\text {NAND}}_1\)

Step | | | | \({\overline{Q}}\) |
---|---|---|---|---|

0 | 0.75 | 0.25 | 0.5 | 0.625 |

1 | 0.75 | 0.25 | 0.625 | 0.5 |

2 | 0.75 | 0.25 | 0.5 | 0.375 |

3 | 0.75 | 0.25 | 0.625 | 0.375 |

4 | 0.75 | 0.25 | 0.5 | 0.375 |

5 | 0.75 | 0.25 | 0.625 | 0.375 |

6 | 0.75 | 0.25 | 0.5 | 0.375 |

\(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) | \(\vdots \) |

## 7 Conclusion and future work

We defined *Quantized FzKripke* as a variant of multi-valued Kripke structure on interval \([0,1]_\varDelta \). We also defined FzCTL as the modal temporal logic to express temporal properties of FzKripke. A series of operators like quasi-comparison, bounded-add, bounded-subtract, and scalar-multiplication on discrete interval are defined in FzCTL that are rarely seen in other logics introduced prior to this. This gives FzCTL the ability to specify sophisticated behaviors of fuzzy systems easily.

Having defined a powerful fuzzy temporal logic, we paired it with FzPG as the modeling structure. This is a more convenient structure to model fuzzy systems due to its compactness and readability. Moreover, we introduced *Quantized FzPG* such that it is convertible to Quantized FzKripke. In order to model check an FzCTL formula \(\varphi \) over an FzPG a translation to an equivalent FzKripke with an exponential blow-up was inevitable leading to state-space explosion. By the means of OBDD vectors, we devised a symbolic method that can perform direct checking of \(\varphi \) on a Quantized FzPG avoiding the aforementioned exponential blow-up.

In order to demonstrate the applicability of our method, we formally investigated the correctness of a multi-valued D Flip-Flop as a case study, and showed a flaw in the circuitry that is not seen in design phase with computer simulations. This flaw yields to a dynamic hazard making the whole flip-flop unstable under certain initial conditions. Afterwards, by investigating a potential design for Fuzzy J-K Flip-Flops, we demonstrated how the proposed method can be useful in design phase of such intuitive circuits for analyzing their complex behaviors.

Considering the expressibility of FzCTL, compactness and readability of FzPG, our method is affordable in terms of memory and computational complexity. We believe further investigation is needed to compare our proposed method with a relevant method introduced in [22] in terms of expressiveness, scalability, and applicability for real-world scenarios. We believe it is not the case that these methods are not equivalent but making this comparison is initially difficult because the modeling structure in [22], i.e., FzKripke structure, is by an exponential factor larger than FzPG and the model checking method in [22] follows a different theoretical base.

Furthermore, an improved implementation for \(\textsc {Ex}\) operator is proposed in Appendix A, which is of lower memory and computational complexity. Not only we analysed the worst case complexity of all algorithms in this paper but we also implemented our method and made an intuitive assessment. Appendix A.2 reads about practical performance analysis of the proposed method through an intuitive assessment.

We had covered all preliminaries about abstraction and approximation in fuzzy temporal logic and models in a discrete setup [26]; and now we covered a symbolic model checker that deals with state-space explosion in the same setup. The ultimate goal of this series of research is to apply formal verification in field of fuzzy control systems. To this purpose, it is required to define some extensions to our modeling, specification, and verification approach. For future research our intention is to perceive concrete time in form of fuzzy sets and also to include natural language propositions in an augmented fuzzy extended temporal logic.

## Notes

### Acknowledgements

Open access funding provided by Graz University of Technology. The authors would like to thank anonymous reviewers for their valuable comments and suggestions that improved the quality of this manuscript.

## Supplementary material

## References

- 1.Avrachenkov, K., Sanchez, E.: Fuzzy markov chains and decision-making. FO & DM
**1**(2), 143–159 (2002). https://doi.org/10.1023/A:1015729400380. MathSciNetzbMATHGoogle Scholar - 2.Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008). https://doi.org/10.1093/comjnl/bxp025. http://mitpress.mit.edu/books/principles-model-checking
- 3.Baresi, L., Pasquale, L., Spoletini, P.: Fuzzy goals for requirements-driven adaptation. In: 2010 18th IEEE International Requirements Engineering Conference, pp. 125–134. IEEE (2010). https://doi.org/10.1109/RE.2010.25. http://staff.lero.ie/lpasqua/files/2012/02/RE2010.pdf, http://ieeexplore.ieee.org/lpdocs/epic03/wrapper.htm?arnumber=5636887
- 4.Bianco, A., de Alfaro, L.: Model Checking of Probabilistic and Nondeterministic Systems, pp. 499–513. Springer, Berlin (1995). https://doi.org/10.1007/3-540-60692-0_70 CrossRefzbMATHGoogle Scholar
- 5.Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: Proceedings of Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12–16, 2004, pp. 281–293 (2004). https://doi.org/10.1007/978-3-540-27836-826
- 6.Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol: TOSEM
**12**(4), 371–408 (2003)CrossRefzbMATHGoogle Scholar - 7.Chechik, M., Gurfinkel, A., Devereux, B., Lai, A., Easterbrook, S.: Data structures for symbolic multi-valued model-checking. Form. Methods Syst. Des.
**29**(3), 295–344 (2006). https://doi.org/10.1007/s10703-006-0016-z CrossRefzbMATHGoogle Scholar - 8.Choi, B., Shukla, K.: Multi-valued logic circuit design and implementation. Int. J. Electron. Electr. Eng.
**3**(4), 256–262 (2015)Google Scholar - 9.Frigeri, A., Pasquale, L., Spoletini, P.: Fuzzy time in linear temporal logic. ACM Trans. Comput. Log.
**15**(4), 30:1–30:22 (2014). https://doi.org/10.1145/2629606 MathSciNetCrossRefzbMATHGoogle Scholar - 10.Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput.
**6**(5), 512–535 (1994). https://doi.org/10.1007/BF01211866 CrossRefzbMATHGoogle Scholar - 11.Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27–30, 1996, pp. 278–292. IEEE Computer Society (1996). https://doi.org/10.1109/LICS.1996.561342
- 12.Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci.
**57**(1), 94–124 (1998). https://doi.org/10.1006/jcss.1998.1581. http://www.sciencedirect.com/science/article/pii/S0022000098915811 - 13.Hirota, K., Ozawa, K.: The concept of fuzzy flip-flop. IEEE Trans. Syst. Man Cybern.
**19**(5), 980–997 (1989). https://doi.org/10.1109/21.44013. http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=44013’escapeXml=’false’/> - 14.Hirota, K., Pedrycz, W.: Design of fuzzy systems with fuzzy flip-flops. IEEE Trans. Syst. Man Cybern.
**25**(1), 169–176 (1995). https://doi.org/10.1109/21.362956 CrossRefGoogle Scholar - 15.Liang, W., Bing-wen, W., Yi-Ping, G.: Cell mapping description for digital control system with quantization effect. Technical report (2007). http://arxiv.org/abs/0712.2501
- 16.Lind-Nielsen, J.: BuDDy—A Binary Decision Diagram Package. IT-TR. Department of Information Technology, Technical University of Denmark, Lyngby (1996)Google Scholar
- 17.Moon, S., Lee, K.H., Lee, D.: Fuzzy branching temporal logic. IEEE Trans. Syst. Man Cybern. Part B
**34**(2), 1045–1055 (2004)CrossRefGoogle Scholar - 18.Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Form. Methods Syst. Des.
**43**(2), 164–190 (2013)CrossRefzbMATHGoogle Scholar - 19.Ozawa, K., Hirota, K., Koczy, L.: Fuzzy flip-flop. In: Patyra, M.J., Mlynek, D.M. (eds.) Fuzzy Logic. Implementation and Applications, pp. 197–236. Wiley, Chichester (1996)Google Scholar
- 20.Ozawa, K., Hirota, K., Koczy, L.T., Pedrycz, W., Ikoma, N.: Summary of fuzzy flip-flop. In: Proceedings of 1995 IEEE International Conference on Fuzzy Systems, vol. 3 (1995). https://doi.org/10.1109/FUZZY.1995.409897
- 21.Palshikar, G.K.: Representing fuzzy temporal knowledge. In: International Conference on Knowledge-Based Systems (KBCS-2000), pp. 252–263. Mumbai, India (2000)Google Scholar
- 22.Pan, H., Li, Y., Cao, Y., Ma, Z.: Model checking fuzzy computation tree logic. Fuzzy Sets Syst.
**262**, 60–77 (2015)MathSciNetCrossRefzbMATHGoogle Scholar - 23.Pedrycz, W.: Fuzzy Control and Fuzzy Systems (\(2{nd}\), extended edn. Research Studies Press Ltd., Taunton (1993)Google Scholar
- 24.Pnueli, A.: Current trends in concurrency. Overviews and tutorials. In: Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends, pp. 510–584. Springer, New York (1986). http://dl.acm.org/citation.cfm?id=19518.19527
- 25.Sladoje, N.: On analysis of discrete spatial fuzzy sets in 2 and 3 dimensions. Ph.D. thesis, Swedish University of Agricultural Sciences Uppsala (2005). http://pub.epsilon.slu.se/963/1/ThesisNSladoje.pdf
- 26.Sotudeh, G., Movaghar, A.: Abstraction and approximation in fuzzy temporal logics and models. Form. Asp. Comput.
**27**, 1–26 (2014). https://doi.org/10.1007/s00165-014-0318-7 MathSciNetzbMATHGoogle Scholar - 27.Whittle, J., Sawyer, P., Bencomo, N., Cheng, B.H., Bruel, J.M.: RELAX: incorporating uncertainty into the specification of self-adaptive systems. In: 2009 17th IEEE International Requirements Engineering Conference, pp. 79–88. IEEE, Atalanta, Georgia (2009). https://doi.org/10.1109/RE.2009.36
- 28.Wierman, M.: An Introduction to the Mathematics of Uncertainty, p. 133. Creighton University (2010). http://typo3.creighton.edu/fileadmin/user/CCAS/programs/fuzzy_math/docs/MOU.pdf
- 29.Zadeh, L.A.: Probability Theory and Fuzzy Logic. https://pdfs.semanticscholar.org/38a2/90e1d109427869ca95904457e45c2265d117.pdf. Accessed 23 Jan 2017

## Copyright information

**Open Access**This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.