Model checking possibilistic linear-time properties was investigated by Li in 2017. However, nondeterminism of the system is absent in previous studies. Therefore, in order to permit both possibilistic and nondeterministic choices, we use the generalized possibilistic decision process (GPDP) as a model of the system. First, the definition of GPDP describing the behavior of nondeterministic system is given in detail, the resolution of nondeterminism is performed by using the notion of schedulers, and the semantics of generalized possibilistic linear-temporal logic (GPoLTL) with schedulers are defined. Second, we study possibilistic model checking of some fuzzy linear-time properties under GPDP. Since there are many (infinite) schedulers satisfying a certain linear timing property in a given state of a GPDP, it is particularly critical to study the optimal strategy and its corresponding possible measure, which is called extremal possibility model checking. For some special fuzzy linear-time properties, such as constrained reachability, step-bounded constrained reachability, reachability, always reachability, repeated reachability, persistence reachability, we present complete solution to the optimal (including maximum and minimum cases) possibilistic model checking of the above reachability using the fixpoint techniques. We also introduce fuzzy$\omega$-regular properties in GPDP and show that their model checking can be simplified by repeated reachability. The algorithms for model checking are also provided. Additionally, an example is presented to illustrate the methods described in the article.

Probabilistic model checking has received increasing attention in formal verification. Meanwhile, in the fuzzy setting, the possibilistic model checking has been well studied by Li et al. in recent years. However, nondeterminism of choices was not considered in previous work. The nondeterminism is crucial for modeling open systems interacting with the environment. To fill the gap, we propose the possibilistic decision processes (PDPs) to model fuzzy systems with nondeterminism and introduce possibilistic strategy computation tree logic (PoSCTL) to specify properties with nondeterministic choices. More importantly, optimal strategy model checking over PDPs has been investigated, which is an important formal verification method for quantitatively checking the degree of satisfiability of properties in a model. We give mathematical methods to calculate the maximum and minimum possibilities for a system modeled by PDPs satisfies a property specified by PoSCTL when ranging over all strategies. We prove memoryless strategies are sufficient for PoSCTL model checking without the step-bounded until operator, and give the algorithms to output the corresponding optimal strategy. Finally, an illustrative example of robots moving is given to explain the methods presented in this article.

Based on the Kripke structure, linear temporal logic and generalized possibility measure, this article studies the model checking problems of generalized possibilistic fuzzy linear temporal logic (GPoFTL). The generalized possibilistic Kripke structure is introduced to describe the system model. The syntax of GPoFTL, which includes fuzzy temporal operators such as ``soon'', ``presently'', ``gradually'', ``within'', ``last'', ``nearly always'', ``almost alwayss'', ``in the long distant future'', ``in the middle of'', ``nearly until'' and ``almost until'', and its language semantics and path semantics under generalized possibility measure are given. Next, we explain the semantics of fuzzy temporal operators through some examples and prove that GPoFTL is an extension of generalized possibilistic linear temporal logic in fuzzy time temporal logic. Furthermore, the GPoFTL model checking algorithm is given by explicit calculation formulas one by one for any GPoFTL formula involving fuzzy temporal operators using fuzzy matrix operations. Last, the algorithm of necessary threshold model checking of GPoFTL is studied using automata theory and its time complexity is discussed.

This paper investigates the approximate bisimulation relations for fuzzy automata in order to study the approximate minimization problem of fuzzy automata. For a small positive real number ∈, we introduce the notion of ∈-bisimulation relations between two fuzzy automata, and prove that the behavior of a fuzzy automaton A differs by ∈ from the behavior of a fuzzy automaton B under a ∈-bisimulation relation between them. Also, the notion of surjective functional ∈-bisimulation relations between two fuzzy automata is defined. According to surjective functional ∈-bisimulation relations, we discuss ∈-bisimulation relations for a fuzzy automaton. A construction of aggregated fuzzy automaton by the given ∈-bisimulation for a fuzzy automaton is given. Furthermore, we find that there might not exist the greatest ∈-bisimulation relation for a fuzzy automaton, and we novelly give an effective algorithm to construct all maximal ∈-bisimulation relations for the given fuzzy automaton. Finally, we point out that bisimulation relations for a fuzzy automaton are also ∈-bisimulation relations, the conditions for the real number ∈ to ensure the existence of the greatest ∈-bisimulation are also discussed.

In this paper, we study the relationship between ordering structures on semirings and semiring-induced valuation algebras. We show that a semiring-induced valuation algebra is a complete (resp. continuous) lattice if and only if the semiring is complete (resp. continuous) lattice with respect to the reverse order relation on semirings. Furthermore, a semiring-induced information algebra is compact, if the dual of the semiring is an algebraic lattice.

