Renewable energy power has advantages such as sustainability and cleanliness, which helps to save energy and reduce emissions, improve energy utilization efficiency, and protect the environment. Nevertheless, it exerts significant pressure on power grids when large scale renewable energy power integrates into power grid straightforwardly, such as the safe and stable operation and economic efficiency of the power grid system. To resolve the above power grid challenges, we propose a renewable energy power transmission system which overlays Electric Vehicles (EV), for the sparse deployment of renewable energy power stations, combing the Vehicle-to-Grid technology. We formulate the Social optimization EV User Selection (SEUS) problem and show that the SEUS problem is NP-hard. We design the incentive mechanism based on Deep Reinforcement Learning and greedy approach. By means of rigorous theoretical analysis and empirical simulations, we have established that our proposed incentive mechanism can ensure individual rationality and truthfulness, and significantly surpass the benchmark algorithms.

Drone-assisted Wireless Rechargeable Sensor Networks (WRSNs) have been widely adopted in various urban applications due to their sustainability and scalability. In drone-assisted WRSN systems, incentive mechanisms are essential to motivate potential drone users to provide sustainable energy replenishment services. This paper presents a system model for drone-assisted WRSN scenarios, formulating the problem as a Social Optimization Drone User Selection (SODUS) problem. We design an incentive mechanism combining Deep Reinforcement Learning (DRL) with greedy optimization. By means of thorough theoretical analysis and extensive simulations, we can show that our proposed mechanism not only attains individual rationality and truthfulness, but also remarkably surpasses the benchmarks in performance.

Wireless Power Transmission (WPT) has been widely used to replenish energy for various rechargeable devices. The ElectroMagnetic Radiation (EMR) of WPT has attracted great attention of safety concerns. It is possible for the malicious attacker to launch the EMR attack by capturing multiple wireless chargers. Little work has studied the EMR attack itself. In this paper, we propose a realistic EMR hazard model, which outputs the diminishing marginal hazard with EMR, with adjustable parameters to the target entities. We formulate three EMR attack models, termed Cumulative EMR Attack (CEA), Overall EMR Attack (OEA) and Unsafety EMR Attack (UEA), and propose the performance guaranteed algorithm of EMR attack for each model. We conduct extensive simulations and field experiments on a testbed. The results show that the proposed algorithms can output the near-optimal solution with much less running time than the optimal algorithms. The results of field experiments in a small testbed show that the utilities of CEAA and OEAA are increased by 70.5% and 12.9% than the comparison algorithms, respectively. Moreover, the number of captured chargers of UEAA is 5.9% less than the comparison algorithms. Our simulations also show the designed algorithms can perform better in a large-scale charging network.

Public transportation system is one of the most effective ways to conserve energy and reduce carbon emissions. However, the traditional public transportation system does not provide customized service and cannot guarantee the arrival time to destination. To address these issues, we formulate the minimum shared bus scheduling problem to minimize the number of shared buses such that all orders can be completed under constraints of deadlines and capacity of shared bus. We propose the approximation algorithms, S-MBSA for the shared bus with strong endurance and E-MBSA for the large-scale order scenario, to solve the minimum shared bus scheduling problem. We further formulate the constrained maximum revenue shared bus scheduling problem to maximize the revenue under the limited number of shared buses, and propose an approximation algorithm, CMRBSA, to find the shared bus route schedules. Through the extensive simulations, we demonstrate the significant superiority of S-MBSA and E-MBSA in terms of number of shared buses. Furthermore, CMRBSA outperforms the benchmark algorithms significantly in terms of revenue.

Operating system in intelligent transportation systems (ITSs) is a complex software system whose correctness and security are not obvious. There are advances in formal description and verification of operating systems in ITSs recently and they mainly focus on bottom-up proofs in which the source codes satisfy certain expected properties expressed by logic formulae. In this paper, we propose a layered object model for operating systems in ITSs. This model includes functionality layer, refinement layer and concrete layer. We consider the operating system object model as a logic system ( $L)$ with variables representing the objects of $L$ , and a series of logic formulae for security and functional configurations in security of ITSs. We establish a mathematical structure as a domain of discourse for operating system in ITSs and accordingly, construct a mapping from operating system objects to the domain. In this way, we propose a formal method to verify the operating system security properties and configurations in ITSs. We use the virtual memory management part of our self-designed operating system VSOS as an example to illustrate the model and show that the claimed security properties can be rigorously proven for ITSs. The evaluation and verification of VSOS indicate that the proposed model implementation is feasible and achieves the security goals.

