Safety and liveness are fundamental to many system verification paradigms. In contrast to existing approaches for extending safety and liveness properties of fuzzy systems, we first utilize ultrametric to measure the similarity of valuations, traces and properties in a fuzzy Kripke structure (FKS). A distance threshold $\alpha$ is introduced, which is used to define two quantitative extensions of safety and liveness properties, called $\alpha$-safety and $\alpha$-liveness properties. In addition, we provide characterizations of $\alpha$-safety and $\alpha$-liveness properties in terms of Büchi automata. These results will provide the foundation for the verification of fuzzy systems.

Metric transition systems (MTSs) are proposed for quantitative verification of reactive systems. There are already a number of papers on quantitatively analyzing behaviors of systems based on MTSs. In this article, we make further progress along this research line by lifting safety properties, which assert that nothing “bad” happens during execution of systems, to MTSs. First, we introduce a distance threshold$\alpha \ \text{taken from [0,1],}$which is used to analyze to what extent a system satisfies its specification. Then, we present a quantitative extension of safety properties, called$\alpha$-safety properties. Furthermore, we give an alternative characterization of$\alpha$-safety properties by means of their closure. In addition, an algorithm for verifying whether a system satisfies a subclass of$\alpha$-safety properties is developed, assuming that the method to convert a regular$\alpha$-safety property to an equivalent metric finite automaton has been given. Finally, we present an example to illustrate our approaches.

Refinement relations, such as trace containment, simulation preorder, and their alternating versions, have been successfully applied in formal verification of concurrent systems. Recently, trace containment and simulation preorder have been adopted and developed in fuzzy systems, but the generalization of their alternating versions to fuzzy systems has not been investigated. To satisfy the need for modeling and analyzing fuzzy systems, this article proposes two types of refinement relations called fuzzy alternating trace containment and fuzzy alternating simulation preorder, based on fuzzy concurrent game structures (FCGSs) under the Gödel semantics. These two fuzzy notions inherit properties from the corresponding classical setting. For example, fuzzy alternating simulation preorder for finite-state FCGSs can be computed in polynomial time; fuzzy alternating simulation preorder is a fuzzy subset of fuzzy alternating trace containment, and both relations can be logically characterized in terms of fuzzy version of alternating-time temporal logic. These properties make the theory developed here suitable for the modeling and verification of fuzzy systems.

The computational study on finite/infinite-state systems, probabilistic systems, and finite-state fuzzy systems, has received much attention recently. In contrast, there are very few results for algorithmic analysis of infinite-state fuzzy systems. In this paper, we introduce fuzzy pushdown termination games (FPDTGs), which are an extension of fuzzy pushdown automata with a game feature and can serve as a formal model of infinite-state fuzzy systems. We investigate some computational issues of the games under termination objectives for two players: the goal of player-1 is to maximize the truth value of eventually terminating at some given configurations with the empty stack, while player-2 aims at the opposite. Some interesting results are obtained. For example, we show that both players have optimal memoryless strategies and the same value. The problem of computing the value can be solved in exponential time when the triangular norm is chosen as the minimum one. Furthermore, we present efficient algorithms for computing the values of two special subclasses of FPDTGs. The potential for practical use of our model is demonstrated by a case study on a manufacturing system.

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.

To model and analyze systems with multi-valued information, in this paper, we present an extension of Kripke structures in the framework of complete residuted lattices, which we will refer to as lattice-valued Kripke structures (LKSs). We then show how the traditional trace containment and equivalence relations, can be lifted to the lattice-valued setting, and we introduce two families of lattice-valued versions of the relations. Further, we explore some interesting properties of these relations. Finally, we provide logical characterizations of our relations by a natural extension of linear temporal logic.

In this paper, we define lattice-valued labeled transition systems (LLTS) as a general framework for allowing imprecise or incomplete specifications to be expressed. We introduce a lattice-valued bisimulation between LLTSs that measures the degree of closeness of two systems as elements of residuated lattice, in contrast to the traditional boolean yes/no to bisimulation. Also, we show that our bisimulation is compositional for a synchronous composition operator. Moreover, we also consider lattice-valued extension of Kripke structures, define a lattice-valued bisimulation between lattice-valued Kripke structures (LKSs), and establish the correspondence between lattice-valued bisimulation in LLTS and lattice-valued bisimulation in LKS.

Many researchers suggested extending bisimilarity to quantitative versions to avoid the rigidity of classical bisimilarity. To explore the relation between different notions of approximate bisimilarity mentioned in literature, in this paper, we present a quantitative extension of doubly labeled transition systems, MDLTS, where its states and actions form metric spaces. We then introduce two notions of approximate bisimilarity, (η, λ)-bisimilarity and (η, λ, α)-bisimilarity, and discuss their basic property. We also consider the special kind of (η, λ)-bisimilarity, λ-bisimilarity to characterize the branching distance with arbitrary discount α of metric labeled transition system. Finally, we discuss the translation between metric transition system and MDLTS which preserves the approximate bisimilarity.