This paper deals with a synthesis of a nonautonomous system with a stable limit cycle. We propose a synthesis method of a nonautonomous system whose transient trajectories converge to a prescribed limit cycle. We use receding horizon control to control a transient behavior of the nonautonomous system, and confirm its validity by simulation.

In this paper, we propose a synthesis method of hybrid systems with specified limit cycles. Several methods which sysnthesize a nonlinear system with prescribed limit cycles have been proposed. In these methods, the limit cycle is given by an algebraic equation, which will be called constraint equations, and its stability is guaranteed by a Lyapunov function derived from the constraint equation. In general, limit cycles of hybrid systems are nonsmooth due to the discontinuous vector fields. So the limit cycles are given by piecewise smooth constraint equations, we employ the piecewise smooth Lyapunov functions to construct desired nonsmooth limit cycles and guarantee their stability.

In real-time systems, deadline misses of the tasks cause a degradation in the quality of their results. To improve the quality, we have to allocate CPU utilization for each task adaptively. Recently, Buttazzo et al. address a feedback scheduling algorithm, which dynamically adjusts task periods based on the current workloads by applying a linear elastic task model. In their model, the utilization allocated to each task is treated as the length of a linear spring and its flexibility is described by a constant elastic coefficient. In this paper, we first consider a nonlinear elastic task model, where the elastic coefficient depends on the utilization allocated to the task. We propose a simple iterative method for calculating the desired allocated resource and derive a sufficient condition for the convergence of the method. Next, we apply the nonlinear elastic model to an adaptive fair sharing controller. Finally, we show the effectiveness of the proposed method by computer simulation.

This paper considers a motion planning method for humanoid robots. First, we review a modular state net which is a state net representing behavior of a part of the humanoid robots. Each whole body motion of the humanoid robots is represented by a combination of modular state nets for those parts. In order to obtain a feasible path of the whole body, a timed Petri net is used as an abstracted model of a set of all modular state nets. Next, we show an algorithm for constructing nonlinear dynamics which describes a periodic motion. Finally, we extend the state net in order to represent primitive periodic motions and their transition relation so that we can generate a sequence of primitive periodic motions satisfying a specified task.

In this paper, we propose a formal method for detection of three automation surprises in human-machine interaction; a mode confusion, a refusal state, and a blocking state. The mode confusion arises when a machine is in a different mode from that anticipated by the user, and is the most famous automation surprise. The refusal state is a situation that the machine does not respond to a command the user executes. The blocking state is a situation where an internal event occurs, leading to change of an interface the user does not know. In order to detect these phenomena, we propose a composite model in which a machine and a user model evolve concurrently. We show that the detection of these phenomena in human-machine interaction can be reduced to a reachability problem in the composite model.

This paper analyzes automation surprises in human-machine systems with time information. Automation surprises are phenomena such that the underlying machine's behavior diverges from user's intention and may lead to critical situations. Thus, designing human-machine systems without automation surprises is one of fundamental issues to achieve reliable user interaction with the machines. In this paper, we focus on timed human-machine interaction and address their formal aspects. The presented framework is essentially an extension of untimed human-machine interaction and will cover the previously proposed methodologies. We employ timed automata as a model of human-machine systems with time information. Modeling the human-machine systems as timed automata enables one to deal with not only discrete behavior but also time constraints. Then, by introducing the concept of timed simulation of the machine model and the user model, conditions which guarantee the nonexistence of automation surprises are derived. Finally, we construct a composite model in which a machine model and a user model evolve concurrently and show that automation surprises can be detected by solving a reachability problem in the composite model.