- All Categories
- Featured Events
- Alumni
- Application Deadline
- Arts
- Campus Discourse
- Careers
- BU Central
- Center for the Humanities
- Charity & Volunteering
- Kilachand Center
- Commencement
- Conferences & Workshops
- Diversity & Inclusion
- Examinations
- Food & Beverage
- Global
- Health & Wellbeing
- Keyword Initiative
- Lectures
- LAW Community
- Meetings
- Orientation
- Other Events
- Religious Services & Activities
- Special Interest to Women
- Sports & Recreation
- Social Events
- Study Abroad
- Weeks of Welcome
- Art Education Thesis ExhibitionAll day
- MFA Thesis Exhibition: Painting & Sculpture IIAll day
- MFA Thesis Exhibition: Graphic DesignAll day
- Moments In Time8:00 am
- Boston University's Information Security Annual Spring Shred10:00 am
- Sanghee Lim's PhD Dissertation Defense Seminar10:00 am
- 2019 John Cogan Patient Safety Lecture12:00 pm
- Drop-In Writing Assistance 12:00 pm
- GRS Dissertation Defense of Amir Effat12:30 pm
- SE PhD Final Defense of Iman Haghighi1:00 pm
- Current Topics Seminar – Jianjun Chen, Ph.D.2:00 pm
- GRS Dissertation Defense of Chi Zhang2:00 pm
- GRS Dissertation Defense of Alla Yalonetskaya Hamilton2:30 pm
- Dr. Mary Bassett: The Pursuit of Health, Equity, and Racial Justice4:30 pm
- Dr. Mary Bassett: The Pursuit of Health, Equity, and Racial Justice4:30 pm
- Memory in Living Room5:00 pm
- Drop-In Writing Assistance 5:00 pm
- Community of Educators Reception5:00 pm
- Women Faculty Networking Dinner5:30 pm
- Challah For Hunger - Baking5:30 pm
- ‘Sounding’ School and Sentience: Writing the Field Recording in Educational Ethnograph6:00 pm
- Baroque Chamber Concert6:30 pm
- BLUETS: A LECTURE IN SIX FUGUES7:30 pm
- THE LATHE OF HEAVEN7:30 pm
- MAINSTAGE OPERA: The Cunning Little Vixen by Leoš Janáček 7:30 pm
- Sargent Choice Test Kitchen8:00 pm
SE PhD Final Defense of Iman Haghighi
TITLE: SPATIO-TEMPORAL LOGICS FOR VERIFICATION AND CONTROL OF NETWORKEDSYSTEMS
ABSTRACT Emergent behaviors in networks of locally interacting dynamical systems have been a topic of great interest in recent years. As the complexity of these systems increases, so does the range of emergent properties that they exhibit. Due to recent developments in areas such as syntheticbiology and multi-agent robotics, there has been a growing necessity for a formal and automated framework for studying global behaviors in such networks. We propose a formal methods approach for describing, verifying, and synthesizing complex spatial and temporal network properties.
Two novel logics are introduced in the first part of this dissertation: Tree Spatial Superposition Logic (TSSL) and Spatial Temporal Logic (SpaTeL). The former is a purely spatial logic capable of formally describing global spatial patterns. The latter is a temporal extension of TSSL and is ideal for expressing how patterns evolve over time. We demonstrate how machine learning techniques can be utilized to learn logical descriptors from labeled and unlabeled system outputs. Moreover, these logics are equipped with quantitative semantics and thus provide a metric for distance to satisfaction for randomly generated system trajectories. We illustrate how this metric is used in a statistical model checking framework forverification of networks of stochastic systems.
The parameter synthesis problem is considered in the second part, where the goal is to determine static system parameters that lead to the emergence of desired global behaviors. We use quantitative semantics to formulate optimization procedures with the purpose of tuning system inputs. Particle swarm optimization is employed to efficiently solve these optimization problems, and the efficacy of this framework is demonstratedin two applications: biological cell networks and smart power grids.
The focus of the third part is the control synthesis problem, where the objective is to find time-varying control strategies. We propose two approaches to solve this problem: an exact solution based on mixed integer linear programming, and an approximate solution based on gradientdescent. We show that these algorithms are not restricted to the logics introduced in this paper and can be applied to other existing logics in the literature. Finally, the capabilities of our framework are shown in the context of multi-agent robotics and robotic swarms.
COMMITTEE: ADVISORCalin Belta, SE/ME; Ioannis Paschalidis, SE/ECE; Roberto Tron, SE/ME; Wenchao Li, SE/ECE; CHAIR Sean Andersson, SE/ME
When | 1:00 pm to 3:00 pm on Wednesday, May 1, 2019 |
---|---|
Location | 110 Cummington Mall, Room 245 |