Computation Tree Logic Model Checking of Multi-Agent Systems Based on Fuzzy Epistemic Interpreted Systems

Model checking is an automated formal verification method to verify whether epistemic multi-agent systems adhere to property specifications.Although there is an extensive literature on qualitative properties such as safety and liveness,there is still a lack of quantitative and uncertain property verifications for these systems.In uncertain environments,agents must make judicious decisions based on subjective epistemic.To verify epistemic and measurable properties in multi-agent systems,this paper extends fuzzy computation tree logic by introducing epistemic modalities and proposing a new Fuzzy Computation Tree Logic of Knowledge(FCTLK).We represent fuzzy multi-agent systems as distributed knowledge bases with fuzzy epistemic interpreted systems.In addition,we provide a transformation algorithm from fuzzy epistemic interpreted systems to fuzzy Kripke structures,as well as transformation rules from FCTLK formulas to Fuzzy Computation Tree Logic(FCTL)formulas.Accordingly,we transform the FCTLK model checking problem into the FCTL model checking.This enables the verification of FCTLK formulas by using the fuzzy model checking algorithm of FCTL without additional computational overheads.Finally,we present correctness proofs and complexity analyses of the proposed algorithms.Additionally,we further illustrate the practical application of our approach through an example of a train control system.

Model Checking Workflow Net Based on Petri Net

The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic （CTL） allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic ＊ （CTL ＊ ） can be used to character the relaxed soundness of the workflow.

Model Checking Electronic CommerceSecurity Protocols Based on CTL

We present a model based on Computational Temporal Logic (CTL) methods forverifying security requirements of electronic commerce, protocols. The model describes formally theauthentication, confidentiality integrity, non-repudiation) denial of serviee and access control ofthe e-lectronic commerce protocols. We illustrate as case study a variant of the Lu-Smolka protocolproposed by Lu-Smolka Moreover, we have discovered two attacks that allow a dishonest user topurchase a good debiting the amountto another user. And also, we compared our work with relativeresearch works and found lhat the formal way of this paper is more general to specify securityprotocols for E-Commerce.

Modeling and Analysis of Data Dependencies in Business Process for Data-Intensive Services

With the growing popularity of data-intensive services on the Internet, the traditional process-centric model for business process meets challenges due to the lack of abilities to describe data semantics and dependencies, resulting in the inflexibility of the design and implement for the processes. This paper proposes a novel data-aware business process model which is able to describe both explicit control flow and implicit data flow. Data model with dependencies which are formulated by Linear-time Temporal Logic(LTL) is presented, and their satisfiability is validated by an automaton-based model checking algorithm. Data dependencies are fully considered in modeling phase, which helps to improve the efficiency and reliability of programming during developing phase. Finally, a prototype system based on j BPM for data-aware workflow is designed using such model, and has been deployed to Beijing Kingfore heating management system to validate the flexibility, efficacy and convenience of our approach for massive coding and large-scale system management in reality.

Automatic Verification of Biochemical Network Using Model Checking Method

This study focuses on automatic searching and verifying methods for the teachability, transition logics and hierarchical structure in all possible paths of biological processes using model checking. The automatic search and verification for alternative paths within complex and large networks in biological process can provide a considerable amount of solutions, which is difficult to handle manually. Model checking is an automatic method for verifying if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic, such as computational tree logic （CTL）. This article represents that model checking is feasible in biochemical network verification and it shows certain advantages over simulation for querying and searching of special behavioral properties in biochemical processes.

Aspect-Oriented Design Method for Embedded Systems Based on Timed Statecharts

The formal modelling and verification method has become an effective way of improving the reliability and correctness of complex,safety-critical embedded systems.Statecharts are widely used to formally model embedded applications,but they do not realise the reasonable separation of system concerns,which would result in code scattering and tangling.Aspect-Oriented Software Development(AOSD)technology could separate crosscutting concerns from core concerns and identify potential problems in the early phase of the software development life cycle.Therefore,the paper proposes aspect-oriented timed statecharts(extended timed statecharts with AOSD)to separately model base functional requirements and other requirements(e.g.,scheduling,error handling),thereby improving the modularity and development efficiency of embedded systems.Furthermore,the dynamic behaviours of embedded systems are simulated and analysed to determine whether the model satisfies certain properties(e.g.,liveness,safety)described by computation tree logic formulae.Finally,a given case demonstrates some desired properties processed with respect to the aspect-oriented timed statecharts model.

Fair Preorder for Partial Fair Kripke Structures

