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.

Monte Carlo Method for the Uncertainty Evaluation of Spatial Straightness Error Based on New Generation Geometrical Product Specification

Straightness error is an important parameter in measuring high-precision shafts. New generation geometrical product speeifieation（GPS） requires the measurement uncertainty characterizing the reliability of the results should be given together when the measurement result is given. Nowadays most researches on straightness focus on error calculation and only several research projects evaluate the measurement uncertainty based on ＂The Guide to the Expression of Uncertainty in Measurement（GUM）＂. In order to compute spatial straightness error（SSE） accurately and rapidly and overcome the limitations of GUM, a quasi particle swarm optimization（QPSO） is proposed to solve the minimum zone SSE and Monte Carlo Method（MCM） is developed to estimate the measurement uncertainty. The mathematical model of minimum zone SSE is formulated. In QPSO quasi-random sequences are applied to the generation of the initial position and velocity of particles and their velocities are modified by the constriction factor approach. The flow of measurement uncertainty evaluation based on MCM is proposed, where the heart is repeatedly sampling from the probability density function（PDF） for every input quantity and evaluating the model in each case. The minimum zone SSE of a shaft measured on a Coordinate Measuring Machine（CMM） is calculated by QPSO and the measurement uncertainty is evaluated by MCM on the basis of analyzing the uncertainty contributors. The results show that the uncertainty directly influences the product judgment result. Therefore it is scientific and reasonable to consider the influence of the uncertainty in judging whether the parts are accepted or rejected, especially for those located in the uncertainty zone. The proposed method is especially suitable when the PDF of the measurand cannot adequately be approximated by a Gaussian distribution or a scaled and shifted t-distribution and the measurement model is non-linear.

New Refinement Relations of Z Specifications for Multiple Viewpoints Oriented Requirements Method

In this paper we develop several new refinement relations of Z for multiple viewpoints oriented requirements method (MVORM). The original motivation is that we found the standard Z refinement relation is not adequate or correct when considering specifications that have temporal relationships of operations. The concept of temporal state variables is introduced into Z. Then new implementation relations are defined and new refinement relations are deduced, mainly for temporal state variables to process temporal relationships of operations. We use state transition systems to abstract the temporal state transitions. A simple example is used to show the procedures of MVORM. Finally some directions of further work are forwarded.

An Integration of UML Sequence Diagram with Formal Specification Methods—A Formal Solution Based on Z

UML Diagrams are considered as a main component in requirement engineering process and these become an industry standard in many organizations. UML diagrams are useful to show an interaction, behavior and structure of the system. Similarly, in requirement engineering, formal specification methods are also being used in crucial systems where precise information is required. It is necessary to integrate System Models with such formal methods to overcome the requirements errors i.e. contradiction, ambiguities, vagueness, incompleteness and mixed values of abstraction. Our objective is to integrate the Formal Specification Language (Z) with UML Sequence diagram, as sequence diagram is an interaction diagram which shows the interaction and proper sequence of components (Methods, procedures etc.) of the system. In this paper, we focus on components of UML Sequence diagram and then implement these components in formal specification language Z. And the results of this research papers are complete integrated components of Sequence diagram with Z schemas, which are verified by using tools and model based testing technique of Formal Specifications. Results can be more improved by integrating remaining components of Sequence and other UML diagrams into Formal Specification Language.

为SOFL Specification自动生成消息序列(MSC)

形式化方法以其精确的描述能力,可验证性,和自动化潜力而得到了人们的关注。特别是在一些对安全性要求非常高的领域,已经有了很多成功的案例。但他始终没有在业界得到推广。原因之一就是基于数学符号的形式化语法十分晦涩难懂,这给开发人员之间,开发人员和客户之间的交流造成了巨大的障碍。我们认为要解决这一问题,就需要为形式化规范提供更直观,更为大家所熟悉的行为表现方式。文章介绍如何自动生成MSC(messagesequencechart)来描述SOFL(StructuredObjectorientedFormalLanguage)[12]specification的行为。通过用MSC来动态模拟规范的行为的执行过程,可以很好地帮助人们理解规范内容,这对于规范校验(specificationvalidation)有重要的意义。此外,我们为支持这一MSC自动生成过程编写的一款工具原形,也会在文中作简要介绍。

Formalization of the Abstract Architecture of MAS Based on FIPA Specification

