Fuzzy Alternating Refinement Relations Under the Godel Semantics

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 Godel 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.