This project is a component of a larger effort is to develop the foundations of modeling, synthesis and development of verified medical device software and systems from verified closed-loop models of the device and organ(s). This research spans both implantable medical devices such as cardiac pacemakers and physiological control systems such as drug infusion pumps which have multiple networked medical systems. Here we focus on advancing two aspects of this work: (1) development of patient-specific models and therapies and (2) multi-scale modeling of complex physiological phenomena.

The CyberCardia project will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification.  The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behavior matches designer intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care.  

This project advances the scientific knowledge on design methods for improving the resilience of civil infrastructures to disruptions. To improve resilience, critical services in civil infrastructure sectors must utilize new diagnostic tools and control algorithms that ensure survivability in the presence of both security attacks and random faults, and also include the models of incentives of human decision makers in the design process.

Traditionally, autonomous cars make predictions about other drivers' future trajectories, and plan to stay out of their way. This tends to result in defensive and opaque behaviors. Our key insight is that an autonomous car's actions will actually affect what other cars will do in response, whether the car is aware of it or not. Our thesis is that we can leverage these responses to plan more efficient and

In a team decision problem, a team of agents interacts with a system; each agent receives a measurement that is probabilistically related to the state of the system; each agent uses its measurement to choose an action; and the team incurs a cost that is a function of the state of the system and the actions of the agents; the objective is to design the rules that the agents use to choose their actions in order to minimize the expected cost. Despite their simplicity, team decision problems are a fundamental building block of decentralized control, and the

Wide-area management of terrestrial scale infrastructures often involves human operators, who are sandwiched between physical-world systems and cyber- assets.  These Management Coupled Cyber-Physical Infrastructures (MCCPIs) are subject to diverse threats that can propagate across network elements.  In this research effort, a layered network modeling paradigm for MCCPIs is developed, and threats to cyber, physical, and human assets are modeled at several resolutions.

Human interaction with the physical world is increasingly mediated by autonomy, as planes assist pilots, robots assist surgeons, and cars assist drivers.  Automation is introduced in such systems to aid humans and guarantee safety and performance.  However, such guarantees are hard to provide, since humans may misunderstand the automation's intentions or behave in an unanticipated manner; tragic examples like the crash of Air France flight 447 illustrate that such confusion between pilots and autopilots can lead to catastrophic outcomes.

This research is high-risk and high-reward. Failure means that the resulting planning algorithms will make unfair decisions and prioritize a few organizations or donors, or will make fair, but inefficient allocation decisions, which will endanger social justice and community well-being. Success will improve both eciency of resource distribution and the quality of life of underserved populations in the United States.

This poster presents a uniform method for translating an arbitrary nondeterministic nite automaton (NFA) into a deterministic mass action chemical reaction network (CRN) that simulates it. The CRN receives its input as a continuous time signal consisting of concentrations of chemical species that vary to represent the NFA's input string in a natural way. The CRN exploits the inherent parallelism of chemical kinetics to simulate the NFA in real time, and its size is linear in the number of states of the NFA. The compiler of Chen et al.