{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/102388"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/102388","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Statistical verification and differential privacy in cyber-physical systems","abstract":"This thesis studies the statistical verification and differential privacy in Cyber-Physical Systems. The first part focuses on the statistical verification of stochastic hybrid system, a class of formal models for Cyber-Physical Systems. Model reduction techniques are performed on both Discrete-Time and Continuous-Time Stochastic Hybrid Systems to reduce them to Discrete-Time Markov Chains and Continuous-Time Markov Chains, respectively; and statistical verification algorithms are proposed to verify Linear Inequality LTL and Metric Interval Temporal Logic on these discrete probabilistic models. In addition, the advantage of stratified sampling in verifying Probabilistic Computation Tree Logic on Labeled Discrete-Time Markov Chains is studied; this method can potentially be extended to other statistical verification algorithms to reduce computational costs. The second part focuses on the Differential Privacy in multi-agent systems that involve share information sharing to achieve overall control goals. A general formulation of the systems and a notion of Differential Privacy are proposed, and a trade-off between the Differential Privacy and the tracking performance of the systems is demonstrated. In addition, it is proved that there is a trade-off between Differential Privacy and the entropy of the unbiased estimator of the private data, and an optimal algorithm to achieve the best trade-off is given.","abstract_html":"This thesis studies the statistical verification and differential privacy in Cyber-Physical Systems. The first part focuses on the statistical verification of stochastic hybrid system, a class of formal models for Cyber-Physical Systems. Model reduction techniques are performed on both Discrete-Time and Continuous-Time Stochastic Hybrid Systems to reduce them to Discrete-Time Markov Chains and Continuous-Time Markov Chains, respectively; and statistical verification algorithms are proposed to verify Linear Inequality LTL and Metric Interval Temporal Logic on these discrete probabilistic models. In addition, the advantage of stratified sampling in verifying Probabilistic Computation Tree Logic on Labeled Discrete-Time Markov Chains is studied; this method can potentially be extended to other statistical verification algorithms to reduce computational costs. The second part focuses on the Differential Privacy in multi-agent systems that involve share information sharing to achieve overall control goals. A general formulation of the systems and a notion of Differential Privacy are proposed, and a trade-off between the Differential Privacy and the tracking performance of the systems is demonstrated. In addition, it is proved that there is a trade-off between Differential Privacy and the entropy of the unbiased estimator of the private data, and an optimal algorithm to achieve the best trade-off is given.","abstract_has_math":false,"creators":["Wang, Yu"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Mechanical Engineering","degree_department":null,"school":null,"contributors":["Dullerud, Geir E.","Mitra, Sayan","West, Matthew","Egerstedt, Magnus","Viswanathan, Mahesh"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019-02-06T19:32:38Z","date_published":"2019-02-06T19:32:38Z","updated_at":"2026-07-22T22:24:40Z","subjects":["Model Reduction","Markov Chains","Temporal Logic","Multi-Agent Systems","Laplace Mechanisms"],"languages":["en"],"rights":["Copyright 2018 Yu Wang"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/102388","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Dullerud, Geir E.","Mitra, Sayan","West, Matthew","Egerstedt, Magnus","Viswanathan, Mahesh"]},{"key":"dc:creator","label":"Author","values":["Wang, Yu"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2019-02-06T19:32:38Z","2018-08-21","2018-12"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Mechanical Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Model Reduction","Markov Chains","Temporal Logic","Multi-Agent Systems","Laplace Mechanisms"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2018 Yu Wang"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/102388"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This thesis studies the statistical verification and differential privacy in Cyber-Physical Systems. The first part focuses on the statistical verification of stochastic hybrid system, a class of formal models for Cyber-Physical Systems. Model reduction techniques are performed on both Discrete-Time and Continuous-Time Stochastic Hybrid Systems to reduce them to Discrete-Time Markov Chains and Continuous-Time Markov Chains, respectively; and statistical verification algorithms are proposed to verify Linear Inequality LTL and Metric Interval Temporal Logic on these discrete probabilistic models. In addition, the advantage of stratified sampling in verifying Probabilistic Computation Tree Logic on Labeled Discrete-Time Markov Chains is studied; this method can potentially be extended to other statistical verification algorithms to reduce computational costs. The second part focuses on the Differential Privacy in multi-agent systems that involve share information sharing to achieve overall control goals. A general formulation of the systems and a notion of Differential Privacy are proposed, and a trade-off between the Differential Privacy and the tracking performance of the systems is demonstrated. In addition, it is proved that there is a trade-off between Differential Privacy and the entropy of the unbiased estimator of the private data, and an optimal algorithm to achieve the best trade-off is given.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-02-05 without embargo terms","The student, Yu Wang, accepted the attached license on 2018-08-15 at 18:22.","The student, Yu Wang, submitted this Dissertation for approval on 2018-08-15 at 18:36.","This Dissertation was approved for publication on 2018-08-21 at 13:21.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12973 on 2019-02-05 at 11:07:36","Made available in DSpace on 2019-02-06T19:32:38Z (GMT). No. of bitstreams: 2 WANG-DISSERTATION-2018.pdf: 784732 bytes, checksum: 64af8178e62cec2f6110a36a86dc6f66 (MD5) LICENSE.txt: 4204 bytes, checksum: 6ed8c29e9193693e607d467f431a818c (MD5) Previous issue date: 2018-08-21"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Statistical verification and differential privacy in cyber-physical systems"]}]}],"canonical_facts":{"dc:contributor":["Dullerud, Geir E.","Mitra, Sayan","West, Matthew","Egerstedt, Magnus","Viswanathan, Mahesh"],"dc:creator":["Wang, Yu"],"dc:date":["2019-02-06T19:32:38Z","2018-08-21","2018-12"],"dc:description":["This thesis studies the statistical verification and differential privacy in Cyber-Physical Systems. The first part focuses on the statistical verification of stochastic hybrid system, a class of formal models for Cyber-Physical Systems. Model reduction techniques are performed on both Discrete-Time and Continuous-Time Stochastic Hybrid Systems to reduce them to Discrete-Time Markov Chains and Continuous-Time Markov Chains, respectively; and statistical verification algorithms are proposed to verify Linear Inequality LTL and Metric Interval Temporal Logic on these discrete probabilistic models. In addition, the advantage of stratified sampling in verifying Probabilistic Computation Tree Logic on Labeled Discrete-Time Markov Chains is studied; this method can potentially be extended to other statistical verification algorithms to reduce computational costs. The second part focuses on the Differential Privacy in multi-agent systems that involve share information sharing to achieve overall control goals. A general formulation of the systems and a notion of Differential Privacy are proposed, and a trade-off between the Differential Privacy and the tracking performance of the systems is demonstrated. In addition, it is proved that there is a trade-off between Differential Privacy and the entropy of the unbiased estimator of the private data, and an optimal algorithm to achieve the best trade-off is given.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-02-05 without embargo terms","The student, Yu Wang, accepted the attached license on 2018-08-15 at 18:22.","The student, Yu Wang, submitted this Dissertation for approval on 2018-08-15 at 18:36.","This Dissertation was approved for publication on 2018-08-21 at 13:21.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12973 on 2019-02-05 at 11:07:36","Made available in DSpace on 2019-02-06T19:32:38Z (GMT). No. of bitstreams: 2 WANG-DISSERTATION-2018.pdf: 784732 bytes, checksum: 64af8178e62cec2f6110a36a86dc6f66 (MD5) LICENSE.txt: 4204 bytes, checksum: 6ed8c29e9193693e607d467f431a818c (MD5) Previous issue date: 2018-08-21"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/102388"],"dc:language":["en"],"dc:rights":["Copyright 2018 Yu Wang"],"dc:subject":["Model Reduction","Markov Chains","Temporal Logic","Multi-Agent Systems","Laplace Mechanisms"],"dc:title":["Statistical verification and differential privacy in cyber-physical systems"],"dc:type":["text"],"thesis:degree_discipline":["Mechanical Engineering"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:40Z"}