This article investigates the estimate (i.e., the invariant subset) of domain of attraction (DOA) for complex network. Starting with the quadratic Lyapunov function of isolated node, we construct a quadratic Lyapunov function of complex network for estimating the DOA of network. In this way, if the largest spherical estimate of the DOA for isolated node can be obtained, we can directly obtain the largest spherical estimate of the DOA for network. Then, for improving the existing estimate, we directly utilize the Laplacian matrix to ingeniously construct a new Lyapunov-like function, relaxing the constraint that the derivative of the Lyapunov function is negative definite in a neighborhood of the origin. Moreover, we iteratively compute Lyapunov-like functions to maximize the obtained estimate as far as possible. Afterward, for polynomial networks, the estimate problem of the DOA is transformed into a classical sum of squares (SOS) programming problem. Particularly, we use the properties of isolated node and network topology to significantly reduce the computational complexity of the above SOS programming problem, such that our estimate can be effectively obtained even for large-scale networks. Finally, four examples are given to illustrate the validity of our theoretical results and the efficiency of our computable approach.

In this work, we investigate the reach-avoid problem of a class of time-varying analytic systems with disturbances described by uncertain parameters. Firstly, by proposing the concepts of maximal and minimal reachable sets, we connect the avoidability and reachability with maximal and minimal reachable sets respectively. Then, for a given disturbance parameter, we introduce the evolution function for exactly describing the reachable set, and find a series representation of this evolution function with its Lie derivatives, which can also be regarded as a series function with respect to the uncertain parameter. Afterward, based on the partial sums of this series, over- and under-approximations of the evolution function are constructed, which can be realized by interval arithmetics with designated precision. Further, we propose sufficient conditions for avoidability and reachability and design a numerical quantifier elimination-based algorithm to verify these conditions; moreover, we improve the algorithm with a time-splitting technique. We implement the algorithms and use some benchmarks with comparisons to show that our methodology is both efficient and promising. Finally, we additionally extend our methodology to deal with systems with complex initial sets and time-dependent switchings. The performance of our extended method for these systems is also shown by four examples with comparisons and discussions.

In this article, the synchronization issue of certain edge-colored networks is investigated. We start with a linear subspace determined by the colored edges and show that the invariant kernel of this linear subspace is precisely consists of all the synchronous states. Moreover, this invariant kernel is characterized by a cluster of algebraic equations. Especially, for network described by a polynomial vector field, due to the property of Noetherian rings, this invariant kernel can be determined by a finite number of algebraic equations. Furthermore, the equivalence between network synchronization and the asymptotic behavior of the aforementioned invariant kernel are proved. Based on the colored edges and the invariant kennel, we decompose the original network twice, arriving at a three-layer network: the first two layers, referred to as the external part, can only synchronize to an equilibrium point, while the third layer, known as the internal part, possesses the same colored edges. For this three-layer network, we construct two Lyapunov-type functions for the external part and the internal part, respectively, to establish the synchronization criteria. In particular, our criteria involve linear matrix inequalities and polynomial inequalities of smaller scale, which can be solved by the existing semi-definite programming tools. Finally, this article provides three examples to illustrate the effectiveness and advantages of the theoretical results presented.

In this work, we investigate the reach-avoid problem of a class of time-varying analytic systems with disturbances described by uncertain parameters. Firstly, by proposing the concepts of maximal and minimal reachable sets, we connect the avoidability and reachability with maximal and minimal reachable sets respectively. Then, for a given disturbance parameter, we introduce the evolution function for exactly describing the reachable set, and find a series representation of this evolution function with its Lie derivatives, which can also be regarded as a series function w.r.t. the uncertain parameter. Afterward, based on the partial sums of this series, over- and under-approximations of evolution function are constructed, which can be realized by interval arithmetics with designated precision. Further, we propose sufficient conditions for avoidability and reachability and design a numerical quantifier elimination based algorithm to verify these conditions; moreover, we improve the algorithm with a time-splitting technique. Finally, we implement the algorithm and use some benchmarks with comparisons to show that our methodology is both efficient and promising.

In this article, based on polynomial differential inclusions, we propose a heuristic iterative approach for estimating the domains of attraction for nonpolynomial systems. First, we use the fuzzy model to construct a polynomial differential inclusion for the nonpolynomial system, which can be equivalently written as a time-invariant uncertain polynomial system. Then, beginning with an initial inner estimation, we present an iterative approach to enlarge this initial inner estimation by calculating common Lyapunov-like functions. Furthermore, the domains of attraction are estimated by combining this iterative approach with heuristic construction of differential inclusions. In the end, our heuristic iterative approach is implemented with linear semidefinite programming and then tested on some nonpolynomial examples with comparisons to the existing methods in the literature.

