Abstract This study addresses the problem of scheduling machining operations in a highly automated manufacturing environment while considering the work styles of workers. In actual manufacturing, many aspects of the operation must be considered, such as constraints related to the works to be machined in the machining schedule and the states of the workers. To derive good solutions for such a large-scale problem with many constraints within a realistic amount of computation time, we develop an optimization technique based on a mixed-integer programming (MIP)-based large neighborhood local search method for the machining scheduling problem. Then, computer experiments on a problem based on actual machining requirements are performed to verify the validity of the proposed method.

The autonomous vehicle control system is a typical kind of hybrid system that combines both continuous and discrete behavior.Formal specification and verification techniques help us to verify desired properties of given systems.In this study, we propose a way to describe a formal specification of an autonomous vehicle control system in CafeOBJ algebraic specification language.The control system is a hybrid system with continuous variables of time, velocity, and position controlled by discrete pedal actions including acceleration, braking, and no-operation.We also verify the safety property of the autonomous vehicle control system by a theorem proving technique called the proof score method *

The Lim-Jeong-Park-Lee protocol (LJPL protocol) has been proposed as an efficient distributed mutual exclusion algorithm for intersection traffic control.The LJPL protocol has been specified and verified formally using the Maude model checker.Because of the limitation of computation, the existing model checking approach restricts the number of vehicles participating the protocol.In this paper, we model the LJPL protocol as an observational transition system, describe its specification in CafeOBJ, the algebraic specification language, and verify its safety property using the proof score method, where mutual exclusiveness can be proved for an arbitrary number of vehicles * .

Hybrid systems combine both continuous and discrete behaviors.Formal descriptions of hybrid systems may help us to verify desired properties of a given system formally with computer supports.In this paper, we propose a way to describe a formal specification of a given multitask hybrid system as an observational transition system in CafeOBJ algebraic specification language and verify it by the proof score method based on equational reasoning implemented in CafeOBJ interpreter.

Hybrid systems combine both continuous and discrete behaviors, which occur frequently in safety-critical applications in various domains including Internet-of-Things (IoT) and Cyber-Physical Systems (CPS) applications such as health care, transportation, and robotics. For safe and reliable information society with IoT and CPS technologies, it is important to establish a way to specify and verify hybrid systems formally. Formal descriptions of hybrid systems may help us to verify desired properties of a given system formally with computer supports. We propose a way to describe a formal specification of a given multitask hybrid system as an observational transition system (OTS) in CafeOBJ algebraic specification language. OTSs are models where systems behaviors are described through observations. CafeOBJ supports specification execution based on a rewrite theory. We verify that OTS/CafeOBJ specifications of hybrid systems satisfy desired property by the proof score method based on equational reasoning implemented in CafeOBJ interpreter. In this paper, we specify a signal control system with an arbitrary number of vehicles by our proposed method, and verify the system satisfies a safety property by the proof score method.

This paper proposes MIP (Mixed-Integer Programming)-based power distribution optimization method for decentralized energy network with electric vehicles (EVs). Decentralized energy network is a new grid systems toward independence from existing power grid, and renewable energy is main energy source for the decentralized energy network. EVs are expected to take an important role of future mobility and energy network. Because the latest EV usually include large battery for long cruising distance, now EVs can be regarded as “moving battery.” Proposed method utilizes both battery in house and EV's battery to minimize total purchased energy and wasted energy. This method brings an opportunity to charge the surplus energy at house to EV's battery, and the total purchased energy may be reduced. Experimental results demonstrated the interconnection between the energy network with rich connectivity and EV reduced the purchased energy by more than half.

A proposed approach is specialized for large scale vehicle routing problems(VRPs) and based on area segmentation and gradual area integration mechanisms so as to avoid combinatorial explosion. The purpose of the proposed approach is to deconstruct large scale problem into small size sub-problems and gradually restore these to original state. Firstly, an original large scale problem is divided into some small sub-areas and optimal solutions in each sub-area are derived. When a best incumbent solution remains unchanged for a certain period, subareas are gradually integrated and new optimal solutions in a new integrated sub-area are newly searched through use of the obtained solutions in previous sub area. This gradual integration and optimization are iterated until every sub-area are integrated into the one (the original problem), and the optimal solution of original problem can be obtained at this time. The proposed approach aims to deconstruct large scale problem into small size sub-problems and perform more efficient search. Through some typical test problems, it was demonstrated that our approach could derive better results more effectively than conventional approach.

