Hybrid DF and SIR Forwarding Strategy in Conventional and Distributed Alamouti Space-Time Coded Cooperative Networks

In this paper,we propose a hybrid decode-and-forward and soft information relaying(HDFSIR)strategy to mitigate error propagation in coded cooperative communications.In the HDFSIR approach,the relay operates in decode-and-forward(DF)mode when it successfully decodes the received message;otherwise,it switches to soft information relaying(SIR)mode.The benefits of the DF and SIR forwarding strategies are combined to achieve better performance than deploying the DF or SIR strategy alone.Closed-form expressions for the outage probability and symbol error rate(SER)are derived for coded cooperative communication with HDFSIR and energy-harvesting relays.Additionally,we introduce a novel normalized log-likelihood-ratio based soft estimation symbol(NL-SES)mapping technique,which enhances soft symbol accuracy for higher-order modulation,and propose a model characterizing the relationship between the estimated complex soft symbol and the actual high-order modulated symbol.Further-more,the hybrid DF-SIR strategy is extended to a distributed Alamouti space-time-coded cooperative network.To evaluate the~performance of the proposed HDFSIR strategy,we implement extensive Monte Carlo simulations under varying channel conditions.Results demonstrate significant improvements with the hybrid technique outperforming individual DF and SIR strategies in both conventional and distributed Alamouti space-time coded cooperative networks.Moreover,at a SER of 10^(-3),the proposed NL-SES mapping demonstrated a 3.5 dB performance gain over the conventional averaging one,highlighting its superior accuracy in estimating soft symbols for quadrature phase-shift keying modulation.

Nonlinear symbolic LFT model for UAV

A nonlinear modeling framework is presented for an oceanographic unmanned aerial vehicle （UAV） by using symbolic modeling and linear fractional transformation （LFT） techniques . Consequently, an exact nonlinear symbolic LFT model of the UAV is derived in a standard M-A form where M represents the nominal, known, part of the system and A contains the time-varying, uncertain and nonlinear components. The advantages of the proposed modeling approach are that： it not only provides an ideal starting point to obtain various final design-oriented models through subse- quent assumptions and simplifications, but also it facilitates the control system analysis with models of different levels of fidelity/complexity. Furthermore, a linearized symbolic LFT model of the UAV is proposed based on the LFT differentiation, which is amenable directly to a sophisticated linear ro- bust control strategy such as μ synthesis/analysis. Both of the derived LFT models are validated with the original nonlinear model in time domain. Simulation results show the effectiveness of the pro- posed algorithm.

Symbolic Model Checking and Analysis for E-Commerce Protocol

A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiation and fairness using SME. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker.

Bounded Model Checking of CTL＊

Bounded Model Checking has been recently introduced as an efficient verification method for reactive systems. This technique reduces model checking of linear temporal logic to propositional satisfiability. In this paper we first present how quantified Boolean decision procedures can replace BDDs. We introduce a bounded model checking procedure for temporal logic CTL＊ which reduces model checking to the satisfiability of quantified Boolean formulas. Our new technique avoids the space blow up of BDDs, and extends the concept of bounded model checking.