Hierarchical Controller Synthesis Under Linear Temporal Logic Specifications Using Dynamic Quantization

Linear temporal logic(LTL)is an intuitive and expressive language to specify complex control tasks,and how to design an efficient control strategy for LTL specification is still a challenge.In this paper,we implement the dynamic quantization technique to propose a novel hierarchical control strategy for nonlinear control systems under LTL specifications.Based on the regions of interest involved in the LTL formula,an accepting path is derived first to provide a high-level solution for the controller synthesis problem.Second,we develop a dynamic quantization based approach to verify the realization of the accepting path.The realization verification results in the necessity of the controller design and a sequence of quantization regions for the controller design.Third,the techniques of dynamic quantization and abstraction-based control are combined together to establish the local-to-global control strategy.Both abstraction construction and controller design are local and dynamic,thereby resulting in the potential reduction of the computational complexity.Since each quantization region can be considered locally and individually,the proposed hierarchical mechanism is more efficient and can solve much larger problems than many existing methods.Finally,the proposed control strategy is illustrated via two examples from the path planning and tracking problems of mobile robots.

Translating Linear Temporal Logic Formula s into Automata

To combat the well-known state-space explosion problem in Prop ositional Linear T emp o- ral Logic （PLTL） model checking, a novel algo- rithm capable of translating PLTL formulas into Nondeterministic Automata （NA） in an efficient way is proposed. The algorithm firstly transforms PLTL formulas into their non-free forms, then it further translates the non-free formulas into their Normal Forms （NFs）, next constructs Normal Form Graphs （NFGs） for NF formulas, and it fi- nally transforms NFGs into the NA which ac- cepts both finite words and int-mite words. The experimental data show that the new algorithm re- duces the average number of nodes of target NA for a benchmark formula set and selected formulas in the literature, respectively. These results indi- cate that the PLTL model checking technique em- ploying the new algorithm generates a smaller state space in verification of concurrent systems.

Fuzzy Logic Deadzone Compensation with Feedback Linearization of Nonlinear Systems

A fuzzy logic compensator is designed for feedback linearizable nonlinear systems with deadzone nonlinearity. The classification property of fuzzy logic systems makes them a natural candidate for the rejection of errors induced by the deadzone, which has regions in which it behaves differently. A tuning algorithm is given for the fuzzy logic parameters, so that the deadzone compensation scheme becomes adaptive, guaranteeing small tracking errors and bounded parameter estimates. Formal nonlinear stability proofs are given to show that the tracking error is small. The fuzzy logic deadzone compensator is simulated on a one-link robot system to show its efficacy.

Hierarchical Coordinated Control for Power System Voltage Using Linear Temporal Logic

The paper proposed an approach to study the power system voltage coordinated control using Linear Temporal Logic (LTL). First, the hybrid Automata model for power system voltage control was given, and a hierarchical coordinated voltage control framework was described in detail. In the hierarchical control structure, the high layer is the coordinated layer for global voltage control, and the low layer is the power system controlled. Then, the paper introduced the LTL language, its specification formula and basic method for control. In the high layer, global voltage coordinated control specification was defined by LTL specification formula. In order to implement system voltage coordinated control, the LTL specification formula was transformed into hybrid Automata model by the proposed algorithms. The hybrid Automata in high layer could coordinate the different distributed voltage controller, and have constituted a closed loop global voltage control system satisfied the LTL specification formula. Finally, a simple example of power system voltage control include the OLTC controller, the switched capacitor controller and the under-voltage shedding load controller was given for simulating analysis and verification by the proposed approach for power system coordinated voltage control. The results of simulation showed that the proposed method in the paper is feasible.

Identification of Question and Non-Question Segments in Arabic Monologues Using Prosodic Features: Novel Type-2 Fuzzy Logic and Sensitivity-Based Linear Learning Approaches

