Computing crisp simulations for fuzzy labeled transition systems

The problem of checking whether a state in a finite fuzzy labeled transition system (FLTS) crisply simulates another is one of the fundamental problems of the theory of FLTSs. This problem is of the same nature as computing the largest crisp simulation between two finite FLTSs. A naive approach to the latter problem is to crisp the given FLTSs and then apply one of the currently known best methods to the obtained crisp labeled transition systems. The complexity of the resulting algorithms is of order O (l (m + n) n), where l is the number of fuzzy values occurring in the specification of the input FLTSs, m is the number of transitions and n is the number of states of the input FLTSs. In the worst case, l can be m + n and O (l (m + n) n) is the same as O ((m + n) 2 n). In this article, we design an efficient algorithm with the complexity O ((m + n) n) for computing the largest crisp simulation between two finite FLTSs. This gives a significant improvement. We also adapt our algorithm to computing the largest crisp simulation between two finite fuzzy automata.

A Unifying Coalgebraic Semantics Framework for Quantum Systems

As a quantum counterpart of labeled transition system (LTS), quantum labeled transition system (QLTS) is a powerful formalism for modeling quantum programs or protocols, and gives a categorical understanding for quantum computation. With the help of quantum branching monad, QLTS provides a framework extending some ideas in non-deterministic or probabilistic systems to quantum systems. On the other hand, quantum finite automata (QFA) emerged as a very elegant and simple model for resolving some quantum computational problems. In this paper, we propose the notion of reactive quantum system (RQS), a variant of QLTS capturing reactive system behavior, and develop a coalgebraic semantics for QLTS, RQS and QFA by an endofunctor on the category of convex sets, which has a final coalgebra. Such a coalgebraic semantics provides a unifying abstract interpretation for QLTS, RQS and QFA. The notions of bisimulation and simulation can be employed to compare the behavior of different types of quantum systems and judge whether a coalgebra can be behaviorally simulated by another.

A LTS Approach to Control in Event-B

In Event-B, people need to use control variables to constrain the order of events, which is a time-consuming and error-prone process. This paper presents a method of combining labeled transition system and iUML-B to complete the behavior modeling of system, which is more convenient and practical for engineers who are accustomed to using the automaton to build a system behavior model. First, we use labeled transition system to establish the behavior model of the system. Then we simulate and verify the event traces of the labeled transition system behavior model. Finally, we convert labeled transition system model into iUML-B state machine and use it to generate the corresponding control flow model. We use Abrial’s bounded retransmission protocol to demonstrate the practicality of our approach. The simulation results show that the system behavior model generated by the iUML-B state machine has the same event trace as the corresponding labeled transition system model.

Fuzzy Labeled Transition Refinement Tree

This paper aims to provide a formal framework that supports an incremental development of dynamic systems such as multi agents systems (MAS). We propose a fuzzy labeled transition system model (FLTS for short). FLTS allows a concise action refinement representation and deals with incomplete information through its fuzziness representation. Afterward, based on FLTS model, we propose a refinement model called fuzzy labeled transition refinement tree (FLTRT for short). The FLTRT structure serves as a tree of potential concurrent design trajectories of the system. Also, we introduce bisimulation relations for both models in order to identify equivalent design trajectories, which could be assessed with respect to relevant design parameters.

Open Fuzzy Synchronized Petri Net

Designing Multi agent systems needs a high-level specification model which supports abstraction, dynamicity, openness and enables fuzziness. Since the model of Synchronized Petri Nets supports dynamicity and abstraction, we extend it by fuzziness, openness and interaction with environment. The proposed model called Open Fuzzy Synchronized Petri Nets (OFSyPN for short) associates action name with transitions and enables openness feature and interaction with environment. Each action has an uncertainty degree and places are typed. The authors give an operational semantics for OFSyPN in terms of Fuzzy Labeled Transition System (FLTS for short). FLTS is a semantics model, which allows a concise action refinement representation and deals with incomplete information through its fuzziness representation. Furthermore the structure can be used to produce a tree of potential concurrent design trajectories, named fuzzy labeled transition refinement tree (FLTRT for short). We exemplify the OFSyPN model thought a case study.

Application of Fuzzy Labeled Transition System to Contract Net Protocol

For developing large dynamic systems in a rigorous manner, fuzzy labeled transition refinement tree (FLTRT for short) has been defined. This model provides a formal specification framework for designing such systems. In fact, it supports abstraction and enables fuzziness which allows a rigorous formal refinement process. The purpose of this paper is to illustrate the applicability of FLTRT for designing multi agent systems (MAS for short), among others collective and internal agent's behaviors. Therefore, Contract Net Protocol (CNP for short) is chosen as case study.

Hierarchical Design Method for Multi-Agent Systems

This paper proposes a new hierarchical design method for the specification and the verification of multi agent systems (MAS). For this purpose, the authors propose the model of Refinable Recursive Petri Nets (RRPN) under a maximality semantics. In this model, a notion of undefined transitions is considered. The underlying semantics model is the Abstract Maximality-based Labeled Transition System (AMLTS). Hence, the model supports a definition of a hierarchical design methodology. The example of goods transportation is used for illustrating the approach. For the system assessment, the properties are expressed in CTL logic and verified using the verification environment FOCOVE (Formal Concurrency Verification Environment).