In this article, we search for polynomial Lyapunov functions beyond the quadratic form to investigate the synchronization problems of nonlinearly coupled complex networks. First, with a relaxed assumption than the quadratic condition, a synchronization criterion is established for nonlinearly coupled networks with asymmetric coupling matrices. Compared with the existing synchronization criteria, our results are less conservative and have a wider application. Second, the synchronization problem for polynomial networks is characterized as the sum-of-squares (SOS) optimization one. In this way, polynomial Lyapunov functions can be obtained efficiently with SOS programming tools. Furthermore, it is shown that the local synchronization of certain nonpolynomial networks can also be analyzed by using the SOS optimization method through the Taylor series expansion. Finally, three numerical examples are presented to verify the effectiveness and less conservatism of our analytical results.

The classical planning problem aims to find a sequence of permitted actions leading a system to a designed state, i.e., to achieve the system’s task. However, in many realistic cases we also have requirements on how to complete the task, indicating that some behaviors and situations are more preferred than others. In this paper, we present the probabilistic preference-based planning problem ($\mathrm{P4}$) for Markov decision processes, where the preferences are defined based on an enriched probabilistic LTL-style logic. We first recall$\mathrm{\mathrm{P4} {}Solver}$, an SMT-based planner computing the preferred plan by reducing the problem to a quadratic programming one previously developed to solve$\mathrm{P4}$. To improve computational efficiency and scalability, we then introduce a new encoding of the probabilistic preference-based planning problem as a multi-objective model checking one, and propose the corresponding planner$\mathrm{\mathrm{P4} {}Solver} _{{MO}}$. We illustrate the efficacy of both planners on some selected case studies to show that the model checking-based algorithm is considerably more efficient than the quadratic-programming-based one.

In this paper, the synchronization problem of complex networks with linearly diffusively coupled nonidentical nodes is investigated. Starting with the boundedness condition of network trajectories, we introduce an invariant set such that it contains all limit points of ultimately synchronous trajectories. Then, we develop a decomposition technique for the heterogeneous network. With this decomposition, the synchronization of the network can be investigated by the convergence of one decomposed network and the synchronization of the other decomposed homogeneous-like network. Moreover, for a particular case that the invariant set is a linear subspace, conditional synchronization analysis is provided to reduce the coupling complexity between the two decomposed networks. It is noted that our decomposition technique is quite simple yet general: by this technique, the synchronization of various heterogeneous complex networks can be transformed into the stability of nonlinear systems and synchronization of homogeneous-like complex networks. Finally, we present several numerical examples to demonstrate the effectiveness of the theoretical results. In particular, we use an example to show that our theoretical procedure is also feasible for some heterogeneous networks with a general invariant submanifold instead of linear subspace.

In this article, we investigate the inner estimations of the minimal domains of attraction (MDA) for uncertain nonlinear systems, whose uncertainties are modeled by parameters defined in a semialgebraic set. We begin from an initial inner estimation of MDA and then enlarge this initial inner estimation by iterative calculating common Lyapunov-like functions with a linear sum of squares programming-based approach. Afterwards, this enlarged inner estimation of MDA is further improved by iterative computations of parameter-dependent Lyapunov-like functions. Especially, we use a simple semialgebraic set, described by a polynomial level-set function, to under-approximate this improved estimation. In the end, our methods are implemented and tested on several uncertain examples with comparisons to existing methods in the literatures.

The classical planning problem can be enriched with quantitative and qualitative user-defined preferences on how the system behaves on achieving the goal. In this paper, we propose the probabilistic preference planning problem for Markov decision processes, where the preferences are based on an enriched probabilistic LTL-style logic. We develop P4Solver, an SMT-based planner computing the preferred plan by reducing the problem to quadratic programming problem, which can be solved using SMT solvers such as Z3. We illustrate the framework by applying our approach on two selected case studies.

In this paper we propose a mechanisable approach for discovering multiple Lyapunov functions for switched hybrid systems. We start with the classical definition on asymptotic stability, which can be assured by the existence of multiple Lyapunov functions. Then, we derive an algebraizable sufficient condition on multiple Lyapunov functions in quadratic form for asymptotic stability analysis. Since different modes are considered, in addition to real root classification, we further apply a projection operator step by step to under-approximate this sufficient condition and obtain a set of semi-algebraic sets which only involve the coefficients of the multiple Lyapunov function. Moreover, for each step, we use the information on modes to optimize our intermediate computation results. Finally, we compute a sample point in the resulting semi-algebraic sets for coefficients. We tested our approach on five examples using prototypical implementation. The computation and comparison results demonstrate the applicability and efficiency of our approach.

In this paper we propose a mechanisable technique for asymptotic stability analysis of continuous dynamical systems. We start from linearizing a continuous dynamical system, solving the Lyapunov matrix equation and then check whether the solution is positive definite. For the cases that the Jacobian matrix is not a Hurwitz matrix, we first derive an algebraizable sufficient condition for the existence of a Lyapunov function in quadratic form without linearization. Then, we apply a real root classification based method step by step to formulate this derived condition as a semi-algebraic set such that the semi-algebraic set only involves the coefficients of the pre-assumed quadratic form. Finally, we compute a sample point in the resulting semi-algebraic set for the coefficients resulting in a Lyapunov function. In this way, we avoid the use of generic quantifier elimination techniques for efficient computation. We prototypically implemented our algorithm based on DISCOVERER. The experimental results and comparisons demonstrate the feasibility and promise of our approach.