| LDR | | 00000nam u2200205 4500 |
| 001 | | 000000433075 |
| 005 | | 20200225111940 |
| 008 | | 200131s2019 ||||||||||||||||| ||eng d |
| 020 | |
▼a 9781085641722 |
| 035 | |
▼a (MiAaPQ)AAI13883558 |
| 040 | |
▼a MiAaPQ
▼c MiAaPQ
▼d 247004 |
| 082 | 0 |
▼a 004 |
| 100 | 1 |
▼a Haghighi, Iman. |
| 245 | 10 |
▼a Spatio-Temporal Logics for Verification and Control of Networked Systems. |
| 260 | |
▼a [S.l.]:
▼b Boston University.,
▼c 2019. |
| 260 | 1 |
▼a Ann Arbor:
▼b ProQuest Dissertations & Theses,
▼c 2019. |
| 300 | |
▼a 168 p. |
| 500 | |
▼a Source: Dissertations Abstracts International, Volume: 81-04, Section: B. |
| 500 | |
▼a Advisor: Belta, Calin A. |
| 502 | 1 |
▼a Thesis (Ph.D.)--Boston University, 2019. |
| 506 | |
▼a This item must not be sold to any third party vendors. |
| 520 | |
▼a 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. |
| 590 | |
▼a School code: 0017. |
| 650 | 4 |
▼a Engineering. |
| 650 | 4 |
▼a Applied mathematics. |
| 650 | 4 |
▼a Computer science. |
| 690 | |
▼a 0537 |
| 690 | |
▼a 0364 |
| 690 | |
▼a 0984 |
| 710 | 20 |
▼a Boston University.
▼b Systems Engineering ENG. |
| 773 | 0 |
▼t Dissertations Abstracts International
▼g 81-04B. |
| 773 | |
▼t Dissertation Abstract International |
| 790 | |
▼a 0017 |
| 791 | |
▼a Ph.D. |
| 792 | |
▼a 2019 |
| 793 | |
▼a English |
| 856 | 40 |
▼u http://www.riss.kr/pdu/ddodLink.do?id=T15491313
▼n KERIS
▼z 이 자료의 원문은 한국교육학술정보원에서 제공합니다. |
| 980 | |
▼a 202002
▼f 2020 |
| 990 | |
▼a ***1816162 |
| 991 | |
▼a E-BOOK |