Some remarks on static-feedback linearization for time-varying systems

This work summarizes some results about static state feedback linearization for time-varying systems. Three different necessary and sufficient conditions are stated in this paper. The first condition is the one by [Sluis, W. M. (1993). A necessary condition for dynamic feedback linearization. Systems & Control Letters, 21, 277–283]. The second and the third are the generalizations of known results due respectively to [Aranda-Bricaire, E., Moog, C. H., Pomet, J. B. (1995). A linear algebraic framework for dynamic feedback linearization. IEEE Transactions on Automatic Control, 40, 127–132] and to [Jakubczyk, B., Respondek, W. (1980). On linearization of control systems. Bulletin del’Academie Polonaise des Sciences. Serie des Sciences Mathematiques, 28, 517–522]. The proofs of the second and third conditions are established by showing the equivalence between these three conditions. The results are re-stated in the infinite dimensional geometric approach of [Fliess, M., Lévine J., Martin, P., Rouchon, P. (1999). A Lie–Bäcklund approach to equivalence and flatness of nonlinear systems. IEEE Transactions on Automatic Control, 44(5), 922–937].     

Comments on: “Efficient robust constrained model predictive control with a time varying terminal constraint set” by Wan and Kothare

We present an algorithm that modifies the original formulation proposed in Wan and Kothare [Efficient robust constrained model predictive control with a time-varying terminal constraint set, Systems Control Lett. 48 (2003) 375–383]. The modified algorithm can be proved to be robustly stabilizing and preserves all the advantages of the original algorithm, thereby overcoming the limitation pointed out recently by Pluymers et al. [Min–max feedback MPC using a time-varying terminal constraint set and comments on “Efficient robust constrained model predictive control with a time-varying terminal constraint set”, Systems Control Lett. 54 (2005) 1143–1148].     

On-the-fly Workload Prediction and Redistribution in the Distributed Timed Model Checker Zeus

In this work we present the on-the-fly workload prediction and redistribution techniques used in Zeus [Braberman, V., A. Olivero and F. Schapachnik, Zeus: A distributed timed model checker based on kronos, in: Workshop on Parallel and Distributed Model Checking, affiliated to CONCUR 2002 (13^th International Conference on Concurrency Theory), ENTCS 68 (2002), Braberman, V., A. Olivero and F. Schapachnik, Issues in Distributed Model-Checking of Timed Automata: building zeus, to appear in International Journal of Software Tools for Technology Transfer (2004)], a Distributed Model Checker that evolves from the tool Kronos [Daws, C., A. Olivero, S. Tripakis and S. Yovine, The Tool KRONOS, in: Proceedings of Hybrid Systems III, LNCS 1066 (1996), pp. 208–219].After reviewing why it is so hard to have good speedups in distributed timed model checking, we present the methods used to get promising results when verifying reachability properties over timed automata [Alur, R. and D. L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994) 183–235].     

A linear time algorithm for monadic querying of indefinite data over linearly ordered domains

This paper demonstrates the generation of a linear-time query-answering algorithm based on the constructive proof of Higman’s lemma by Murthy and Russell [Proceedings of the 5th IEEE Symposium on Logic in Computer Science, 1990, p. 257–267]. The target problem is linear-time evaluation of a fixed disjunctive monadic query on an indefinite database over linearly ordered domains, first posed by van der Meyden [Proceedings of the 11th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1992, p. 331–345]. Van der Meyden showed the existence of a linear-time algorithm, but an explicit construction has, until now, not been reported.     

Fair Π