The FIPA specification of MAS (multi agent system)is accepted by most of the applications of MAS in the world, and has been used in many projects. This paper draws an Abstract architecture from the FIPA based MAS, and gives formalization about it.

THE Z SPECIFICATION DEPENDENCE GRAPH

The lack of existing solutions makes it really hard to understand formal specification languages since the application domain for representations is useful for the purpose of carrying out certain software engineering operations such as slicing and the computation of program metrics.A Z specification dependence graph is presented in this letter. It draws on the strengths of a range of earlier works and adapts them, if necessary, to the Z language.

A FORMAL SPECIFICATION LANGUAGE FOR DYNAMIC STRAND SPACE MODEL

Specification language is used to provide enough information for the model of the cryptographic protocol. This paper first extends strand space model to dynamic strand model, and then a formal specification language for this model is defined by using BNF grammar. Compared with those in literatures, it is simpler because of only concerning the algebraic properties of cryptographic protocols.

The specification and analysis of network embedded system

This paper proposes a formal method which is used to model and analyze network devices such as touters. It is based on an algebraic process called “ACSR-VP”, which enhances the original CCS algebraic process by incorporating the notions of time, resource requirements, dynamic prioritization, and synchronization. Therefore, although there are many formal methods to analyze the timed concurrency system, ACSR-VP, due to its prominent features, is best fit for analysis of a resource bounded real-time system. This paper extends ACSR-VP to EACSR-VP, which is more adaptive to the features of network devices and specializes in analyzing this kind of embedded system. EACSR-VP adds the notion of n-way communication which allows more than two processes to participate in synchronization. It also enhances value-passing capabilities which make for more flexible specifications. Finally, specifications, verification and analysis methods with EACSR-VP are introduced by a case study of router with multiple input queues.

A Conflicts Detection Approach for Merging Formal Specification Views

Specifying software requirements is an important, complicated and error prone task. It involves the collaboration of several people specifying requirements that are gathered through several stakeholders. During this process, developers working in parallel introduce and make modifications to requirements until reaching a specification that satisfies the stakeholders’ requirements. Merge conflicts are inevitable when integrating the modifications made by different developers to a shared specification. Thus, detecting and resolving these conflicts is critical to ensure a consistent resulting specification. A conflicts detection approach for merging Object-Oriented formal specifications is proposed in this paper. Conflicts are classified, formally defined and detected based on the results of a proposed differencing algorithm. The proposed approach has been empirically evaluated, and the experimental results are discussed in this paper.

Gas Chromatographic Method for Identification and Quantification of Commonly Used Residual Solvents in Pharmaceuticals Products

Background: Impurities are not expected in the final pharmaceutical products. All impurities should be regulated in both drug substances and drug products in accordance with pharmacopeias and ICH guidelines. Three different types of impurities are generally available in the pharmaceutical’s product specification: organic impurities, inorganic impurities, and residual solvents. Residual solvents are organic volatile chemicals used or generated during the manufacturing of drug substances or drug products. Purpose: The aim of this study is to develop a cost-effective gas chromatographic method for the identification and quantification of some commonly used solvents—methanol, acetone, isopropyl alcohol (IPA), methylene chloride, ethyl acetate, tetrahydrofuran (THF), benzene, toluene, and pyridine—in pharmaceutical product manufacturing. This method will be able to identify and quantify the multiple solvents within a single gas chromatographic procedure. Method: A gas chromatography (GC) equipped with a headspace sampler and a flame ionization detector, and a column DB 624, 30-meter-long × 0.32-millimeter internal diameter, 1,8 μm-thick, Brand-Agilent was used to develop this method. The initial GC oven temperature was 40°C and held for 5 minutes. It was then increase to 80˚C at a rate of 2˚C per minute, followed by a further increase to 225˚C at a rate of 30˚C per minute, with a final hold at 225˚C for 10 minutes. Nitrogen was used as a carrier gas at a flow rate of 1.20 mL per minute. Dimethyl sulfoxide (DMSO) was selected as sample solvent. Results: The developed method is precise and specific. The percent RSD for the areas of six replicate injections of this gas chromatographic method was within 10.0 and the recovery result found within 80.0% to 120.0%.

Two-Stream Approximation to the Radiative Transfer Equation:A New Improvement and Comparative Accuracy with Existing Methods