Complex-valued Hopfield network is used to model the dynamics of a network of limit cycle oscillators, each of which emerges via Hopf bifurcation, to investigate the dependency of the network dynamics on a bifurcation parameter. As an application, a network of two complex-valued neurons is used as a central pattern generator model for a biped locomotion. A bifurcation parameter is a constant input from higher motor centers. Numerical calculations show the system successfully expresses some characteristic behaviors, which were obtained by more complicated Fitzhugh-Nagumo oscillator model, and which were found in clinical data of disordered interlimb coordination caused by Parkinson's disease. The observed results of symmetric anti -phase synchronization, asymmetric synchronization, and breakdown of the synchronization can be explained by the existence condition of the energy function of the complex-valued neural network, and by the synchronization condition of a coupled system of phase oscillators.

The phase synchronization in the complex-valued Hopfield network has been shown to be effective for a signal control in an area-wide urban traffic flow control. The basic idea of the original method is to attain the global effectiveness as a weighted summation of the local effectiveness. And the complex-valued Hopfield network is designed to converge to such an optimal state through the appropriate interaction between the neurons which model the traffic signals. As the result, the network possesses the energy function which expresses the global effectiveness, whose leading term is given by the summation of the substantial traffic flows under the given offset. Thus, it is a bottom-up approach to optimize the global effectiveness as the total of the local effectiveness. In this paper, two different approaches are introduced, and added to or compared with the above approach. The first approach is the feedback from the real time information of local traffics. The purpose of the feedback is to decrease the differences of the disadvantages among conflicting flows, which are measured by a congestion or the number of waiting vehicles. The addition of the feedback to the original method shows that the local feedback works as a pinpoint control on a local congestion, while keeping the total effectiveness especially in regular traffic patterns. The second is a top-down approach to attain the global optimization by real-coded genetic algorithms. The proposed GA directly searches the effective offset using a traffic simulator to calculate the average traveling time for the evaluation. Therefore, genetic operations are designed for a small size population and a real-code in a torus space. The best offsets obtained by GA reduce the average traveling time by 2%~7% compared with the results obtained by the original approach.

This paper presents two new approaches for transforming a single-objective problem into a multi-objective problem. These approaches add new objectives to a problem to make it multi-objective and use a multi-objective optimization approach to solve the newly defined problem. The first approach is based on relaxation of the constraints of the problem and the other is based on the addition of noise to the objective value or decision variable. Intuitively, these approaches provide more freedom to explore and a reduced likelihood of becoming trapped in local optima. We investigated the characteristics and effectiveness of the proposed approaches by comparing the performance on single-objective problems and multi-objective versions of those same problems. Through numerical examples, we showed that the multi-objective versions produced by relaxing constraints can provide good results and that using the addition of noise can obtain better solutions when the function is multimodal and separable.

This paper presents two new approaches for transforming a single-objective problem into a multi-objective problem. The first approach is based on relaxation of the constraints of the problem and the other is based on the addition of noise to the objective value or decision variable. Intuitively, these approaches provide more freedom to explore and a reduced likelihood of becoming trapped in local optima.Through numerical examples, we showed that the multi-objective versions produced by relaxing constraints can provide good results and that using the addition of noise can obtain better solutions when the function is multimodal and separable.

Dynamics of 2 types of complex-valued neural network is numerically analyzed. In [Kuroe, Y, et al., 2003], some mathematical properties of a mutually connected Hopfield-type network of nonrotating complex-valued neurons were shown, and the sufficient conditions of the existence of an energy function are derived for 2 types (types A and B) of the activation function of the neuron. In this paper, we consider the Hopfield network of rotating complex-valued neurons. The network dynamics is decomposed into the dynamics of the amplitude and phase of each neuron. For type B network, the dynamics of the phases is shown to be the dynamics of a coupled system of rotating phase oscillators with a pair-wise sinusoidal phase-difference interaction [Nishikawa, I and Kuroe, Y, 2004]. Therefore a phase synchronization, which is well known in a phase oscillator system [Kuramoto, Y, 1984], is expected also in type B network. At the same time in this type B network, the network dynamics of homogeneously rotating neurons can be transformed into the network dynamics of non-rotating neurons, for which the existence condition of an energy function is derived explicitly. On the other hand for type A network, there is no such correspondence to a phase oscillator system, nor equivalence to the network whose convergence is assured by the existence of an energy function. One recent result on a phase oscillator system is the effectiveness for an area-wide signal control of an urban traffic network. Therefore in this paper, the dynamics of type A and B complex-valued rotating neural networks is numerically investigated, especially from the point of view of the effective control of the signal offset. The similarity and the difference between the 2 types of dynamics are shown through computer simulations using a microscopic traffic simulator on several traffic flow patterns and conditions.

Complex-valued Hopfield networks which possess the energy function are analyzed. The dynamics of the network with certain forms of an activation function is de-composable into the dynamics of the amplitude and phase of each neuron. Then the phase dynamics is described as a coupled system of phase oscillators with a pair-wise sinusoidal interaction. Therefore its phase synchronization mechanism is useful for the area-wide offset control of the traffic signals. The computer simulations show the effectiveness under the various traffic conditions.