This paper discussed how to handle the fairness conditions in partial Kripke structures. The partial Kripke structures were used for partial state spaces model checking, which is a new technique to solve problems of state explosion. This paper extended the partial Kripke structure with fairness conditions by defining a partial fair Kripke structure, and a 3 valued fair CTL(Computation Tree Logic) semantics correspondingly. It defines a fair preorder between partial Kripke structures that preserves fairness and is akin to fair bisimulation. In addition, a pertinent theorem is also given, which indicates the relationship between the partial state spaces and the more complete one by illustrating the characterizations of states in the partial fair structure in terms of CTL formulae.

Nondeterministic Probabilistic Petri Net -- A New Method to Study Qualitative and Quantitative Behaviors of System

There are many variants of Petri net at present, and some of them can be used to model system with both function and performance specification, such as stochastic Petri net, generalized stochastic Petri net and probabilistic Petri net. In this paper, we utilize extended Petri net to address the issue of modeling and verifying system with probability and nondeterminism besides function aspects. Using probabilistic Petri net as reference, we propose a new mixed model NPPN （Nondeterministic Probabilistic Petri Net） system, which can model and verify systems with qualitative and quantitative behaviours. Then we develop a kind of process algebra for NPPN system to interpret its algebraic semantics, and an action- based PCTL （Probabilistic Computation Tree Logic） to interpret its logical semantics. Afterwards we present the rules for compositional operation of NPPN system based on NPPN system process algebra, and the model checking algorithm based on the action-based PCTL. In order to put the NPPN system into practice, we develop a friendly and visual tool for modeling, analyzing, simulating, and verifying NPPN system using action-based PCTL. The usefulness and effectiveness of the NPPN system are illustrated by modeling and model checking an elaborate model of travel arrangements workflow.

Computational Mechanisms for Metaphor in Languages： A Survey

Metaphor computation has attracted more and more attention because metaphor, to some extent, is the focus of mind and language mechanism. However, it encounters problems not only due to the rich expressive power of natural language but also due to cognitive nature of human being. Therefore machine-understanding of metaphor is now becoming a bottle-neck in natural language processing and machine translation. This paper first suggests how a metaphor is understood and then presents a survey of current computational approaches, in terms of their linguistic historical roots, underlying foundations, methods and techniques currently used, advantages, limitations, and future trends. A comparison between metaphors in English and Chinese languages is also introduced because compared with development in English language Chinese metaphor computation is just at its starting stage. So a separate summarization of current progress made in Chinese metaphor computation is presented. As a conclusion, a few suggestions are proposed for further research on metaphor computation especially on Chinese metaphor computation.

Recent progress of fiber-based transistors: materials, structures and applications

Wearable electronics on fibers or fabrics assembled with electronic functions provide a platform for sensors,displays,circuitry,and computation.These new conceptual devices are human-friendly and programmable,which makes them indis-pensable for modern electronics.Their unique properties such as being adaptable in daily life,as well as being lightweight and flexible,have enabled many promising applications in robotics,healthcare,and the Internet of Things(IoT).Transistors,one of the fundamental blocks in electronic systems,allow for signal processing and computing.Therefore,study leading to integration of transistors with fabrics has become intensive.Here,several aspects of fiber-based transistors are addressed,including materials,system structures,and their functional devices such as sensory,logical circuitry,memory devices as well as neuromorphic computation.Recently reported advances in development and challenges to realizing fully integrated electronic textile(e-textile)systems are also discussed.

Intracellular Logic Computation with Framework Nucleic Acid-Based Circuits for mRNA Imaging

Main observation and conclusion DNA circuits have been designed for implementation of various functions based on DNA strand displacement in cell-free settings,but their capabilities in biological environments remain limited.In this work,we report framework nucleic acid(FNA)-based circuits enabling intracellular logic computation for mRNA imaging.FNAs as rigid scaffolds enable to deliver our built DNA circuits into cells without aid of transfection reagents,evading a time-consuming and tedious process prior to analysis,and the pendant duplex DNA designed at one vertex of FNA as gate is suitable for four-way strand exchange,minimizing crosstalk with other nucleic acids in the cellular milieu.We demonstrated that such FNA-based circuits can operate both in vitro and in vivo logic computation,including OR and AND logic gates.Moreover,in situ mRNA imaging was also realized by exploiting native mRNA as scaffolds to bind multiple FNA-based gates for the enhanced signal-to-background ratio.We hope that this FNA-based circuit can be applied for disease diagnosis,facilitating the development of biomedicine.

On the Toggling-Branching Recurrence of Computability Logic

We introduce a new, substantially simplified version of the toggling-branching recurrence operation of com- putability logic, prove its equivalence to Japaridze＇s old, ＂canonical＂ version, and also prove that both versions preserve the static property of their arguments.