Mathematical modeling of the interaction between solar radiation and the Earth's atmosphere is formalized by the radiative transfer equation(RTE), whose resolution calls for two-stream approximations among other methods. This paper proposes a new two-stream approximation of the RTE with the development of the phase function and the intensity into a third-order series of Legendre polynomials. This new approach, which adds one more term in the expression of the intensity and the phase function, allows in the conditions of a plane parallel atmosphere a new mathematical formulation of γparameters. It is then compared to the Eddington, Hemispheric Constant, Quadrature, Combined Delta Function and Modified Eddington, and second-order approximation methods with reference to the Discrete Ordinate(Disort) method(δ –128 streams), considered as the most precise. This work also determines the conversion function of the proposed New Method using the fundamental definition of two-stream approximation(F-TSA) developed in a previous work. Notably,New Method has generally better precision compared to the second-order approximation and Hemispheric Constant methods. Compared to the Quadrature and Eddington methods, New Method shows very good precision for wide domains of the zenith angle μ 0, but tends to deviate from the Disort method with the zenith angle, especially for high values of optical thickness. In spite of this divergence in reflectance for high values of optical thickness, very strong correlation with the Disort method(R ≈ 1) was obtained for most cases of optical thickness in this study. An analysis of the Legendre polynomial series for simple functions shows that the high precision is due to the fact that the approximated functions ameliorate the accuracy when the order of approximation increases, although it has been proven that there is a limit order depending on the function from which the precision is lost. This observation indicates that increasing the order of approximation of the phase function of the RTE leads to a better precision in flux calculations. However, this approach may be limited to a certain order that has not been studied in this paper.

Systematic Method for Constructing Lewis Representations

The systematic method for constructing Lewis representations is a method for representing chemical bonds between atoms in a molecule. It uses symbols to represent the valence electrons of the atoms involved in the bond. Using a number of rules in a defined order, it is often better suited to complicated cases than the Lewis representation of atoms. This method allows us to determine the formal charge and oxidation number of each atom in the edifice more efficiently than other methods.

The Quality Specifications of Mischmetal Wire and Rod and the Method of Adding Rare Earth in Steel

The quality of mischmetal wire and rod and the method of adding rare earth into steel are quite important for making high quality steel. This paper proposes a quality specification of wire and rod as well as related adding method. The paper also provides principles for selecting raw material and adding method.

金融能力、正规信贷约束与农户创业行为

基于金融能力和正规信贷约束视角,利用2017年和2019年CHFS微观数据,通过构建Probit模型实证分析金融能力对农户创业行为的影响,探讨正规信贷约束在金融能力和农户创业行为关系中发挥的中介效应。结果表明:金融能力对农户创业行为具有显著正向影响,且在考虑内生性的情况下,该结论仍然成立;中介机制检验表明,金融能力能够通过缓解正规信贷约束来促进农户创业行为;异质性分析表明,中、西部地区和三线及以下城市的农户金融能力对其创业行为的影响更为显著。据此,建议建立完善的金融能力培养体系,加大对欠发达地区的政策扶持,且提高正规信贷支持力度。

城市间房价分化的影响因素研究

面对一二三线城市房价增速的分化走势,“因城施策”逐渐成为主基调,为此需要准确识别不同城市房价分化的主要因素。本文综合使用XGBoost等机器学习方法以及SHAP值解释性方法,基于2009—2019年全国70个大中城市面板数据,测算并分析一二三线城市房价分化的主要因素。结果表明:(1)预期因素在多轮房价分化期间都起到重要驱动作用;(2)货币政策本身并不是房价分化的主要因素,但可以通过影响预期导致房价分化;(3)需求因素和供给因素本身也不是房价分化的主要因素,但也可以通过影响预期导致房价分化。有鉴于此,“因城施策”的关键在于稳定公众对房价的预期:一线城市应在控制土地成本的前提下适当增加住房供给,削弱由于供不应求所带来的房价上涨预期;二三线城市需进一步完善基础设施,提高教育、医疗和环境质量,改善居民购房需求,防范人口外流带来的房价下跌预期。

复杂性理论视角下员工安全生产违规的前因组态研究