In this paper, we extend our previous study of addressing the important problem of automatically identifying question and non-question segments in Arabic monologues using prosodic features. We propose here two novel classification approaches to this problem: one based on the use of the powerful type-2 fuzzy logic systems (type-2 FLS) and the other on the use of the discriminative sensitivity-based linear learning method (SBLLM). The use of prosodic features has been used in a plethora of practical applications, including speech-related applications, such as speaker and word recognition, emotion and accent identification, topic and sentence segmentation, and text-to-speech applications. In this paper, we continue to specifically focus on the Arabic language, as other languages have received a lot of attention in this regard. Moreover, we aim to improve the performance of our previously-used techniques, of which the support vector machine (SVM) method was the best performing, by applying the two above-mentioned powerful classification approaches. The recorded continuous speech is first segmented into sentences using both energy and time duration parameters. The prosodic features are then extracted from each sentence and fed into each of the two proposed classifiers so as to classify each sentence as a Question or a Non-Question sentence. Our extensive simulation work, based on a moderately-sized database, showed the two proposed classifiers outperform SVM in all of the experiments carried out, with the type-2 FLS classifier consistently exhibiting the best performance, because of its ability to handle all forms of uncertainties.

The Media Logic and Cultural Impact of WeChat

Through its media logic, which is defined by programmability, pervasiveness, connectivity, and datafication, WeChat establishes a non-linear, interactive, and user-dominated media environment. This media logic enhances the influence of each user within WeChat’s narrative landscape and revolutionises traditional media narration methods by enabling them to generate and distribute content. In such an environment, users are able to edit, receive, and send information without constraints of time or distance, which enables delayed interactions that broaden the potential for human communication and dissemination. Additionally, WeChat partially replaces social behaviours and institutions, thereby modifying their original structures and characteristics. As individuals become more accustomed to this media environment, they progressively adjust to the forms that are appropriate for media representation on WeChat, thereby completing the mediatization of culture and society. In this process, individuals are becoming more dependent on media and media logic, with WeChat’s influence permeating social and cultural activities through its media logic. This interaction has a substantial impact on society and culture, thereby aiding in their reconstruction.

Transient Stability Improvement of Power System Using Non-Linear Controllers

This paper presents the design of a non-linear controller to prevent an electric power system losing synchronism after a large sudden fault and to achieve good post fault voltage level. By Direct Feedback Linearization (DFL) technique robust non-linear excitation controller is designed which will achieve stability enhancement and voltage regulation of power system. By utilizing this technique, there is a possibility of selecting various control loops for a particular application problem. This method plays an important role in control system and power system engineering problem where all relevant variables cannot be directly measured. Simulated results carried out on a single machine infinite bus power system model which shows the enhancement of transient stability regardless of the fault and changes in network parameters.

Load Frequency Control of Small Hydropower Plants Using One-Input Fuzzy PI Controller with Linear and Non-Linear Plant Model

This study presents an intelligent approach for load frequency control (LFC) of small hydropower plants (SHPs). The approach which is based on fuzzy logic (FL), takes into account the non-linearity of SHPs—something which is not possible using traditional controllers. Most intelligent methods use two- input fuzzy controllers, but because such controllers are expensive, there is economic interest in the relatively cheaper single-input controllers. A non- linear control model based on one-input fuzzy logic PI (FLPI) controller was developed and applied to control the non-linear SHP. Using MATLAB/Si- mulink SimScape, the SHP was simulated with linear and non-linear plant models. The performance of the FLPI controller was investigated and compared with that of the conventional PI/PID controller. Results show that the settling time for the FLPI controller is about 8 times shorter;while the overshoot is about 15 times smaller compared to the conventional PI/PID controller. Therefore, the FLPI controller performs better than the conventional PI/PID controller not only in meeting the LFC control objective but also in ensuring increased dynamic stability of SHPs.

Spectral Characteristics of the Best Affine Approach of Multi-Output m-Valued Logical Functions

This paper discusses the best affine approach （BAA） of multi-output m-valued logical functions. First, it gives the spectra of rate of accordance between multi-output m-valued logical functions and their affine functions, then analyzes the BAA of multi-output m-valued logical functions and finally gives the spectral characteristics of BAA of multi-output m-valued logical functions.

