{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/81718"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/81718","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Probabilistic Modeling and Verification of Large Scale Systems","abstract":"Many large scale systems have a stochastic behavior. Such stochastic behavior is the result of the randomness in the systems' operating environments. It can also be the result of the use of randomized protocols that are used to reduce the need for costly synchronization. We abstract a system state as a probability mass function (pmf); a pmf is succinct in representation and is informative enough to describe many useful aggregate behaviors of the system. We model the dynamics of the state transitions as a Discrete Time Markov Chain (DTMC) and develop an on-line model estimation method as well as a goodness of fit test that statistically validates the model. We develop a probabilistic temporal logic called iLTL in order to specify aggregate behaviors of large scale systems. Many important performance criteria on DTMC models can be accurately expressed in iLTL. For the iLTL specifications, performance evaluation is systematically performed through a process of model checking. If a performance criterion is not satisfiable, the model checker returns a sequence of computations that violates the specification in order to help users fix the problem. We show the usefulness of our methodology through an experiment with a wireless sensor network of 90 nodes.","abstract_html":"Many large scale systems have a stochastic behavior. Such stochastic behavior is the result of the randomness in the systems' operating environments. It can also be the result of the use of randomized protocols that are used to reduce the need for costly synchronization. We abstract a system state as a probability mass function (pmf); a pmf is succinct in representation and is informative enough to describe many useful aggregate behaviors of the system. We model the dynamics of the state transitions as a Discrete Time Markov Chain (DTMC) and develop an on-line model estimation method as well as a goodness of fit test that statistically validates the model. We develop a probabilistic temporal logic called iLTL in order to specify aggregate behaviors of large scale systems. Many important performance criteria on DTMC models can be accurately expressed in iLTL. For the iLTL specifications, performance evaluation is systematically performed through a process of model checking. If a performance criterion is not satisfiable, the model checker returns a sequence of computations that violates the specification in order to help users fix the problem. We show the usefulness of our methodology through an experiment with a wireless sensor network of 90 nodes.","abstract_has_math":false,"creators":["Kwon, YoungMin"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Agha, Gul A."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2015,"date_issued":"2015-09-25T20:20:08Z","date_published":"2015-09-25T20:20:08Z","updated_at":"2026-07-22T22:26:16Z","subjects":["Computer Science"],"languages":["eng"],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["(MiAaPQ)AAI3223636"],"render_values":[{"text":"(MiAaPQ)AAI3223636","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/81718","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Agha, Gul A."]},{"key":"dc:creator","label":"Author","values":["Kwon, YoungMin"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2015-09-25T20:20:08Z","10000-01-01","2006"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"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":["Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/81718","(MiAaPQ)AAI3223636"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Many large scale systems have a stochastic behavior. Such stochastic behavior is the result of the randomness in the systems' operating environments. It can also be the result of the use of randomized protocols that are used to reduce the need for costly synchronization. We abstract a system state as a probability mass function (pmf); a pmf is succinct in representation and is informative enough to describe many useful aggregate behaviors of the system. We model the dynamics of the state transitions as a Discrete Time Markov Chain (DTMC) and develop an on-line model estimation method as well as a goodness of fit test that statistically validates the model. We develop a probabilistic temporal logic called iLTL in order to specify aggregate behaviors of large scale systems. Many important performance criteria on DTMC models can be accurately expressed in iLTL. For the iLTL specifications, performance evaluation is systematically performed through a process of model checking. If a performance criterion is not satisfiable, the model checker returns a sequence of computations that violates the specification in order to help users fix the problem. We show the usefulness of our methodology through an experiment with a wireless sensor network of 90 nodes.","Made available in DSpace on 2015-09-25T20:20:08Z (GMT). No. of bitstreams: 2 license.txt: 4848 bytes, checksum: 96035ab3f5e1c23cc7138a224ce498bd (MD5) 3223636.pdf: 2507424 bytes, checksum: 9da8e68248d3aded3ffede18d260560b (MD5) Previous issue date: 2006","Embargo set by: Seth Robbins for item 82999 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","U of I Only","99 p.","Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 2006."]},{"key":"dc:title","label":"Title","values":["Probabilistic Modeling and Verification of Large Scale Systems"]}]}],"canonical_facts":{"dc:contributor":["Agha, Gul A."],"dc:creator":["Kwon, YoungMin"],"dc:date":["2015-09-25T20:20:08Z","10000-01-01","2006"],"dc:description":["Many large scale systems have a stochastic behavior. Such stochastic behavior is the result of the randomness in the systems' operating environments. It can also be the result of the use of randomized protocols that are used to reduce the need for costly synchronization. We abstract a system state as a probability mass function (pmf); a pmf is succinct in representation and is informative enough to describe many useful aggregate behaviors of the system. We model the dynamics of the state transitions as a Discrete Time Markov Chain (DTMC) and develop an on-line model estimation method as well as a goodness of fit test that statistically validates the model. We develop a probabilistic temporal logic called iLTL in order to specify aggregate behaviors of large scale systems. Many important performance criteria on DTMC models can be accurately expressed in iLTL. For the iLTL specifications, performance evaluation is systematically performed through a process of model checking. If a performance criterion is not satisfiable, the model checker returns a sequence of computations that violates the specification in order to help users fix the problem. We show the usefulness of our methodology through an experiment with a wireless sensor network of 90 nodes.","Made available in DSpace on 2015-09-25T20:20:08Z (GMT). No. of bitstreams: 2 license.txt: 4848 bytes, checksum: 96035ab3f5e1c23cc7138a224ce498bd (MD5) 3223636.pdf: 2507424 bytes, checksum: 9da8e68248d3aded3ffede18d260560b (MD5) Previous issue date: 2006","Embargo set by: Seth Robbins for item 82999 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","U of I Only","99 p.","Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 2006."],"dc:identifier":["http://hdl.handle.net/2142/81718","(MiAaPQ)AAI3223636"],"dc:language":["eng"],"dc:subject":["Computer Science"],"dc:title":["Probabilistic Modeling and Verification of Large Scale Systems"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:26:16Z"}