Newswise — The National Science Foundation has awarded $1.86 million to three Stony Brook University professors to develop computational techniques for analyzing models of complex systems arising from a wide array of application domains. A particular focus of the research will be disease-related biological systems, including inter-cellular signaling in pancreatic cancer and fibrillation onset in cardiac tissue, and the control systems found embedded in automobiles, aircraft, and spacecraft.

The award is part of a five-year, $10 million grant in NSF's "Expeditions in Computing" initiative. Stony Brook faculty are teamed with scientists at Carnegie Mellon University, the project's lead institution, along with researchers at New York University, Cornell University, University of Maryland, University of Pittsburgh, NASA's Jet Propulsion Laboratory, and the City University of New York's Lehman College.

Scott Smolka, Professor of Computer Science is the principal investigator at Stony Brook University. He is also the project's Deputy Director, a position he shares with Computer Science Professor Amir Pnueli of NYU. Smolka and Pnueli will work closely with Project Director and lead PI Edmund M. Clarke, a professor of computer science at CMU. Pnueli and Clarke are both recipients of the ACM Turing Award, Computer Science's equivalent of the Nobel Prize.

Smolka is joined on the project by Stony Brook colleagues and co-investigators James Glimm, Distinguished Professor of Applied Mathematics and Statistics and Department Chair, and Radu Grosu, Associate Professor of Computer Science. Smolka's research focuses on concurrency theory, model checking, and the application of these techniques to biological, control and cyber-security systems. Grosu's research interests include model-based design and verification of cyber-physical systems. Glimm is renowned for his contributions to C*-algebras, quantum field theory, partial differential equations, and fluid dynamics, and is a recipient of the National Medal of Science.

Smolka, Grosu and Glimm will collaborate with co-investigators at Cornell University's Department of Physiology, Flavio Fenton and Robert F. Gilmour, Jr., to develop novel computational models of cardiac cells that will allow physicians to predict the onset of atrial fibrillation and other disturbances to the normal electrical activity of the human heart. Atrial fibrillation is the most common form of heart rhythm disturbance, contributes to congestive heart disease, and is responsible for 15 to 20 percent of all strokes. Moreover, its incidence increases with age, so the aging demographics of America mean that this condition afflicting 2 to 3 million people today could be a problem for 10 million by 2050.

The overall team of 19 scientists and engineers assembled for this NSF multi-institutional project will seek to combine Model Checking and Abstract Interpretation (MCAI), two methods that have been successful in finding errors in computer circuitry and software, and extend them so they can provide insights into models of complex systems, whether they are biological or electronic.

Model Checking is a widely used technique for detecting and diagnosing errors in complex hardware and software designs. It considers every possible state of a hardware or software design and determines if it is consistent with the designer's specifications; it produces diagnostic counter-examples when it uncovers inconsistencies. Model Checking is limited, however, by the size of the systems it can analyze.

Abstract Interpretation, by contrast, doesn't attempt to look at every possible state of a system, but rather to develop a simplified approximation of the system that preserves the particular properties that need to be assessed. This makes it possible to analyze very large, complex systems, such as the one million lines of code in the Airbus A380's primary flight control system, but with less precision than is possible with Model Checking.

"We hope to develop revolutionary techniques based on the next generation of the MCAI paradigm for automatically analyzing and predicting the behavior of biological and embedded control systems," says Smolka. "Using the new techniques, scientists and engineers will be able to greatly accelerate the pace of their discoveries by automating model-discovery and model-exploration tasks that currently must be performed manually."

"Undergraduate research is a key component of this project," Smolka also notes. "It provides for up to five research stipends for Stony Brook undergraduates per year, and to support an annual minority-focused workshop for undergraduates on understanding complex embedded and biological systems. In addition, a key project goal is to develop a highly ambitious cross-disciplinary educational program called 'Complex Systems Science Engineering.'"

Funding has also been set aside for graduate student stipends, and other research opportunities are available for Stony Brook graduate and postdoctoral students within the NASA JPL Research Affiliates Program.