为揭示员工安全生产违规(EWSV)与其前因条件之间的复杂因果关系,提升安全治理效能,首先,基于复杂性理论,构建一个整合当代威慑理论、保护动机理论和社会学习理论的综合模型,从领导、同事和员工3个视角识别出影响EWSV的6种前因条件;然后,使用模糊集定性比较分析法(fsQCA)揭示什么样的前因条件组态会导致高EWSV。研究结果表明:单一条件并不构成高EWSV的必要条件,但是,领导安全惩罚缺失(SLPO)和同事安全生产违规(CWSV)在产生高EWSV上发挥较普适的作用;5种条件组态构成的3类驱动模式均可导致高EWSV。3种条件组态导致非高EWSV,降低CWSV和提高员工感知正式惩罚对促成非高EWSV至关重要;多种前因条件的不同组合方式均可导致高EWSV,高EWSV与其多种前因条件之间存在并发性、等效性和非对称性的复杂因果关系。

基于性能的通航桥梁抗船撞评估方法及应用研究

为合理有效地开展通航桥梁抗船撞性能评估,提出基于性能的桥梁抗船撞标准化评估方法。基于现行《公路桥梁抗撞设计规范》(JTG/T 3360-02-2020),从抗撞性能等级确定、设防代表船型确定、船撞力计算、船撞效应计算以及抗撞性能验算等方面,采用结构性能目标作为评估准则,建立桥梁抗撞性能评估各环节流程的标准化评估方法。以江苏扬中三桥为应用实例,运用该方法进行该桥20号墩抗撞性能评估,结果表明:20号墩桩基顺桥向抗弯性能不满足JX1级要求,其余验算结果满足要求,桥墩抗撞性能综合评估结果为不满足要求。参照评估结果该桥加装了浮动式防撞设施。桥梁抗撞性能评估标准化,可准确高效实现桥梁抗撞性能等级确定、船撞效应计算、抗撞性能验算等预期的评估功能要求。

良性前列腺增生患者临床参数间的相关性分析及方法学评价

目的探讨良性前列腺增生患者的前列腺体积、患者年龄、血清总前列腺特异性抗原(TPSA)、血清游离前列腺特异性抗原(FPSA)、前列腺特异性抗原密度(PSAD)的相互关系,同时通过患者年龄预测前列腺体积(PV)大小的准确性。研究胶乳免疫比浊法检测血清TPSA、FPSA水平与电化学发光法比较的可行性和实用性。方法收集172例患者的临床资料进行统计学分析,总结患者年龄、前列腺体积、TPSA、FPSA及PSAD的相关性,并使用受试者特征ROC曲线分析血清TPSA、FPSA预测前列腺体积的准确性。用两种方法同时检测血清TPSA和FPSA,比较其相关性、偏差和阴阳性符合率。结果患者TPSA,FPSA,PV随年龄增高而增大(r=0.318、0.325、0.511,P均<0.01),TPSA和FPSA也随PV增大而增高(r=0.279、0.368,P均<0.01)。与TPSA相比,FPSA与患者年龄、PV的相关性更强。TPSA水平<4ng/mL时,对于前列腺体积30~49mL、50~79mL和>80mL 3组,TPSA预测的AUC为0.621、0.708、0.913,最佳临界值分0.7、1.98、2.37ng/mL;FPSA预测的AUC为0.682、0.711、0.832,最佳临界值为0.37、0.56、0.81ng/mL。电化学发光法与胶乳免疫比浊法检测TPSA、FPSA相关性良好(r=0.986、0.975,P均<0.01);两种方法检测TPSA结果和FPSA结果的一致性良好;二者的阳性符合率、阴性符合率和总符合率分别为98.63%和90.54%、93.94%和96.94%、96.51%和94.18%,Kappa值为0.930、0.850(P均<0.01)。其精密度,线性范围和参考区间验证均符合标准。结论患者年龄、前列腺体积、TPSA水平、FPSA水平之间有显著的相关关系。血清TPSA和FPSA作为临床上独立预测PV的简便可行的因子具有较高准确性,其中FPSA预测的准确性更高。胶乳免疫比浊法与电化学发光法比较一致性较好,胶乳免疫比浊法可以作为检测TPSA和FPSA水平的推荐方法。

双峰法测量^(125)I溶液的比活度

采用双峰法对^(125)I溶液的比活度进行了测量,该文章简述了^(125)I放射性核素的衰变特点、双峰法测量^(125)I核素的基本原理、测量装置的组成、测量样品的制备以及测量条件的确定过程,最终给出了^(125)I溶液比活度的测量结果,并对其不确定度进行了评定。