-
Abstract—For series interconnection of non-deterministic, continuous-time linear systems, we develop a modular verification and design framework that utilises the notion of (γ,δ)- similarity to measure to what extent a global specification is satisfied in an approximate sense. We first address the modular verification problem where we make use of our prior knowledge of local specifications on components to replace each high-dimensional component by its low-dimensional specification and then conduct verification on the basis of these local specifications. We therefore derive a condition that guarantees the global specification solely on the basis of local specifications. We characterise this condition as a linear matrix inequality feasibility problem that is only in terms of the parameters of the (global and local) specifications. We then address the modular design problem where for a given component and its associated specification, we design the other component such that the resulting series interconnection satisfies the global specification. We characterise the existence of such component as a linear matrix inequality feasibility problem that is only in terms of the parameters of the (local and global) specifications rather than those of the component. On the basis of this characterisation, we propose an algorithm to construct the component.
-
Abstract—We develop a modular verification and synthesis framework that utilizes assume-guarantee contracts to express specifications on the asymptotic external behavior of linear dynamical systems. We describe the asymptotic behavior of a system in terms of the solution trajectories of an autonomous exosystem and accordingly construct contracts as pairs of two subspaces of matrices, namely assumptions and guarantees. The assumptions subspace specifies the acceptable asymptotic behavior of external inputs to a system, whereas the guarantees subspace specifies the allowed asymptotic behavior of the system output. We formalize this by introducing the notion of implementation which is then characterized in terms of the solvability of regulator equations. Based on this characterization, we propose a computationally effective technique that verifies contracts by solving a linear matrix equation solely determined by system parameters, the basis of assumptions, and the basis of guarantees. We then construct the series composition of contracts to conduct modular verification for interconnected systems with series architecture. Finally, for systems that fail to implement a contract, we conceive the notion of controlled implementation, which determines the possibility of enforcing a system to implement a contract through control synthesis.
-
Abstract—We compensate for the scalability issues in controller synthesis by developing a hierarchical control scheme within the framework of (γ,δ)-similarity, which measures to what extent a potentially non-deterministic system satisfies specifications expressed as solution trajectories of a dynamical ‘specification’ system. This scheme synthesizes a controller for a non-deterministic ‘concrete’ system in three hierarchical steps. First, an ‘abstract’ system, which is a low-dimensional model of the concrete system, is obtained. Then, a controller is designed for the abstract system. At last, the abstract controller is refined into the concrete controller through an ‘interface’. To enable this, we introduce and characterize the notion of (γ,δ)-abstraction that utilizes an L2 approximation metric to measure the behavioral similarity of the concrete system and its abstraction in the presence of the interface. We utilize this characterization to propose a step-by-step procedure to construct the interface. We then synthesize the abstract controller and refine it into a concrete one.
-
Abstract—For non-deterministic linear ‘concrete’ systems, we develop a control framework that conducts controller synthesis within three hierarchical steps. First, a low-dimensional ‘abstract’ system is obtained that behaves similarly to the concrete system in an input-output sense. Then, a con- troller is designed for the abstract system. Due to the low-dimensionality of the abstract system, designing such controller is computationally efficient. At last, the synthesized abstract controller is refined into a concrete controller using an ‘interface’. We introduce the notion of (γ,δ,ρ)-abstraction to measure the behavioral similarity of the concrete system and its abstraction in the presence of the interface and the abstract controller. Utilizing an L2 approximation metric to measure behavioral similarity, (γ,δ,ρ)-abstraction induces a hierarchical control framework that is compatible with existing effective methods for analysis and synthesis of control systems, in particular, techniques from robust control and dissipativity theory. We characterize the notion of (γ,δ,ρ)-abstraction as a linear matrix inequality feasibility problem. We then exploit this to characterize the existence of an abstract system in terms of a rank-constrained linear matrix inequality feasibility problem. On the basis of such feasibility problem, we propose an algorithm to construct the abstract system and interface.
-
Abstract—We introduce (γ,δ)-similarity, a notion of system comparison that measures to what extent two stable linear dynamical systems behave similarly in an input-output sense. This behavioral similarity is characterized by measuring the sensitivity of the difference between the two output trajectories in terms of the external inputs to the two potentially non-deterministic systems. As such, (γ,δ)-similarity is a notion that characterizes approximation of input-output behavior, whereas existing notions of simulation target equivalence. Next, as this approximation is specified in terms of the L2 signal norm, (γ,δ)-similarity allows for integration with existing methods for analysis and synthesis of control systems, in particular, robust control techniques. We characterize the notion of (γ,δ)-similarity as a linear matrix inequality feasibility problem and derive its interpretation in terms of transfer matrices. Our study on the compositional properties of (γ,δ)-similarity shows that the notion is preserved through series and feedback interconnections. This highlights its potential application in compositional reasoning, namely abstraction and modular synthesis of large-scale interconnected dynamical systems. We further illustrate our results in an electrical network example.
-
Abstract—Through the combination of contraction mapping and pseudospectral method, we propose a successive approximation technique to approximate the solution of a class of regulator equations with periodic exosystems and hyperbolic zero dynamics. In this scheme, the initial points of flows on the zero-error constrained manifolds are approximated successively as the fixed point of a contractive integral mapping. Accordingly, flows are obtained by utilizing the scaled Fourier–Gauss–Radau collocation method. Appropriate error analysis, in association with both regulation error and the error resulting from the approximate solution of the center manifold equation, is provided. Our analysis shows that the regulation error becomes negligible as we start the approximation process at an adequately large order and maintain it for a proper number of iterations.
-
Abstract—This article presents a novel geometric framework for the design of extended state observers (ESOs) using the immersion and invariance (I&I) method. The ESO design problem of a class of uncertain lower-triangular nonlinear systems is considered for joint state and total disturbance observation. This problem is formulated as designing a dynamical system, as the observer, along with an appropriately defined manifold in the system-observer extended state-space. The ESO convergence translates into the attractivity of this manifold; that is, the convergence of the system-observer trajectories to a small boundary layer around the manifold. The design of both reduced-order and full-order ESOs is studied using the I&I formulation. Moreover, an optimization method based on linear matrix inequalities is proposed to establish the convergence of ESOs. It is shown that the I&I-based method leads to a unifying framework for the design and analysis of ESOs with linear, nonlinear, and time-varying gains. Detailed simulations are provided to show the efficacy of the proposed ESOs.
-
Abstract—We investigate the formation of cancer stem cells and their role in maintaining avascular solid tumors. For this purpose, we provide a mathematical framework to study the major biological interpretations on the stemness of cancerous cells (stochastic scheme) and the self-renewal ability of particular progenitor cells (hierarchical scheme). These interpretations are related to the genetic characteristics of cancer, which could be described by a set of mechanisms shared by all types of cancer, i.e., hallmarks of cancer. Hallmarks of cancer relate cellular genetics, differentiation and heterogeneity, and tumor micro-environment (TME). To reach our goal, based on hallmarks of cancer, we propose a hybrid discrete-continuous model that combines continual interactions of cellular genetics and tumor micro-environment. Using this model, we conduct computational experiments on EMT6/Ro tumor to study the possibility of stochastic and hierarchical schemes. Our experiments suggest that even in well-suited genomic and micro-environmental conditions, a tumor survives only when the majority of tumor cells are in the stemness state (stochastic approach), or progenitor to CSC transition exists (hierarchical approach). In the lack of progenitor to CSC transition, in the hierarchical scheme, the tumor fades away due to the CSCs malnutrition. These results are supported by a sensitivity analysis of the model parameters. Although our computational experiments are carried out for the EMT6/Ro tumor, due to the generic nature of this approach, we believe, this work could provide insights regarding similar behaviors in other tumors.
Journal Publications
-
Abstract—We propose a methodology that exploits the contract formalism to characterize the continuous-time safety control problem, which is often difficult to address, in terms of a discrete-time one for which numerous efficient solution scheme exist. We construct contracts as pairs of assumptions and guarantees which are set-valued mappings that describe the safe boundaries within which the system must operate. By formalizing safety control as contract implementation, we develop a vertical hierarchy according to which we translate implementation from continuous to discrete time. We accomplish this by constructing a discrete-time contract and system in such a way that any solution of the discrete-time implementation problem completely characterizes that of the original continuous-time one. We then use this characterization to construct a control input that establishes implementation in continuous time on the basis of the control sequence that achieves implementation in discrete time.
-
Abstract—We address the problems of specification verification and controller synthesis in the context of (γ,δ)-similarity, a notion of approximate system comparison that measures to what extent the external behaviors of two potentially non-deterministic systems are similar in an L2 sense. Expressing specifications in terms of input-output trajectories of a dynamical system, we use (γ,δ)-similarity to verify whether the external behavior of a system satisfies such specifications in an approximate sense. We characterize this problem as a linear matrix inequality feasibility problem. In case a control system fails to satisfy specifications with a desired accuracy, we synthesize a dynamic controller that enforces specification satisfaction. We characterize the synthesis problem in terms of a bilinear matrix inequality feasibility problem. Aware of the computational costs for solving such problem, we obtain a sufficient condition for the existence of the controller that can be expressed in terms of a linear matrix inequality. Based on this, we propose an algorithm to construct the controller.
-
Abstract—A large variety of social robots with various applications have been developed recently in order to improve Human-Robot Interaction (HRI) and satisfy certain social needs such as companionship. However, they cannot be deployed in Middle East due to their inability to have verbal communications in user's native language, availability issues, and high costs. This research introduces the design and development of a semi-autonomous robot called RoboParrot which can be used in various applications such as Autism Spectrum Disorder (ASD) therapy, teaching foreign languages, and elderly companionship. Previous versions of RoboParrot have been successfully deployed as a tool for ASD screening and have shown high acceptance rates among children. The new version has been used for interaction with both autistic and typical children and also elderly people. The platform is capable of adding further features to increase its autonomy so it can be widely used in homes of independent-living elderly people, nursing home, hospitals, and for home based ASD therapy. In order to expand applicable fields, various features have been added to the robot making it a multi-purpose portable social robot.
Conference Proceedings
-
Abstract—We develop a formal framework for the behavioral comparison of linear systems across different time domains. We accomplish this by introducing the notion of system interpolation, which determines whether the input-state trajectories of a continuous-time system can be realized as a piece-wise polynomial interpolation of the input-state trajectories of a discrete-time system. In this context, piecewise polynomial interpolations of a discrete-time signal are characterized as continuous-time functions that coincide with the discrete-time signal at given sampling instants and can be realized as a polynomial of a prescribed degree over intervals between these instants. By representing piecewise polynomial functions as linear combinations of shifted Legendre polynomials, we characterize system interpolation as a subspace inclusion that is completely in terms of system parameters. This therefore allows for a computationally efficient comparison of the input-state behavior of a continuous-time system with that of a discrete-time one. We then utilize this characterization to identify the set of all inputs that enforce the continuous-time system to generate piece-wise polynomial interpolations of a given discretetime trajectory. Lastly, given a control specification, we utilize system interpolation to synthesize controllers that ensure satisfaction at each given sampling instant, while they measure the extent of (possible) violation over intervals between these instants.
-
Abstract—We introduce the notion of asymptotic similarity which compares the asymptotic external behavior of two non-deterministic continuous-time stable linear systems. Describing the asymptotic external behaviors in terms of the solution trajectories of an autonomous exosystem, asymptotic similarity determines the ability of a system in reproducing the asymptotic external behavior of another system. We characterize the notion of asymptotic similarity in terms of the solvability of regulator equations that are solely in terms of system matrices. We accordingly characterize the solvability of these equations as a subspace inclusion which allows one to determine asymptotic similarity through rank computation. We then conceive and characterize the notion of asymptotic bisimilarity which is a symmetric version of asymptotic similarity in the sense that it determines the equivalence of the asymptotic behaviors of systems. By specializing asymptotic similarity to deterministic systems, we give an interpretation of the notion in terms of the transfer matrices of systems. We also propose a technique to extract and compare the transient behavior of asymptotically similar systems. We finally extend the notion of asymptotic similarity to interconnected systems and show that it is preserved through series and feedback interconnections.
Preprints/Submitted Papers
-
Abstract—For linear continuous-time systems, we solve the signal temporal logic control problem by translating it from continuous to discrete time such that a solution to the discrete-time problem guarantees a solution to the original continuous-time one. We split control synthesis into three hierarchical tasks. First, we discretise the continuous-time STL formula into a discrete-time one by sampling the temporal behaviour it specifies. We accordingly discretise the continuous-time system by constructing a discrete-time model such that the input-state trajectories of the continuous-time system can be characterised as piecewise polynomial interpolations of the input-state trajectories of the discrete-time model. Second, we exploit this characterisation to formulate mixed-integer linear constraints on the discrete-time trajectories that allow for planning a trajectory whose piecewise polynomial interpolation satisfies the continuous-time STL formula. In fact, system discretisation and trajectory planning are performed in such a manner that any feasible solution to these constraints gives a discrete-time trajectory that can be transformed into a continuous-time one guaranteed to satisfy the original STL formula. Third, we propose a step-by-step algorithm to construct the control input that realises such continuous-time trajectory.
-
Manuscripts in Preparation