模态逻辑的完全性理论至今已经有了很大发展,其证明通常也是逻辑研究中重要且极其困难的一环。从简单的证明命题逻辑有效性的真值表、归谬法的思想出发到反模型的建立;从最早证明模态逻辑系统的Kripke-语义图的出现到Hughes and Gressw...模态逻辑的完全性理论至今已经有了很大发展,其证明通常也是逻辑研究中重要且极其困难的一环。从简单的证明命题逻辑有效性的真值表、归谬法的思想出发到反模型的建立;从最早证明模态逻辑系统的Kripke-语义图的出现到Hughes and Gresswell对Kripke-语义图的修正;从L.Henkin极大一致集的提出到从属模型和典范模型的建立;从典范模型的广泛使用到Bull有限模型的建立无不体现了这一点。对正规模态逻辑系统完全性证明的层层刨析,可以更好地把握和使用完全性证明方法。展开更多
A practical approach is presented to enlarge the recoverable scope and improve the precision of pattern recovery. To specify both structural aspects and behavioral aspects of design patterns, we introduce traditional ...A practical approach is presented to enlarge the recoverable scope and improve the precision of pattern recovery. To specify both structural aspects and behavioral aspects of design patterns, we introduce traditional predicate logic combined with Alien's interval-based temporal logic as our theoretical foundation. Moreover, we take the Visitor pattern as an example to illustrate how to specify design patterns to support recovery of design patterns besides structural category. The experimental results show that the approach presented is practical for recovering design information of real world systems.展开更多
In order to improve a mobile robot＇s autonomy in unknown environments, a novel intelligent controller is designed. The proposed controller is based on fuzzy logic with the aim of assisting a multi-sensor equipped mob...In order to improve a mobile robot＇s autonomy in unknown environments, a novel intelligent controller is designed. The proposed controller is based on fuzzy logic with the aim of assisting a multi-sensor equipped mobile robot to safely navigate in an indoor environment. First, the designs of two behaviors for a robot＇s autonomous navigation are described, including path tracking and obstacle avoidance, which emulate human driving behaviors and reduce the complexity of the robot＇s navigation problems in unknown environments. Secondly, the two behaviors are combined by using a finite state machine （FSM）, which ensures that the robot can safely track a predefined path in an unknown indoor environment. The inputs to this controller are the readings from the sensors. The corresponding output is the desired direction of the robot. Finally, both the simulation and experimental results verify the effectiveness of the proposed method.展开更多
Research on practical and verifiable prediction methods for the service life of bearings plays a critical role in improving the reliability and safety of aircraft engines. The concept of grade-life （GL） is introduce...Research on practical and verifiable prediction methods for the service life of bearings plays a critical role in improving the reliability and safety of aircraft engines. The concept of grade-life （GL） is introduced to de- scribe the service life of bearings. A GL prognostic model for aircraft engine bearings is proposed based on sup- port vector machine （SVM） and fuzzy logic inference. Firstly, the mathematical model is discussed to predict the physics-based GL （PGL）. Then, the diagnostic estimation model based on SVM is presented in detail to predict the empirical GL （EPL）. Thirdly, a fuzzy logic inference is adopted to fuse two GL predicted results. Finally, the GL prognostic model is verified by the run-to-failure data acquired from an accelerated life test of an aircraft bearing. The results show that the model provides a more practical and reliable prediction for the service life of bearings.展开更多
To make service matchmaking more adaptive to various service requests and diverse web services, an adaptive approach-ASMA is proposed to service matchmaking based on temporal logic model-checking. The approach is base...To make service matchmaking more adaptive to various service requests and diverse web services, an adaptive approach-ASMA is proposed to service matchmaking based on temporal logic model-checking. The approach is based on the proposed abstract service model, ASM-TL, which addresses some important constraints for identifying capabilities of web services, such as service inner constraints and invocation constraints, and also has a virtual process model for describing service behavioral properties. By treating service requests as temporal logic conditions and web services as temporal models, ASMA does service matchmaking through model checking. Therefore, ASMA makes service matchmaking more accurate and more adaptive to the variety of service requests and the diversity of web services. The approach has been applied to the problem solving environment （PSE） for bioinformatics research. Applications show that the approach is suitable for dynamic environments.展开更多
In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge...In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge is introduced into the past tense operator, and then a new temporal epistemic logic LTLKP is obtained, so that LTLKP can naturally and precisely describe the system＇s reliability. Secondly, a set of prior algorithms are designed to calculate the maximal reachable depth and the length of the longest of loop free paths in the structure based on the graph structure theory. Finally, some theorems are proposed to show how to approximate the complete threshold with the diameter and recurrence diameter. The proposed work resolves the completeness threshold problem so that the completeness of bounded model checking can be guaranteed.展开更多
A novel optoelectronic functional circuit with heterojunction phototransistors (HPTs) and resonant tunneling diodes (RTDs) is described,which presents the function of both photocurrent switching and photo-current latc...A novel optoelectronic functional circuit with heterojunction phototransistors (HPTs) and resonant tunneling diodes (RTDs) is described,which presents the function of both photocurrent switching and photo-current latching.These behaviors have been demonstrated by simulating experiments and circuit simulation.Furthermore,basing on photo-current latching behavior,various photo-controlled basis logic elements such as delayed flip-flop (DFF) can be designed and fabricated.展开更多
文摘模态逻辑的完全性理论至今已经有了很大发展,其证明通常也是逻辑研究中重要且极其困难的一环。从简单的证明命题逻辑有效性的真值表、归谬法的思想出发到反模型的建立;从最早证明模态逻辑系统的Kripke-语义图的出现到Hughes and Gresswell对Kripke-语义图的修正;从L.Henkin极大一致集的提出到从属模型和典范模型的建立;从典范模型的广泛使用到Bull有限模型的建立无不体现了这一点。对正规模态逻辑系统完全性证明的层层刨析,可以更好地把握和使用完全性证明方法。
文摘A practical approach is presented to enlarge the recoverable scope and improve the precision of pattern recovery. To specify both structural aspects and behavioral aspects of design patterns, we introduce traditional predicate logic combined with Alien's interval-based temporal logic as our theoretical foundation. Moreover, we take the Visitor pattern as an example to illustrate how to specify design patterns to support recovery of design patterns besides structural category. The experimental results show that the approach presented is practical for recovering design information of real world systems.
基金Cultivation Fund for Innovation Project of Ministry of Education (No.708045)
文摘In order to improve a mobile robot＇s autonomy in unknown environments, a novel intelligent controller is designed. The proposed controller is based on fuzzy logic with the aim of assisting a multi-sensor equipped mobile robot to safely navigate in an indoor environment. First, the designs of two behaviors for a robot＇s autonomous navigation are described, including path tracking and obstacle avoidance, which emulate human driving behaviors and reduce the complexity of the robot＇s navigation problems in unknown environments. Secondly, the two behaviors are combined by using a finite state machine （FSM）, which ensures that the robot can safely track a predefined path in an unknown indoor environment. The inputs to this controller are the readings from the sensors. The corresponding output is the desired direction of the robot. Finally, both the simulation and experimental results verify the effectiveness of the proposed method.
基金Supported by the China Postdoctoral Science Foundation(20100481500)~~
文摘Research on practical and verifiable prediction methods for the service life of bearings plays a critical role in improving the reliability and safety of aircraft engines. The concept of grade-life （GL） is introduced to de- scribe the service life of bearings. A GL prognostic model for aircraft engine bearings is proposed based on sup- port vector machine （SVM） and fuzzy logic inference. Firstly, the mathematical model is discussed to predict the physics-based GL （PGL）. Then, the diagnostic estimation model based on SVM is presented in detail to predict the empirical GL （EPL）. Thirdly, a fuzzy logic inference is adopted to fuse two GL predicted results. Finally, the GL prognostic model is verified by the run-to-failure data acquired from an accelerated life test of an aircraft bearing. The results show that the model provides a more practical and reliable prediction for the service life of bearings.
基金The National High Technology Research and Devel-opment Program of China (863Program) (No2006AA12Z202)the National Natural Science Foundation of China (No90412010)
文摘To make service matchmaking more adaptive to various service requests and diverse web services, an adaptive approach-ASMA is proposed to service matchmaking based on temporal logic model-checking. The approach is based on the proposed abstract service model, ASM-TL, which addresses some important constraints for identifying capabilities of web services, such as service inner constraints and invocation constraints, and also has a virtual process model for describing service behavioral properties. By treating service requests as temporal logic conditions and web services as temporal models, ASMA does service matchmaking through model checking. Therefore, ASMA makes service matchmaking more accurate and more adaptive to the variety of service requests and the diversity of web services. The approach has been applied to the problem solving environment （PSE） for bioinformatics research. Applications show that the approach is suitable for dynamic environments.
基金The National Natural Science Foundation of China (No.10974093)the Scientific Research Foundation for Senior Personnel of Jiangsu University (No.07JDG014)the Natural Science Foundation of Higher Education Institutions of Jiangsu Province (No.08KJD520015)
文摘In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge is introduced into the past tense operator, and then a new temporal epistemic logic LTLKP is obtained, so that LTLKP can naturally and precisely describe the system＇s reliability. Secondly, a set of prior algorithms are designed to calculate the maximal reachable depth and the length of the longest of loop free paths in the structure based on the graph structure theory. Finally, some theorems are proposed to show how to approximate the complete threshold with the diameter and recurrence diameter. The proposed work resolves the completeness threshold problem so that the completeness of bounded model checking can be guaranteed.
文摘A novel optoelectronic functional circuit with heterojunction phototransistors (HPTs) and resonant tunneling diodes (RTDs) is described,which presents the function of both photocurrent switching and photo-current latching.These behaviors have been demonstrated by simulating experiments and circuit simulation.Furthermore,basing on photo-current latching behavior,various photo-controlled basis logic elements such as delayed flip-flop (DFF) can be designed and fabricated.