Two-player turn-based games on graphs (or game graphs for short) and their probabilistic versions have received increasing attention in computer science, especially in the formal verification of reactive systems. However, in the fuzzy setting, game graphs are yet to be addressed, although some practical applications, such as modeling fuzzy systems that interact with their environments, appeal to such models. To fill the gap, in this paper, we propose a fuzzy version of game graphs and focus on the fuzzy game graphs with reachability objectives, which we will refer to as fuzzy reachability games (FRGs). In an FRG, the goal of one player is to maximize her truth value of reaching a given target set, while the other player aims at the opposite. In this framework, we show that FRGs are determined in the sense that for every state, both of the two players have the same value, and there exist optimal memoryless strategies for both players. Moreover, we design algorithms, which achieve polynomial time complexity in the size of the FRG, to compute the values of all states and the optimal memoryless strategies for the players. For a special class of FRGs, we provide an improved algorithm that achieves linear-logarithmic running time to compute the values of states. In addition, several examples are given to illustrate our motivation and the theoretical development.

Model checking of linear-time properties based on possibility measures was developed by Li and Li (2013). However, the linear-time properties considered in the previous work were classical and qualitative, possibility information of the systems was not considered thoroughly at all. Therefore, the quantitative model checking of fuzzy linear-time properties based on generalized possibility measures was studied by Li (2016). This paper is a continuation of the above work. In this paper, we study the expressive power of possibilistic linear-temporal logic (PoLTL). Unlike possibilistic computation tree logic (PoCTL) in which the expressiveness of PoCTL is more powerful than computation tree logic (CTL), it is surprising that PoLTL is as expressive as linear-temporal logic (LTL). Furthermore, the comparison between PoLTL and generalized PoLTL (GPoLTL) is given. It is shown that the expressiveness of GPoLTL with restrained conditions is the same as PoLTL when semantics of GPoLTL is interpreted in the frame of possibilistic Kripke structure.

ABSTRACT There are several methods to construct multi‐secret sharing schemes, one of which is based on coding theory. Generally, however, it is very hard to determine the minimal access structures of the schemes based on linear codes. In this paper, we first propose the concept of minimal linear codes so as to make it easier to determine the access structures of the schemes based on the duals of minimal linear codes. It is proved that the shortening codes of minimal linear codes are also minimal ones. Then we present the algorithm to determine whether a class of linear codes are minimal. On the basis of our aforementioned studies, we further devise a new multi‐use multi‐secret sharing scheme based on the dual code of a minimal linear code, where each participant has to carry only one share. Furthermore, we study the minimal access structures of the multi‐secret sharing scheme and present specific examples through programming. Copyright © 2014 John Wiley & Sons, Ltd.

We study generalized possibilistic computation tree logic (GPoCTL) model checking in this paper, which is an extension of possibilistic computation logic model checking introduced by Li et al. (2014). The system is modeled by generalized possibilistic Kripke structures, and the verifying property is specified by a GPoCTL formula. Based on generalized possibility measures and generalized necessity measures, the method of GPoCTL model checking is discussed, and the corresponding algorithm and its complexity are shown in detail. Furthermore, the comparison between possibilistic computation tree logic and GPoCTL is given. Finally, a thermostat example is given to illustrate the GPoCTL model-checking method.

In this paper, the concepts of weighted transducers over strong bimonoids and their input-output-functions are introduced. Further more, the input-functions and output-functions induced by the input-output-functions of weighted transducers over strong bimonoids are given. It is the most important that the input-functions and output-functions of weighted transducers over strong bimonoids can be realized by weighted finite automata over strong bimonoids, and the realization does not depend on the distributive law, which also embodies the applications of weighted finite automata over strong bimonoids.

In this paper, the role of local finiteness of truth values domain of fuzzy automata is analyzed, in which the truth value domain of fuzzy automata is the (commutative) lattice-ordered monoid. We introduce a hierarchy of lattice-valued fuzzy finite automata and the languages which were recognized by these automata. Besides, the role of local finiteness of truth value domain of fuzzy languages to the hierarchy of fuzzy automata, the role of some special archimedean t-norms in the hierarchy of fuzzy automata and the decidability of lattice-valued languages are also discussed.