In this paper, we define fair computations in the π-calculus [Milner, R., Parrow, J. & Walker, D., A Calculus of Mobile Processes, Part I and II, Information and Computation 100 (1992) 1–78]. We follow Costa and Stirling's approach for CCS-like languages [Costa, G. & Stirling, C., A Fair Calculus of Communicating Systems, Acta Informatica 21 (1984) 417–441, Costa, G. & Stirling, C., Weak and Strong Fairness in CCS, Information and Computation 73 (1987) 207–244] but exploit a more natural labeling method of process actions to filter out unfair process executions. The new labeling allows us to prove all the significant properties of the original one, such as unicity, persistence and disappearance of labels. It also turns out that the labeled π-calculus is a conservative extension of the standard one. We contrast the existing fair testing [Brinksma, E., Rensink, A. & Vogler, W., Fair Testing, Proc. of CONCUR'95, LNCS, 962 (1995) 313–327, Natarajan, V. & Cleaveland, R., Divergence and Fair Testing, Proc. of ICALP '95, LNCS, 944 (1995) 648–659] with those that naturally arise by imposing weak and strong fairness as defined by Costa and Stirling. This comparison provides the expressiveness of the various fair testing-based semantics and emphasizes the discriminating power of the one already proposed in the literature.     

On the regular implementability of nD systems

In this short paper we study the problem of finding necessary and sufficient conditions for regular implementability by partial interconnection for nD system behaviors. In [M.N. Belur, H.L. Trentelman, Stabilization, pole placement and regular implementability, IEEE Trans. Automat. Control 47(5) (2002) 735–744.] such conditions were obtained in the context of 1D systems. In the present paper we show that the conditions obtained in [M.N. Belur, H.L. Trentelman, Stabilization, pole placement and regular implementability, IEEE Trans. Automat. Control 47(5) (2002) 735–744.] are no longer valid in general in the nD context. We also show that under additional assumptions, the conditions still remain relevant. We also reinvestigate the conditions for regular implementability by partial interconnection in terms of the canonical controller that were obtained in [P. Rocha, Canonical controllers and regular implementation of nD behaviors, Proceedings of the 16th IFAC World Congress, Prague, Czech Republic, 2005.]. Using the geometry of the underlying modules we generalize a result on regular implementability from the 1D to the nD case. Finally, we study how, in the 1D context, the conditions from [M.N. Belur, H.L. Trentelman, Stabilization, pole placement and regular implementability, IEEE Trans. Automat. Control 47(5) (2002) 735–744; P. Rocha, Canonical controllers and regular implementation of nD behaviors, Proceedings of the 16th IFAC World Congress, Prague, Czech Republic, 2005.] are connected.     

A Compact Linear Translation for Bounded Model Checking

We present a syntactic scheme for translating future-time LTL bounded model checking problems into propositional satisfiability problems. The scheme is similar in principle to the Separated Normal Form encoding proposed in [Frisch, A., D. Sheridan and T. Walsh, A fixpoint based encoding for bounded model checking, in: M.D. Aagaard and J.W. O'Leary, editors, Formal Methods in Computer-Aided Design; 4th International Conference, FMCAD 2002, Lecture Notes in Computer Science 2517 (2002), pp. 238–254] and extended to past time in [Cimatti, A., M. Roveri and D. Sheridan, Bounded verification of past LTL, in: A.J. Hu and A.K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer Aided Design (FMCAD 2004), Lecture Notes in Computer Science (2004)]: an initial phase involves putting LTL formulae into a normal form based on linear-time fixpoint characterisations of temporal operators.As with [Cimatti, A., M. Roveri and D. Sheridan, Bounded verification of past LTL, in: A.J. Hu and A.K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer Aided Design (FMCAD 2004), Lecture Notes in Computer Science (2004)] and [Latvala, T., A. Biere, K. Heljanko and T. Junttila, Simple bounded LTL model checking, in: Formal Methods in Computer-Aided Design; 5th International Conference, FMCAD 2004, Lecture Notes in Computer Science 3312 (2004), pp. 186–200], the size of propositional formulae produced is linear in the model checking bound, but the constant of proportionality appears to be lower.A denotational approach is taken in the presentation which is significantly more rigorous than that in [Frisch, A., D. Sheridan and T. Walsh, A fixpoint based encoding for bounded model checking, in: M.D. Aagaard and J.W. O'Leary, editors, Formal Methods in Computer-Aided Design; 4th International Conference, FMCAD 2002, Lecture Notes in Computer Science 2517 (2002), pp. 238–254] and [Cimatti, A., M. Roveri and D. Sheridan, Bounded verification of past LTL, in: A.J. Hu and A.K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer Aided Design (FMCAD 2004), Lecture Notes in Computer Science (2004)], and which provides an elegant alternative way of viewing fixpoint based translations in [Latvala, T., A. Biere, K. Heljanko and T. Junttila, Simple bounded LTL model checking, in: Formal Methods in Computer-Aided Design; 5th International Conference, FMCAD 2004, Lecture Notes in Computer Science 3312 (2004), pp. 186–200] and [Biere, A., A. Cimatti, E. M. Clarke, O. Strichman and Y. Zhu, Bounded model checking, Advances in Computers 58 (2003)].     

