The matfun toolkit of the scientific computing software Matlab contains more than 40 commonly used matrix computing related functions, which have important applications in artificial intelligence, big data and other fields. This paper makes use of the modeling, simulation and verification language MSVL to imitate all basic functions in the matfun function library, and gives several representative function algorithms and implementation details. Finally we use these functions to design and implement a practical application.
In many decision-making problems, a rational reward function is required, which can correctly guide agents to make ideal operations. For example, an intelligent robot needs to check its power before sweeping. This kind of reward functions involves historical states, rather than a single current state. It is referred to as non-Markovian reward. However, state-of-the-art MDP (Markov Decision Process) planners only support Markovian reward. In this paper, we present an approach to transform non-Markovian reward expressed in LTL f (Linear Temporal Logic over Finite Traces) into Markovian reward. LTL f is converted into an automaton which is compiled to standard MDP model. Then the reward function of the model is further optimized through reward shaping in order to speed up planning. The reshaped reward function can be exploited by MDP planners to guide search and produce good training results. Finally, experiments with augmented International Probabilistic Planning Competition (IPPC) domain demonstrates the effectiveness and feasibility of our approach, especially the reshaped reward function can significantly improve the performance of planners.
Runtime exceptions are difficult to be detected by static analysis tools and their occurrences in runtime often cause software systems to crash or unexcepted termination. Therefore, it is necessary to detect the existence of runtime exceptions in the program before it is executed. In this paper, we describe a novel program segment testing technique for detecting potential occurrences of runtime exceptions during the program construction process. Our testing technique is characterized by three steps. The first step is to determine the target program segment in which potential runtime exceptions may occur during the program execution. The second step is to form an appropriate environment to test the program segment by determining the values of the variables. The final step is to carry out the testing and determine whether the runtime exceptions will occur and will be handled properly during the system execution. This paper also presents a case study to demonstrate that the technique is effective.
Propositional Projection Temporal Logic (PPTL) has been widely used in formal verification, and its expressiveness is suitable for the description of security requirements. However, the expression and application of temporal logic formulas rely on a strong mathematical background, which is difficult for non-domain experts, thus bridging the chasm between natural language descriptions and formal languages is urgently needed. This paper proposes an innovative architecture for neural machine automatic translation named NL2PPTL, which transforms natural language into PPTL specification via utilizing data preprocessing, encoder-decoder network and stack sequentially. To evaluate the performance of our method, the experimental verification is realized on real datasets. The experiment conducted shows that our method has effectiveness on temporal logic specification generation.
Documents on popular libraries such as pyOpenSSL do not specify parameters’ domains precisely. Inexact domains hinder efficiently generating valid test cases. In order to solve this problem, an approach for inferring exact domains, namely IED, is put forward. IED starts from crawling parameters’ data types from online official documents. Then, IED conducts exception testing to find tight domains based on slack domains of data types. Finally, IED attempts to detect the extensibility of tight bounds and outputs exact domains. Based on IED, experiments have been conducted on 29 basic parameters of application programming interfaces of pyOpenSSL. Experimental results show that the inferred exact domains vary dramatically even for the same data type and reduce the original domains of data types significantly. Thus, IED is effective and helpful in efficiently generating valid test cases.