The development of Electric Vehicle (EV) helps to ease energy crises and deduce vehicle exhaust emissions. However, it also brings a great impact on both transportation networks and power grids. There are some serious impediments in terms of energy charging to the popularization of EV, such as high deployment cost of charging stations, low charging efficiency, and voltage deviation of power grid. To address these issues, we design a new EV charging system, which levers the bus network in urban areas through the integration of OnLine Electric Vehicle (OLEV) system and Microwave Power Transfer (MPT) system. We formulate the EV route scheduling problem based on this new charging system to maximize the total residual energy subject to all EVs can arrive to their destinations before deadlines. Then, we propose an approximation algorithm, RSA, to solve the route scheduling problem. To relieve the traffic congestion, we further formulate the conflict-free EV route scheduling problem, and use the matching based algorithm, FRSA, to find the EV route schedules with the maximal residual energy. Through the extensive simulations, we demonstrate that RSA and FRSA can increase the average residual energy by 67.66% and 50.36% compared with the solution without the designed wireless charging system, respectively. Moreover, RSA reduces 22.22% of travel time and outputs 77.23% of residual energy, and FRSA can obtain 83.51% residual energy with 3.62% of extra travel time of the corresponding optimal solutions on average, respectively.

It is important to monitor the early screening of chronic diseases, predict the risk, and provide the comprehensive management of chronic diseases for the elderly. However, it is difficult to provide the robust and real-time emergency service for elderly chronic disease because of the complex social network and diversity of elderly chronic disease service. To address these issues, we design a new drone assisted robust emergency service system. We formulate the Drone assisted Management (DM) problem to minimize the total time cost of drone subject to all elderly chronic disease services which can be guaranteed exactly once by the drone under its energy constraint. Then, we propose the DRS algorithm to solve the DM problem. To provide the robust and real-time service, we further formulate the Charging driven Drone assisted Management (CDM) problem and present the CDRS algorithm to solve the CDM problem. Through the theoretical analysis and numerical simulation experiments, we demonstrate that DRS and CDRS can decrease the total time cost by 37.61% and increase the QoE by 112.80% through the designed system, respectively.

The accuracy of design and implementation of an operating system in intelligent transportation systems is difficult to describe and validate because of its complexity. In this paper, we describe an OS in intelligent transportation systems with automaton theory and establish an OS state model. Based on this model, we construct an isomorphic model in Isabelle/HOL, describe the work objects and operational semantics of the system, and verify the system at the assembly level. We use a micro-kernel OS prototype (VSOS) for intelligent transportation systems as an example to illustrate our method and verify the correctness of design and implementation in VSOS with Isabelle/HOL. Verification shows that the proposed method is feasible.

Wireless Rechargeable Sensor Network (WRSN) is largely used in monitoring of environment and traffic, video surveillance and medical care, etc., and helps to improve the quality of urban life. However, it is challenging to provide the sustainable energy for sensors deployed in buildings, soil or other places, where it is hard to harvest the energy from environment. To address this issue, we design a new wireless charging system, which levers the bus network assisted drone in urban areas. We formulate the drone scheduling problem based on this new wireless charging system to minimize the total time cost of drone subject to all sensors can be charged under the energy constraint of drone. Then, we propose an approximation algorithm DSA for the energy tightened drone scheduling problem. To make the tasks of WRSN sustainable, we further formulate the drone scheduling problem with deadlines of sensors, and present the approximation algorithm DDSA to find the drone schedule with the maximal number of sensors charged by the drone before deadlines. Through the extensive simulations, we demonstrate that DSA can reduce the total time cost by 84.83% compared with Greedy Replenished Energy algorithm, and uses at most 5.98 times of the total time cost of optimal solution on average. Then, we also demonstrate that DDSA can increase the survival rate of sensors by 51.95% compared with Deadline Greedy Replenished Energy algorithm, and can obtain 77.54% survival rate of optimal solution on average.