Averaging with disturbances and closeness of solutions

We establish that, under appropriate conditions, the solutions of a time-varying system with disturbances converge uniformly on compact time intervals to the solutions of the system's average as the rate of change of time increases to infinity. The notions of “average” used for systems with disturbances are the “strong” and “weak” averages introduced in Ne i and Teel (D. Ne i , A.R. Teel, Input-to-state stability for time-varying nonlinear systems via averaging, 1999, submitted for publication. See also: On averaging and the ISS property, Proceedings of the 38th Conference on Decision and Control, Phoenix, AZ, December 1999, pp. 3346–3351.)     

Maximal versus strong solution to algebraic Riccati equations arising in infinite Markov jump linear systems

We deal with a perturbed algebraic Riccati equation in an infinite dimensional Banach space which appears, for instance, in the optimal control problem for infinite Markov jump linear systems (from now on iMJLS). Infinite or finite here has to do with the state space of the Markov chain being infinite countable or finite (see, e.g., [M.D. Fragoso, J. Baczynski, Optimal control for continuous time LQ—problems with infinite Markov jump parameters, SIAM J. Control Optim. 40(1) (2001) 270–297]). By using a certain concept of stochastic stability (a sort of L₂-stability), we have proved in [J. Baczynski, M.D. Fragoso, Maximal solution to algebraic Riccati equations linked to infinite Markov jump linear systems, Internal Report LNCC, no. 6, 2006] existence (and uniqueness) of maximal solution for this class of equations. As it is noticed in this paper, unlike the finite case (including the linear case), we cannot guarantee anymore that maximal solution is a strong solution in this setting. Via a discussion on the main mathematical hindrance behind this issue, we devise some mild conditions for this implication to hold. Specifically, our main result here is that, under stochastic stability, along with a condition related with convergence in the infinite dimensional scenario, and another one related to spectrum—weaker than spectral continuity—we ensure the maximal solution to be also a strong solution. These conditions hold trivially in the finite case, allowing us to recover the result of strong solution of [C.E. de Souza, M.D. Fragoso, On the existence of maximal solution for generalized algebraic Riccati equations arising in stochastic control, Systems Control Lett. 14 (1990) 233–239] set for MJLS. The issue of whether the convergence condition is restrictive or not is brought to light and, together with some counterexamples, unveil further differences between the finite and the infinite countable case.     

Nonsmooth feedback stabilizer for strict-feedback nonlinear systems that may not be linearizable at the origin

We present a continuous feedback stabilizer for nonlinear systems in the strict-feedback form, whose chained integrator part has the power of positive odd rational numbers. Since the power is not restricted to be larger than or equal to one, the linearization of the system at the origin may fail. Nevertheless, we show that the closed loop system is globally asymptotically stable (GAS) with the proposed continuous (but, possibly not differentiable) feedback. We formulate a condition that enables our design by characterizing the powers of the given system. The condition also shows that our result is an extension of Qian and Lin [Non-lipschitz continuous stabilizers for nonlinear systems with uncontrollable unstable linearization, Systems Control Lett. 42 (2001) 185–200] where the power of odd positive integers has been considered. New result on the global finite time stabilization problem is also presented.