Search

The learning and teaching power of the students in different courses can be different according to their intelligence and talent. A student may be smart in one course while being lazy in other courses. In order to increase the efficiency of a class, regardless of the class teacher, it is better to teach each course by the smartest student in that course. Inspired by this fact, we present a new meta-heuristic optimization algorithm called Participation of Smart Students (PSS) in increasing the class efficiency. To analyze the effectiveness of the PSS algorithm, we run it on 10 general test functions and 29 test functions from the 2017 IEEE Congress on Evolutionary Computation (CEC 2017). The results of PSS algorithm are compared with the effectiveness of Teaching and Learning-based Optimization (TLBO) Algorithm, Black Widow Optimization (BWO), Political Optimization (PO), Barnacle Mating Optimizer (BMO), Chimpanzee Optimization Algorithm (CHOA), Aquila Optimizer (AO) and City Council Evolution (CCE). Multiple comparison of the results obtained by the Friedman rank test shows that the PSS algorithm has a higher efficiency than the TLBO, BWO, PO, BMO, CHOA, and AO algorithms and almost similar efficiency as the CCE algorithm in terms of finding the closest solution to the optimal one and the hit rate. Moreover, the PSS algorithm has a higher convergence speed than all other algorithms.

The ability to assess the reliability of safety-critical systems is one of the most crucial requirements in the design of modern safety-critical systems where even a minor failure can result in loss of life or irreparable damage to the environment. Model checking is an automatic technique that verifies or refutes system properties by exploring all reachable states (state space) of a model. In large and complex systems, it is probable that the state space explosion problem occurs. In exploring the state space of systems modeled by graph transformations, the rule applied on the current state specifies the rule that can perform on the next state. In other words, the allowed rule on the current state depends only on the applied rule on the previous state, not the ones on earlier states. This fact motivates us to use a Markov chain (MC) to capture this type of dependencies and applies the Estimation of Distribution Algorithm (EDA) to improve the quality of the MC. EDA is an evolutionary algorithm directing the search for the optimal solution by learning and sampling probabilistic models through the best individuals of a population at each generation. To show the effectiveness of the proposed approach, we implement it in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results confirm that the proposed approach has a high speed and accuracy in comparison with the existing meta-heuristic and evolutionary techniques in safety analysis of systems specified formally through graph transformations.

Safety is one of the most important features of modern software systems, especially safety-critical systems such as nuclear power plants, which can be checked exactly by model checking. Model checking is a formal verification technique that analyzes system properties through exploring all reachable states (state space) of a model of a system. The problem of the technique is that it confronts the state space explosion in large and complex systems due to exponential memory usage. Recent researches show that a partial and intelligent exploration of the state space can be a suitable solution to overcome this problem. In this paper, we propose a two-phase model checking for safety analysis of systems specified formally through graph transformations. In the first phase, the beam-search algorithm explores the state space to a specific number of states. In case of failure of the phase, the second phase starts: in systems specified through graph transformations, the rule applied on the previous state can determine the rule that can perform on the next state. In other words, the rule on current state depends on only the rule applied to previous state, not the one on earlier states. Hence, a Markov chain (MC) is estimated to capture dependencies between the sequence of applied rules in the state space explored by the beam-search algorithm. The MC is then employed to explore the remainder of the state space intelligently. To evaluate the effectiveness of the two-phase model checking, we implement it in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results show that the two-phase model checking has the high speed and accuracy in comparison with the existing meta-heuristic and evolutionary techniques.

Model checking is one of the successful techniques in automated verification of software and hardware systems. However, employing this technique for verification of properties such as the safety and liveness requires that all possible states of a system are generated and then the given property is checked. In large and complex systems, generating all states causes the state space explosion problem. Hence, it is possible to refute such properties by searching the state space to find a state in which the given property is violated. Of course, it is possible that detecting such states in complex systems leads to the exhaustive exploration of the state space. Recent researches confirm that using meta-heuristic and evolutionary approaches to intelligently explore a portion of the state space can be a promising idea. Hence, in this paper, we propose an approach based on ant colony optimization algorithm for refuting the safety and liveness properties and also analyzing reachability ones in systems specified formally through graph transformation system. Refutation of liveness and analyzing reachability properties in systems modeled by graph transformations are the prominent advantages of this approach in comparison with the previous approaches. The proposed approach is implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. Experimental results show that our proposed approach is faster and it generates shorter counterexamples in comparison with others.

While developing concurrent systems, one of the important properties to be checked is deadlock freedom. Model checking is an accurate technique to detect errors, such as deadlocks. However, the problem of model checking in complex software systems is state space explosion in which all reachable states cannot be generated due to exponential memory usage. When a state space is too large to be explored exhaustively, using meta-heuristic and evolutionary approaches seems a proper solution to address this problem. Recently, a few methods using genetic algorithm, particle swarm optimization and similar approaches have been proposed to handle this problem. Even though the results of recent approaches are promising, the accuracy and convergence speed may still be a problem. In this paper, a novel method is proposed using Bayesian Optimization Algorithm (BOA) to detect deadlocks in systems specified formally through graph transformations. BOA is an Estimation of Distribution Algorithm in which a Bayesian network (as a probabilistic model) is learned from the population and then sampled to generate new solutions. Three different structures are considered for the Bayesian network to investigate deadlocks in the benchmark problems. To evaluate the efficiency of the proposed approach, it is implemented in GROOVE, an open source toolset for designing and model checking graph transformation systems. Experimental results show that the proposed approach is faster and more accurate than existing algorithms in discovering deadlock states in the most of case studies with large state spaces.