In this paper, we introduce the notion of lattice-valued fuzzy residual finite automaton (LRFA) and the LRFA-regular language with membership values in a complete residu-ated lattice. Next, we define saturation operator and reduction operator on lattice-valued finite automata(Li'M), which provide a way to simplify LRFA based on their closure properties in LRFA. At last, we define the canonical LRFA based on the notion of irreducible residual language, prove that every LRFA-regular language is recognized by a unique canonical LRFA which has a minimal number of states and largest initial and transition functions.

Using possibility measure, we study model checking of linear-time properties in possibilistic Kripke structures. First, the notion of possibilistic Kripke structures and the related possibility measure are introduced, and then, model checking of reachability and repeated reachability linear-time properties in finite possibilistic Kripke structures are studied. Standard safety properties and ω-regular properties in possibilistic Kripke structures are introduced; the verification of regular safety properties and ω-regular properties using finite automata are thoroughly studied. It has been shown that the verification of regular safety properties and ω-regular properties in a finite possibilistic Kripke structure can be transformed into the verification of reachability properties and repeated reachability properties in the product possibilistic Kripke structure that is introduced in this paper. Several examples are given to illustrate the methods that are presented in this paper.

In this paper (strong) continuity of domain-free information algebras and labeled information algebras are introduced. Relationships between domain-free information algebras and labeled information algebras are mainly explored. It is shown that continuity and compactness can be preserved under certain canonical correspondences between domain-free information algebras and labeled information algebras. Some equivalent characterizations and examples for continuous information algebras are also given.

In this paper, fuzzy Turing machines with membership degrees in distributive lattices, which are called lattice-valued fuzzy Turing machines, are studied. First several formulations of lattice-valued fuzzy Turing machines, including in particular deterministic and nondeterministic lattice-valued fuzzy Turing machines (l-DTMcs and l-NTMs), are given. It is shown that l-DTMcs and l-NTMs are not equivalent as the acceptors of fuzzy languages. This contrasts sharply with classical Turing machines. Second, it is shown that lattice-valued fuzzy Turing machines can recognize n-r.e. sets in the sense of Bedregal and Figueira, the super-computing power of fuzzy Turing machines is established in the lattice-setting. Third, it is demonstrated that the truth-valued lattice being finite is a necessary and sufficient condition for the existence of a universal lattice-valued fuzzy Turing machine. For an infinite distributive lattice with a compact metric, it is declared that a universal fuzzy Turing machine exists in an approximate sense. This means, for any prescribed accuracy, there is a universal machine that can simulate any lattice-valued fuzzy Turing machine on it with the given accuracy.

In this paper, we generalize Ying's model of linguistic quantifiers [M.S. Ying, Linguistic quantifiers modeled by Sugeno integrals, Artificial Intelligence, 170 (2006) 581-606] to intuitionistic linguistic quantifiers. An intuitionistic linguistic quantifier is represented by a family of intuitionistic fuzzy-valued fuzzy measures and the intuitionistic truth value (the degrees of satisfaction and non-satisfaction) of a quantified proposition is calculated by using intuitionistic fuzzy-valued fuzzy integral. Description of a quantifier by intuitionistic fuzzy-valued fuzzy measures allows us to take into account differences in understanding the meaning of the quantifier by different persons. If the intuitionistic fuzzy linguistic quantifiers are taken to be linguistic fuzzy quantifiers, then our model reduces to Ying's model. Some excellent logical properties of intuitionistic linguistic quantifiers are obtained including a prenex norm form theorem. A simple example is presented to illustrate the use of intuitionistic linguistic quantifiers.

We introduce fuzzy monadic second-order (LMSO-) logic and prove that the behaviours of fuzzy finite automata with membership values in an MV-algebra are precisely the fuzzy languages definable with sentences of our LMSO logic. This generalizes Büchi’s and Elgot’s fundamental theorems to fuzzy logic setting. We also consider fuzzy first-order logic and show that star-free fuzzy languages and aperiodic fuzzy languages introduced here coincide with the fuzzy first-order definable ones.

In this paper, we study some variants of fuzzy Turing machines (FTMs) and universal FTM. First, we give several formulations of FTMs, including, in particular, deterministic FTMs (DFTMs) and nondeterministic FTMs (NFTMs). We then show that DFTMs and NFTMs are not equivalent as far as the power of recognizing fuzzy languages is concerned. This contrasts sharply with classical TMs. Second, we show that there is no universal FTM that can exactly simulate any FTM on it. But if the membership degrees of fuzzy sets are restricted to a fixed finite subset$A$of [0,1], such a universal machine exists. We also show that a universal FTM exists in some approximate sense. This means, for any prescribed accuracy, that we can construct a universal machine that simulates any FTM with the given accuracy. Finally, we introduce the notions of fuzzy polynomial time-bounded computation and nondeterministic fuzzy polynomial time-bounded computation, and investigate their connections with polynomial time-bounded computation and nondeterministic polynomial time-bounded computation.

Fuzzy reasoning is intensively used in intelligent systems including fuzzy control, classification, expert systems, and networks to name a few dominant categories of such architectures. As being a fundamental construct permeating so many diverse areas, fuzzy reasoning was studied with respect to its fundamental properties such as robustness. The notion of robustness or sensitivity becomes of paramount importance by leading to a more comprehensive understanding of the way in which reasoning processes are developed. In this study, we introduce and study properties of some measures of robustness (or sensitivity) of fuzzy connectives and implication operators and discuss their relationships with perturbation properties of fuzzy sets. The results produced here are compared and contrasted with the previous findings available in the literature. © 2005 Wiley Periodicals, Inc. Int J Int Syst 20: 393–413, 2005.

Relational composition-based reasoning has become the most prevalent method for qualitative reasoning since Allen's 1983 work on temporal intervals. Underlying this reasoning technique is the concept of a jointly exhaustive and pairwise disjoint set of relations. Systems of relations such as RCC5 and RCC8 were originally developed for ideal regions, not subject to imperfections such as vagueness or fuzziness which are found in many applications in geographic analysis and image understanding. This paper, however, presents a general method for classifying binary topological relations involving fuzzy regions using the RCC5 or the RCC8 theory. Our approach is based on fuzzy set theory and the theory of consonant random set. Some complete classifications of topological relations between fuzzy regions are also given. Furthermore, two composition operators on spatial relations between fuzzy regions are introduced in this paper. These composition operators provide reasonable relational composition-based reasoning engine for spatial reasoning involving fuzzy regions.