SPECTRAL ANALYSIS OF SOME INDEPENDENCES OF MULTIPLE-VALUED LOGICAL FUNCTIONS ON THEIR VARIABLES

There are many kinds of special relationships between multiple-valued logical func-tions and their variables, and they are difficult to be judged from their expressions. In thispaper, some sufficient and necessary conditions of the independence and statistical independenceof multiple-valued logical functions on their variables are given. Some conditions of algebraicindependence of multiple-valued logical functions on some of their variables and the way to de-generate a function to the greatest extent are proposed, and some applications of these resultsare indicated. All the results are studied by using Chrestenson spectral techniques.

一种基于Petri网的多机器人路径规划建模方法

月球基地建设是当前各国月球探测与开发计划的核心使能技术之一。然而,为消除高昂的运输成本和有限载人航天技术的约束,使用多机器人团队建造月球基地的新研究方案被提出,该方案的关键是如何实现多机器人针对复杂任务的路径规划。为此,以月球基地建设场景中的探测采集区域、采集月壤、搬运月壤等作为复杂的任务输入,研究了一种基于Petri网模型的多机器人路径规划建模方法。构建了多机器人运动的Petri网模型;使用线性时序逻辑(linear temporal logic,LTL)语言描述月球基地建设的相关任务;将Petri网模型和LTL公式结合求解得到多机器人路径;在Matlab软件中进行仿真验证,并与使用切换系统的建模方法进行对比。结果表明,使用Petri网模型所需的建模总时间比切换系统模型单个任务的建模时间减少2个数量级,说明建立的Petri网多机器人模型具有避免维度爆炸、计算高效等优势。

改进变值逻辑与线性预测在心音分类中的应用

心音对于评价心脏健康状况具有重要作用.文章介绍了一种新的基于变值逻辑与线性预测倒谱系数融合特征的先心病分类算法,有助于提取心音中的深度病理特征.算法首先对心音进行降噪、包络提取;然后进行变值逻辑运算、标记并转换为可分析的测度数据,并计算信号的线性预测倒谱系数进行特征融合;最后使用随机森林,XGBOOST和LIGHTGBM机器学习分类器进行先心病二分类.研究所用心音样本共4000例,测试结果对正常和异常心音分类的平均准确率为0.9138.算法无需对心音进行心动周期分割,大大简化了分析流程,可望用于先心病的筛查.

基于多目标线性规划的本体冲突消除方法

针对本体逻辑冲突消除传统方法未充分利用本体逻辑性质的缺陷,引入Shapley值法刻画本体逻辑性质,构建基于多目标0-1整数线性规划的本体冲突消除方法,使用分层序列法求解多目标线性规划模型。其解遵循理性放弃原则,避免传统方法中目标权重的平均性或随机性。实验结果表明,采用该方法能够令解集遵循理性放弃原则的前提下,利用本体逻辑性质有效减少解集数量,从而提高决策效率。

基于电网多源数据的电力知识图谱构建方法

电力知识图谱构建方法重复采集电网多源数据,针对构建得到的知识图谱置信度过小的问题,设计一种基于电网多源数据的电力知识图谱构建方法。通过设定实体电网多源数据采集架构,采用局部线性嵌入算法筛选重复采集的电网多源数据。将电力知识间的关系转变可识别特征数值,抽取多源数据中的电力知识划分图谱层级,构建电力知识图谱结构。结合电力知识采集环境完成实验,实验结果表明,文中设计的构建方法准确率为97%,召回率为0.78%,F值为93,满足电力知识图谱的构建需求。

自动泊车系统规划与控制方法研究

