This paper introduces the past temporal operators into computation tree logic(CTL), and obtains a new specification language CTLP which is more expressive than CTL. CTLP model checking algorithm is proposed and its time complexity is the same as CTL. The fixpoint representation of CTLP is presented which makes CTLP model checking symbolic. The symbolic algorithm can overcome the state explosion problem efficiently in model checking.
Path test is an important white-box test method, which can detect more program errors than others. Basis path set contains so many program paths that it will cover all the statements and branches in a program. It gains the better result by testing all the paths in a basis set under the limited test resource. This paper proposes an automatic generation of basis path set method based on depth-first searching. In order to avoid the condition that the algorithm never stops and reduces the searching procedure, and to improve its efficiency, the generation of sub-path method is adopted.
This paper presents the research on Chinese ellipsis recovering based on concept model. It focuses on how to determine on the possible semantic ellipsis through the mapping from semantic level to syntax level which is based on the present semantic model. An ellipsis recovering model is proposed which is applied to the domain natural language understanding. Simulation results show the advantages of the proposed approach in Chinese formal ellipsis recovering.
A novel audio-visual feature-based framework for porn video segment detection is presented, which extracts and analyses audio and video features independently, and combines their results to give out a final detection result. A support vector machine (SVM) is used to learn and then classify the audio sections, and skin info is used to give out a visual analysis result. Experiment results indicate that this approach has a high recognition rate, so it can be adopted to surveillance for video streams and segmentation of particular content in videos.