This research first identifies some of the key concerns about the techniques and algorithms developed for distributed and parallel model checking; specifically, the inherent problem with load balancing and large queue sizes resultant in a static partition algorithm. This research then presents a load balancing algorithm to improve the run time performance in distributed model checking, reduce maximum queue size, and reduce the number of states expanded before error discovery. The load balancing algorithm is based on Generalized Dimension Exchange (GDE). This research presents an empirical analysis of the GDE based load balancing algorithm on three different supercomputing architectures---distributed memory clusters, Networks of Workstations (NOW) and shared memory machines. The analysis shows increased speedup, lower maximum queue sizes and fewer total states explored before error discovery on each of the architectures. Finally, this research presents a study of the communication overhead incurred by using the load balancing algorithm, which although significant, does not offset performance gains.
","abstract_html":"<p>This research first identifies some of the key concerns about the techniques and algorithms developed for distributed and parallel model checking; specifically, the inherent problem with load balancing and large queue sizes resultant in a static partition algorithm. This research then presents a load balancing algorithm to improve the run time performance in distributed model checking, reduce maximum queue size, and reduce the number of states expanded before error discovery. The load balancing algorithm is based on Generalized Dimension Exchange (GDE). This research presents an empirical analysis of the GDE based load balancing algorithm on three different supercomputing architectures---distributed memory clusters, Networks of Workstations (NOW) and shared memory machines. The analysis shows increased speedup, lower maximum queue sizes and fewer total states explored before error discovery on each of the architectures. Finally, this research presents a study of the communication overhead incurred by using the load balancing algorithm, which although significant, does not offset performance gains.</p>","abstract_has_math":false,"creators":["Kumar, Rahul"],"institution":"Brigham Young University - Provo","degree_name":"MS","degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":null,"date_issued":"","date_published":null,"updated_at":"2026-07-24T01:27:16Z","subjects":["load","balancing","computer","model","checking","verification","gde","speedup","error","states","queue","sizes","Computer Sciences"],"languages":["English"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://scholarsarchive.byu.edu/etd/44","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Kumar, Rahul"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2004-06-28T07:00:00Z"]},{"key":"dc:publisher","label":"Institution","values":["Brigham Young University - Provo"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["MS"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["load","balancing","computer","model","checking","verification","gde","speedup","error","states","queue","sizes","Computer Sciences"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["English"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://scholarsarchive.byu.edu/etd/44","https://scholarsarchive.byu.edu/context/etd/article/1043/viewcontent/ETD_CISOPTR_144.pdf"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Physical and Mathematical Sciences; Computer Science"]},{"key":"dc:description.abstract","label":"Abstract","values":["This research first identifies some of the key concerns about the techniques and algorithms developed for distributed and parallel model checking; specifically, the inherent problem with load balancing and large queue sizes resultant in a static partition algorithm. This research then presents a load balancing algorithm to improve the run time performance in distributed model checking, reduce maximum queue size, and reduce the number of states expanded before error discovery. The load balancing algorithm is based on Generalized Dimension Exchange (GDE). This research presents an empirical analysis of the GDE based load balancing algorithm on three different supercomputing architectures---distributed memory clusters, Networks of Workstations (NOW) and shared memory machines. The analysis shows increased speedup, lower maximum queue sizes and fewer total states explored before error discovery on each of the architectures. Finally, this research presents a study of the communication overhead incurred by using the load balancing algorithm, which although significant, does not offset performance gains.
"]},{"key":"dc:format","label":"Dc Format","values":["application:pdf"]},{"key":"dc:source","label":"Dc Source","values":["Brigham Young University - Provo"]},{"key":"dc:title","label":"Title","values":["Load Balancing Parallel Explicit State Model Checking"]}]}],"canonical_facts":{"dc:creator":["Kumar, Rahul"],"dc:date":["2004-06-28T07:00:00Z"],"dc:description":["Physical and Mathematical Sciences; Computer Science"],"dc:description.abstract":["This research first identifies some of the key concerns about the techniques and algorithms developed for distributed and parallel model checking; specifically, the inherent problem with load balancing and large queue sizes resultant in a static partition algorithm. This research then presents a load balancing algorithm to improve the run time performance in distributed model checking, reduce maximum queue size, and reduce the number of states expanded before error discovery. The load balancing algorithm is based on Generalized Dimension Exchange (GDE). This research presents an empirical analysis of the GDE based load balancing algorithm on three different supercomputing architectures---distributed memory clusters, Networks of Workstations (NOW) and shared memory machines. The analysis shows increased speedup, lower maximum queue sizes and fewer total states explored before error discovery on each of the architectures. Finally, this research presents a study of the communication overhead incurred by using the load balancing algorithm, which although significant, does not offset performance gains.
"],"dc:format":["application:pdf"],"dc:identifier":["https://scholarsarchive.byu.edu/etd/44","https://scholarsarchive.byu.edu/context/etd/article/1043/viewcontent/ETD_CISOPTR_144.pdf"],"dc:language":["English"],"dc:publisher":["Brigham Young University - Provo"],"dc:source":["Brigham Young University - Provo"],"dc:subject":["load","balancing","computer","model","checking","verification","gde","speedup","error","states","queue","sizes","Computer Sciences"],"dc:title":["Load Balancing Parallel Explicit State Model Checking"],"dc:type":["Thesis"],"thesis:degree_name":["MS"]},"updated_at":"2026-07-24T01:27:16Z"}