Verification of temporal logic properties plays a crucial role in proving the desired behaviors of continuous systems. In this paper, we propose an interval method that verifies the properties described by a bounded signal temporal logic. We relax the problem so that if the verification process cannot succeed at the prescribed precision, it outputs an inconclusive result. The problem is solved by an efficient and rigorous monitoring algorithm. This algorithm performs a forward simulation of a continuous-time dynamical system, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. In each step, the continuous state at a certain time is enclosed by an interval vector that is proven to contain a unique solution. We experimentally demonstrate the utility of the proposed method in formal analysis of nonlinear and complex continuous systems.

An efficient and practical algorithm is proposed for finding all DC solutions of nonlinear circuits. This algorithm is based on interval analysis and linear programming techniques. The proposed algorithm is very efficient and can be easily implemented by using the free package GLPK (GNU Linear Programming Kit). By numerical examples, it is shown that the proposed algorithm could find all solutions of a system of 2 000 nonlinear circuit equations in practical computation time.

Recently, an efficient algorithm has been proposed for finding all solutions of systems of nonlinear equations using inverses of approximate Jacobian matrices. In this letter, an effective technique is proposed for improving the computational efficiency of the algorithm with a little bit of computational effort.

Recently, an efficient algorithm has been proposed for finding all solutions of systems of nonlinear equations using linear programming. In this algorithm, linear programming problems are formulated by surrounding component nonlinear functions by rectangles. In this letter, it is shown that weakly nonlinear functions can be surrounded by smaller rectangles, which makes the algorithm very efficient.

Related with accuracy, computational complexity and so on, quality of computing for the so-called homotopy method has been discussed recently. In this paper, we shall propose an estimation method with interval analysis of region in which unique solution path of the homotopy equation is guaranteed to exist, when it is applied to a certain class of uniquely solvable nonlinear equations. By the estimation, we can estimate the region a posteriori, and estimate a priori an upper bound of the region.

An efficient algorithm is proposed for finding all solutions of bipolar transistor circuits. This algorithm is based on a simple test that checks the nonexistence of a solution using linear programming. In this test, right-angled triangles are used for surrounding exponential functions of the Ebers-Moll model, by which the number of inequality constraints decreases and the test becomes efficient and powerful.

This paper reviews two topics of nonlinear system analysis done in Japan. The first half of this paper concerns with nonlinear system analysis through the nondeterministic operator theory. The nondeterministic operator is a set-valued or fuzzy set valued operator by K. Horiuchi. From 1975 Horiuchi has developed fixed point theorems for nondeterministic operators. Using such fixed point theorems, he developed a unique theory for nonlinear system analysis. Horiuchi's theory provides a fundamental view point for analysis of fluctuations in nonlinear systems. In this paper, it is pointed out that Horiuchi's theory can be viewed as an extension of the interval analysis. Next, Urabe's theory for nonlinear boundary value problems is discussed. From 1965 Urabe has developed a method of computer assisted existence proof for solutions of nonlinear boundary value problems. Urabe has presented a convergence theorem for a certain simplified Newton method. Urabe's theorem is essentially based on Banach's contraction mapping theorem. In this paper, reformulation of Urabe's theory using the interval analysis is presented. It is shown that sharp error estimation can be obtained by this reformulation. Both works discussed in this paper have been done independently with the interval analysis. This paper points out that they have deep relationship with the interval analysis. Moreover, it is also pointed out that these two works suggest future directions of the interval analysis.

Data of system parameters of real systems have some uncertainty and they should be given by sets (or intervals) rather than fixed values. To analyze and design systems contaning such uncertain parameters, it is required to represent and treat uncertainty in data of parameters, and to compute value sets of characteristic polynomials and transfer functions. Interval arithmetic is one of the most powerful tools to perform such subjects. In this paper, Polygon Interval Arithmetic (PIA) on the set of polygons in the complex plane is considered, and the data structure and algorithms to execute PIA efficiently is proposed. Moreover, practical examples are shown to demonstrate how PIA is useful to compute the evaluation of value sets.