This project aims at deriving a scalable, correct-by-construction formal design methodology for multi-robot systems that can guarantee the accomplishment of high-level team missions through automatic synthesis of local coordination mechanisms and control laws. The basic idea is to decompose the team mission into individual subtasks such that the design can be reduced to local synthesis problems for individual robots. Multidisciplinary approaches combining hybrid systems, supervisory control, regular inference and model checking are utilized to achieve this goal.

The objective of this research is to develop the theory, hardware and computational infrastructure that will enable automatically transforming user-defined, high-level tasks into correct, low-level perception informed control and configurations for modular robots. Modular robots are composed of simple individual modules with limited sensing and actuation; while each module can locomote in the environment, connecting multiple modules in different configurations allows modular robots to perform

Abstract: Robustness Guided Testing and Verification for Cyber-Physical Systems PI: Georgios Fainekos School of Computing, Informatics and Decision System Engineering, Arizona State University. E-mail: fainekos@asu.edu Website: http://www.public.asu.edu/~gfaineko

The powertrain control problem is one of regulating the air-to-fuel ratio in an automotive engine. A series of models of such controllers, with increasing levels of sophistication and fidelity to real-world designs, have been recently proposed by Toyota researchers as challenge problems for today’s verification technologies.

We present a bifurcation analysis of electrical alternans in the two-current Mitchell-Schaeffer (MS) cardiac-cell model using the theory of -decidability over the reals. Electrical alternans is a phenomenon characterized by a variation in the successive Action Potential Durations (APDs) generated by a single cardiac cell or tissue.

This project is a modular multi-robot cyber-physical system (CPS) for assisting young developmentally-delayed children learn to walk. The challenges of assisting young developmentally-delayed children learn to walk are 1) stabilizing medio-lateral body movement; and 2) developing gait that exploits potential and kinetic energy exchange. Typically, adults help children learn to walk by providing support that enables them to safely explore the environment.

This post considers a problem of target or source localization based on the measurements from a mobile sensor or a network of sensors. The assumption is that the received signal strength is strictly monotonic with the distance between the target and the sensor. No explicit signal propagation model, neither the structure nor the mathematical description, is assumed or used in localization. It shows that this mere knowledge of monotonicity suffices in locating the unknown target in the absence of noise.

Optimization algorithms used in a real-time and safety-critical context offer the potential for considerably advancing robotic and autonomous systems by improving their ability to execute complex missions. However, this promise cannot happen without proper attention to the considerably stronger operational constraints that real time, safety-critical applications must meet, unlike their non-real-time, desktop counterparts.