Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent syst...Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed). In this paper, we propose the use of a guasi-classical temporal logic (QCTL) for supporting the verification of temporal properties of such systems even where the consistent model is not available. Our models are paraKripke structures (extended standard Kripke structures), in which both a formula and its negation are satisfied in a same state, and properties to be verified are expressed by QCTL with paraKripke structures semantics. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.展开更多
The PRO/Ⅱ process simulation software was applied to carry out simulated calculation of the aromatics fractionation unit and the heat integrated rectification process was proposed for the aromatics fractionation sect...The PRO/Ⅱ process simulation software was applied to carry out simulated calculation of the aromatics fractionation unit and the heat integrated rectification process was proposed for the aromatics fractionation section of the 1.0 Mt/a toluene disproportionation unit at the Zhenhai Refining and Chemical Company. The optimized operating parameters were obtained through the energy utilization analysis,process simulation,heat exchanger calculations and comparisons of utility consumption. The operation of commercialized unit has revealed that the design parameters of each rectification column were consistent with the operation results,and the utility consumption was about 47% lower than the traditional heat integrated process.展开更多
基金Supported by the National Natural Science Foundation of China (No.60603036)the Jiangsu Province Research Foundation (No.BK2007139)
文摘Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed). In this paper, we propose the use of a guasi-classical temporal logic (QCTL) for supporting the verification of temporal properties of such systems even where the consistent model is not available. Our models are paraKripke structures (extended standard Kripke structures), in which both a formula and its negation are satisfied in a same state, and properties to be verified are expressed by QCTL with paraKripke structures semantics. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.
文摘The PRO/Ⅱ process simulation software was applied to carry out simulated calculation of the aromatics fractionation unit and the heat integrated rectification process was proposed for the aromatics fractionation section of the 1.0 Mt/a toluene disproportionation unit at the Zhenhai Refining and Chemical Company. The optimized operating parameters were obtained through the energy utilization analysis,process simulation,heat exchanger calculations and comparisons of utility consumption. The operation of commercialized unit has revealed that the design parameters of each rectification column were consistent with the operation results,and the utility consumption was about 47% lower than the traditional heat integrated process.