传统的离散数学实验教学,通常使用C、C++等程序设计语言来完成相应的课程验证性实验.学生在花费大量的时间和精力完成程序设计后,依然对程序的正确性没有直观的认识.借助Isabelle/HOL交互式定理证明器工具和形式化方法,构建离散数学实验环境,解决离散数学课程实验教学的直观表达问题以及逻辑推理实验的设置.以二叉树这种离散结构的知识点学习为例,阐述如何使用Isabelle/HOL来完成"离散数学"课程的实验教学设计.通过这种实验教学,能使学生对逻辑演算和推理有清晰的认识,同时培养学生的数学和逻辑思维以及创新、应用能力.

Smart healthcare has been applied in many fields such as disease surveillance and telemedicine, etc. However, there are some challenges for device deployment, data collection and guarantee of stainability in regional disease surveillance. First, it is difficult to deploy sensors and adjust the sensor network in unknown region for dynamic disease surveillance. Second, the limited life-cycle of sensor network may cause the loss of surveillance data. Thus, it is important to provide a sustainable and robust regional disease surveillance system. Given a set of Disease surveillance Area (DsA)s and Point of disease Surveillance (PoS)s, some sensors are deployed to monitor these PoSs, and a drone collect data from the sensors as well as charge the sensors to extend their life-cycles. The drone replenish its energy by relying on the bus network. We first formulate the drone assisted regional disease surveillance problem under the constraints of life-cycle of sensors and energy of drone, and propose an approximation algorithm to find a feasible cycle of drone to minimize the traveling time cost of drone. To satisfy the diversity requirements and dynamic scalability of regional disease surveillance, we deploy one robot in each DsA instead of sensors. We further formulate the learning transferable driven regional disease surveillance problem, and propose a joint schedule algorithm of drone and robots. The results of both theoretical analysis and extensive simulations show that the proposed algorithms can reduce the total time cost by 39.71 and 48.74 percent, average waiting time by 42.00 and 50.14 percent, and increase the average accessing ratio of PoSs by 15.53 and 22.30 percent, through the assistance of bus network and learning transferable features.

Video surveillance system is the integration of computers, networks, communications, and video CODEC, etc. Because of its distributed architecture, parallel image processing and ease of installation and expansion, it is widely used in many fields such as education, transportation and industry. However, there are some challenges of video surveillance applications in smart cities such as large scale of video events, low quality and big delay of video data transmission, and the loss of video surveillance data integrity. In order to solve the above problems, this paper designs a series of optimization algorithms and scheduling strategies based on Unmanned Aerial Vehicle (UAV) cluster. Firstly, we construct a full device coverage network with UAV cluster in heterogeneous communication environment of smart cities. Secondly, we formulate the scheduling problem of UAV cluster as bi-objective fragile bin packing problem, and design an optimal scheduling algorithm with constant approximation performance ratio. The simulation experimental results fully demonstrate the effectiveness, feasibility and robustness of the proposed solution in terms of system life cycle, video decodable frame rate, the ratio of UAV flight time to system life cycle, throughput and delay.

Clustering is an important issue in brain medical image segmentation. Original medical images used for clinical diagnosis are often insufficient for clustering in the current domain. As there are sufficient medical images in the related domains, transfer clustering can improve the clustering performance of the current domain by transferring knowledge across the related domains. In this article, we propose a novel shared hidden space transfer fuzzy c-means (FCM) clustering called SHST-FCM for cross-domain brain computed tomography (CT) image segmentation. SHST-FCM projects both the data samples of the source domain and target domain into the shared hidden space, such that the distributions of the two domains are as close as possible. In the learned shared subspace, the data samples of the source domain serve as the auxiliary knowledge to aid the clustering process in the target domain. Extensive experiments on brain CT medical image datasets indicate the effectiveness of the proposed method.

