{"633503":{"#nid":"633503","#data":{"type":"event","title":"Ph.D. Dissertation Defense - Maxence Dutreix","body":[{"value":"\u003Cp\u003E\u003Cstrong\u003ETitle\u003C\/strong\u003E\u003Cem\u003E:\u0026nbsp; \u003C\/em\u003E\u003Cem\u003EVerification and Synthesis for Stochastic Systems with Temporal Logic Specifications\u003C\/em\u003E\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u003Cstrong\u003ECommittee:\u003C\/strong\u003E\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Samuel Coogan, ECE, Chair , Advisor\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Fumin Zhang, ECE\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Ye Zhao, ME\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Yorai Wardi, ECE\u003C\/p\u003E\r\n\r\n\u003Cp\u003EDr. Kyriakos Vamvoudakis, AE\u003C\/p\u003E\r\n\r\n\u003Cp\u003E\u003Cstrong\u003EAbstract: \u003C\/strong\u003E\u003C\/p\u003E\r\n\r\n\u003Cp\u003EThe objective of this thesis is to first provide a formal framework for the verification of discrete-time, continuous-space stochastic systems with complex temporal specifications. As these problems are generally undecidable or intractable to solve, approximation methods are employed in the form of finite-state abstractions arising from a partition of the original system\u0026#39;s domain for which analysis is greatly simplified. The abstractions of choice in this work are Interval-valued Markov Chains (IMC) which, unlike conventional discrete-time Markov Chains, allow for a non-deterministic range of probabilities of transition between states instead of a fixed probability. Techniques for constructing IMC abstractions which rely on structural properties of the dynamics are presented for the class of mixed monotone systems and the class of polynomial systems. Next, an algorithm for computing satisfaction bounds in IMCs with respect to so-called omega-regular properties is detailed. As probabilistic specifications require finding the set of initial states whose probability of fulfilling some behavior is below or above a certain threshold, this method may yield a set of states whose satisfaction status is undecided. An iterative specification-guided partition refinement method is proposed to reduce conservatism in the abstraction until a precision threshold is met. Secondly, the approach developed for verification is extended to the synthesis of controllers that aim to maximize or minimize the probability of occurrence of temporal behaviors in stochastic systems. Similar interval-based finite abstractions are utilized to synthesize control policies for omega-regular objectives in systems with both a finite number of modes and a continuous set of available inputs. A notion of optimality for these policies is introduced and a partition refinement scheme is presented to reach a desired level of optimality.\u003C\/p\u003E\r\n","summary":null,"format":"limited_html"}],"field_subtitle":"","field_summary":"","field_summary_sentence":[{"value":"Verification and Synthesis for Stochastic Systems with Temporal Logic Specifications "}],"uid":"28475","created_gmt":"2020-03-11 18:39:00","changed_gmt":"2020-03-29 14:40:43","author":"Daniela Staiculescu","boilerplate_text":"","field_publication":"","field_article_url":"","field_event_time":{"event_time_start":"2020-04-09T15:00:00-04:00","event_time_end":"2020-04-09T17:00:00-04:00","event_time_end_last":"2020-04-09T17:00:00-04:00","gmt_time_start":"2020-04-09 19:00:00","gmt_time_end":"2020-04-09 21:00:00","gmt_time_end_last":"2020-04-09 21:00:00","rrule":null,"timezone":"America\/New_York"},"extras":[],"groups":[{"id":"434381","name":"ECE Ph.D. Dissertation Defenses"}],"categories":[],"keywords":[{"id":"100811","name":"Phd Defense"},{"id":"1808","name":"graduate students"}],"core_research_areas":[],"news_room_topics":[],"event_categories":[{"id":"1788","name":"Other\/Miscellaneous"}],"invited_audience":[{"id":"78771","name":"Public"}],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[],"email":[],"slides":[],"orientation":[],"userdata":""}}}