为了对泊车过程中的车辆进行跟踪控制,基于车辆动力学模型,研究设计了一种线性二次型控制器,使用B-spline曲线规划了一条曲率连续的泊车路径,针对控制器设计过程中权重系数选择困难,引入模糊逻辑算法对控制器进行优化处理,节省了人工成本,然而模糊逻辑算法的计算是实时的,且不同速度下车辆状态不同,因此将基于Frobenius范数的更新策略加入程序计算中以降低计算量,利用MATLAB/Carsim联合仿真验证了改进后控制系统的运算时间降为0.2 ms,实时性提升92%,适应度提升30%.

基于自适应高阶滑模的转向控制器设计

针对车辆转向下的操作稳定性和侧倾稳定性不足等问题,研究前轮主动转向的非线性滑膜控制,对汽车行驶稳定性研究有一定的指导意义。采用自适应高阶滑模控制方法结合T-S模糊建模方法,考虑轮胎侧偏角非线性变化,构建模型参数观测器实时获取轮胎动态参数。通过CarSim和MATLAB/Simulink联合仿真,选取双移线和正弦停滞两种典型工况对质心侧偏角、横摆角速度、侧向加速度等性能指标的自适应高阶滑模控制方法进行仿真验证。结果表明,该方法能够改善线控转向系统对转角的动态响应性能;与传统滑模控制策略相比,该策略的横摆角速度和侧向加速度最大值分别降低了22.63%和5.4%,能够提高车辆的操纵稳定性。

时态描述逻辑ALC-LTL的Tableau判定算法

时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-LTL中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。

基于线性时序逻辑理论的仓储机器人路径规划

首先根据仓储物流环境的特点构建了可灵活扩展的仓储环境模型，并制定了适合仓储物流需求的机器人运动规则，使该模型能够适用于动态的仓储物流环境；其次采用线性时序逻辑任务公式描述具体的任务需求，使其可以适用于实际应用中更加复杂的任务；继而将任务需求与环境信息相融合，构建任务可行网络拓扑，避免分段任务搜索；然后采用Dijkstra算法在任务可行网络拓扑上搜索出最优路径，确保规划所得路径的最优性；最后将任务可行网络拓扑上的最优路径映射回加权切换系统，获得环境中满足任务需求的最优路径。与目前广泛使用的A＊算法相比，上述方法不仅能够满足复杂的任务需求，而且能够保证路径规划的最优性，而不是次优解。

基于时态逻辑技术的高压输电线系统故障诊断

提出了将线性时态逻辑(LTL)技术和电网故障模拟量信息引入高压输电线系统故障诊断的新思想。建立了LTL形式化演绎的完整语法、语义解释体系。在变电站端,综合考虑系统容错需求及故障诊断的实时性要求,对故障模拟量进行了实时预处理；在调度中心,分析了故障诊断过程中保护、开关动作的时序关系,形成典型故障模式下的开关量事件序列(TDS)及其相应的模拟量状态序列(TAS),并通过LTL表示TDS和TAS中的时序约束条件。最后通过实例验证了推理的可靠性和容错性。

面向移动应用软件信息泄露的模型检测研究

移动平台上的应用软件私密信息泄露漏洞关注违背用户意愿的接口或数据暴露,而泄露形式和内容的复杂性增添了该类漏洞的检测难度.现有方法主要利用传统的静态数据流分析及动态监控等技术,易发生漏报和误报,且无法处理隐式信息泄露问题.该文首次将基于线性时序逻辑(Linear Temporal Logic,LTL)的模型检测技术应用于移动软件信息泄露检测上,提出了一种基于安全要素语句插装的泄露检测方法.文章首先针对代码中的安全要素提出一种信息泄露抽象关系模型;其次设计驱动生成规则和插装算法,在目标应用上生成可规约系统;继而设计具有通用意义的LTL泄露检测属性并利用符号执行技术优化检测算法;最后构建支持移动平台的模拟方法库,开发了原型检测系统(Leakage Finder of Android,LFDroid).公开数据集实验及对比分析表明,该文方法可以为含有隐式信息泄露数据集提供更为精确的漏洞检测,相较于传统方法准确率和召回率均具有明显优势,除此之外亦发现了3个真实移动应用的5个隐式泄露漏洞威胁.