This paper develops a real-time and reliable data collection system for big scale emotional recognition systems. Based on the data sample set collected in the initialization stage and by considering the dynamic migration of emotional recognition data, we design an adaptive Kth average device clustering algorithm for migration perception. We define a sub-modulus weight function, which minimizes the sum of the weights of the subsets covered by a cover to achieve high-precision device positioning. Combining the energy of the data collection devices and the energy of the wireless emotional device, we balance the data collection efficiency and energy consumption, and define a minimum access number problem based on energy and storage space constraints. By designing an approximate algorithm to solve the approximate minimum Steiner point problem, the continuous collection of emotional recognition data and the connectivity of data acquisition devices are guaranteed under the energy constraint of wireless devices. We validate the proposed algorithms through simulation experiments using different emotional recognition systems and different data scale. Furthermore, we analyze the proposed algorithms in terms of topology for devices classification, location accuracy, and data collection efficiency by comparing with the Bayesian classifier-based expectation maximization algorithm, the background difference-based moving target detection arithmetic averaging algorithm, and the Hungarian algorithm for solving the assignment problem.

Wearable devices, wireless networks and body area networks have become an effective way to solve the problem of human health monitoring and care. However, the radiation problems of wireless devices, the power supply problems of wearable devices and the deployment of body area networks have become obstacles to their wide application in the field of health care. In order to solve the above problems, this paper studies and designs a wearable health medical body area network which is convenient for human health monitoring and medical care, starting from low-cost deployment of wireless wearable devices and active control of wireless radiation. Firstly, in order to avoid replacing equipment batteries, improve the relay and data aggregation capabilities of wireless body area network, and reduce the communication and computing load of edge devices, a deployment scheme of wireless medical health wearable devices is designed based on the optimal segmentation algorithm of Steiner spanning tree. Then, in order to minimize the charging cost and maximize the global charging utility of single source and multiple points in a finite time slot, an approximate algorithm for the optimal charging sequence based on 01 knapsack problem, i.e., the access path of wireless wearable devices, is designed. Then, an active radiation control algorithm for wearable medical health body area network is proposed, which can actively control the transmission power and radiation status of these wireless devices. Finally, simulation results show that the proposed algorithm is better than battery-powered wireless body area network and wireless rechargeable body area network, 16% and 44% reduction of devices, 25%(sic)13% reduction of energy consumption, 26% reduction of radiation, and 5.18 and 1.13 times improvement of signal quality.

We address the problem of real-time transmission of multimedia streams in distributed heterogeneous networks. The effect of this problem directly affects the execution efficiency, real-time and reliability of the network system. Firstly, for distributed multimedia data, the heterogeneity of edge cloud devices is considered. Through in-depth analysis of the dependency between multimedia packets and video frames, the edge cloud and its dependent directed acyclic graph are established, and the edge cloud computing model is set up to execute cost, real-time and dependability. Secondly, based on the deadline features of multimedia real-time applications, the optimal solution of the edge cloud sets is established. The establishment basis is from the maximum satisfiability problem and the search for the best edge cloud with the execution cost and execution time of the multimedia streaming real-time communication application. According to the above models, a real-time multimedia streaming transmission control mechanism upon edge cloud computing and the opportunistic approximation optimization is proposed. Through the simulation and analysis experiments of static network topology and dynamic network topology, the performance of the execution cost, delay and packet loss rate of the proposed mechanism is deeply analyzed and verified. The analysis results show that the proposed mechanism can transparently influence the dynamic network topology and find an optimal solution for the guarantee of real-time and reliability through the deep fusion edge cloud computing and approximate optimization.

Despite the extensive study on relay selection in mobile social networks (MSNs), few work has taken both transmission latency (i.e. efficiency) and information leakage probability (i.e. security) into consideration. Therefore we target on designing an efficient and secure relay selection algorithm to enable communication among legitimate users while reducing the information leakage probability to other users. In this paper, we propose a novel mobility model for MSN users considering both the randomness and the sociality of the movements, based on which the social relationship among users, i.e. the meeting probabilities among the users, are predicted. Taken both efficiency and security into consideration, we design a network formation game based relay selection algorithm by defining the payoff functions of the users, designing the game evolving rules, and proving the stability of the formed network structure. Extensive simulation is conducted to validate the performance of the relay selection algorithm by using both synthetic trace and real-world trace. The results show that our algorithm outperforms other algorithms by trading a balance between efficiency and security.