Software architectural style is one of the best concepts to define a family of related architectures and their common properties. Despite the essential role of software architectures in the software engineering practice, the lack of formal description and analysis may hamper the quality of designed models. Hence, using proper formal languages seems necessary for architectural style description. In this case, it is possible to use model checking to verify the designed models automatically. However, the model checking of complex software systems suffers from the state space explosion problem. To handle this problem, data mining techniques may contribute to obtain the required knowledge for intelligent model checking i.e. searching only a portion of the state space. In this paper, to check the model of complex software systems which are designed according to an architectural style, an efficient approach is proposed using data mining techniques. These software systems must be specified through architectural styles and modeled by Graph Transformation Systems (GTS) formally. In the proposed approach, to check a large model based on a specific style intelligently, a specific knowledge is required. Such knowledge is acquired from mining the data of checking a smaller model consistent with the same style. These smaller models can be designed either by the designers or can be automatically generated consistent with the style. The proposed solution can be used to verify the reachability property and to refute the safety and liveness properties. This solution is implemented in GROOVE, a toolset for designing and model checking of graph transformation systems. The experimental results show that our method is faster and more accurate in comparison with the existing techniques in model checking of complex software systems.

The aim of AI planning is to solve the problems with no exact solution available. These problems usually have a big search space, and planning may not find plans with the least actions and in the shortest time. Recent researches show that using suitable heuristics can help to find desired plans. In planning problems specified formally through graph transformation system (GTS), there are dependencies between applied rules (actions) in the search space. This fact motivates us to solve the planning problem for a small goal (instead of the main goal), extract dependencies from the searched space, and use these dependencies to solve the planning problem for the main goal. In GTS based systems, the nodes of a state (really is a graph) can be grouped due to their type. To create a small (refined) goal, we use a refinement technique to remove the predefined percent of nodes from each group of the main goal. Bayesian Optimization Algorithm (BOA) is then used to solve the planning problem for the refined goal. BOA is an Estimation of Distribution Algorithm (EDA) in which Bayesian networks are used to evolve the solution populations. Actually, a Bayesian network is learned from the current population, and then this network is employed to generate the next population. Since the last Bayesian network learned in BOA has the knowledge about dependencies between applied rules, this network can be used to solve the planning problem for the main goal. Experimental results on four well-known planning domains confirm that the proposed approach finds plans with the least actions and in the lower time compared with the state-of-the-art approaches.

Assessing the reliability of safety-critical systems is an important and challenging task because even a minor failure in these systems may result in catastrophic consequences, like losing human life. A well-known and fully automatic technique in reliability assessing approaches is model checking. However, applying this technique to verify some properties such as safety may lead to the state space explosion problem in which all reachable states cannot be checked due to computational limitations. In such situations that the verification of a safety property is infeasible, it is possible to refute the safety property by searching a reachable state in which a special configuration (e.g., an error or an undesirable behaviour) occurs. Therefore, checking reachability can be done instead of refuting the corresponding safety property. Finding such reachable states, in the worst case, may cause the state space explosion problem again. Hence, using evolutionary algorithms to explore the state space efficiently can be a promising idea. In this paper, at first, we propose an evolutionary algorithm to check reachability properties and refute safety ones in software systems specified formally through graph transformations. Since the accuracy and convergence speed of the proposed approach can still be improved, we employ the Bayesian Optimization Algorithm (BOA) to propose another approach. In BOA, a Bayesian network is learnt from the population and then sampled to generate new solutions. The proposed approaches can be used to analyse the reachability and safety properties. The proposed approaches are implemented in GROOVE which is an open source toolset for designing and model checking graph transformation systems. To evaluate the efficiency of the proposed approaches, different benchmark problems are employed. Experimental results show that the proposed approaches are faster and more accurate than the existing methods.

An optimal algorithm is presented about Conflict-Free Coloring for connected subgraphs of tree of rings. Suppose the number of the rings in the tree is |T| and the maximum length of rings is |R|. A presented algorithm in [1] for a Tree of rings used O(log|T|.log|R|) colors but this algorithm uses O(log|T|+log|R|) colors. The coloring earned by this algorithm has the unique-min property, that is, the unique color is also minimum.

An optimal algorithm is presented about Conflict-Free Coloring for connected subgraphs of chain of rings. Suppose the length of the chain is |C| and the maximum length of rings is |R|. A presented algorithm in [1] for a Chain of rings used O(log|C|.log|R|) colors but this algorithm uses O(log|C|+log|R|) colors. The coloring earned by this algorithm has the unique-min property, that is, the unique color is also minimum.