상세정보
Export to Refworks부가기능
Spatio-Temporal Logics for Verification and Control of Networked Systems
상세 프로파일
| 자료유형 | 학위논문 |
|---|---|
| 서명/저자사항 | Spatio-Temporal Logics for Verification and Control of Networked Systems. |
| 개인저자 | Haghighi, Iman. |
| 단체저자명 | Boston University. Systems Engineering ENG. |
| 발행사항 | [S.l.]: Boston University., 2019. |
| 발행사항 | Ann Arbor: ProQuest Dissertations & Theses, 2019. |
| 형태사항 | 168 p. |
| 기본자료 저록 | Dissertations Abstracts International 81-04B. Dissertation Abstract International |
| ISBN | 9781085641722 |
| 학위논문주기 | Thesis (Ph.D.)--Boston University, 2019. |
| 일반주기 |
Source: Dissertations Abstracts International, Volume: 81-04, Section: B.
Advisor: Belta, Calin A. |
| 이용제한사항 | This item must not be sold to any third party vendors. |
| 요약 | 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 synthetic biology 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 for verification 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 demonstrated in 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 gradient descent. These algorithms are not restricted to the logics introduced in this dissertation 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. |
| 일반주제명 | Engineering. Applied mathematics. Computer science. |
| 언어 | 영어 |
| 바로가기 | 
: 이 자료의 원문은 한국교육학술정보원에서 제공합니다. |
