{"id":{"repo_id":"aachen","oai_identifier":"oai:publications.rwth-aachen.de:61857"},"canonical_url":"https://search.dev.ndltd.org/etd/aachen/oai:publications.rwth-aachen.de:61857","repository":{"repo_id":"aachen","name":"RWTH Aachen University","base_url":"https://publications.rwth-aachen.de/oai2d"},"display":{"title":"Parallel algorithms for verification of large systems","abstract":"The model-checking problem is the question whether a given system model satisfies a property. The property is usually given as formula of a temporal logic, and the system model as labelled transition system. However, the well-known state-space explosion effect is responsible for yielding transition systems of exponential size when compared to their description, and common sequential algorithms often are not capable to solve the model-checking problem with resources available on a single computer. In this thesis, we develop parallel and, in particular, distributed algorithms which exploit the combined resources of a network of commodity workstations to solve problem instances which are beyond the capabilities of today’s sequential algorithms. In a second part, we investigate ways to efficiently generate (low-level) transition systems suitable for many verification tools from compact high-level descriptions of the input model. We propose a virtual-machine based approach, which uses an intermediate format to break the translation from high-level to low-level representations of a model into two steps. This well-known compiler technique simplifies the translation and still is very fast in practice.","abstract_html":"The model-checking problem is the question whether a given system model satisfies a property. The property is usually given as formula of a temporal logic, and the system model as labelled transition system. However, the well-known state-space explosion effect is responsible for yielding transition systems of exponential size when compared to their description, and common sequential algorithms often are not capable to solve the model-checking problem with resources available on a single computer. In this thesis, we develop parallel and, in particular, distributed algorithms which exploit the combined resources of a network of commodity workstations to solve problem instances which are beyond the capabilities of today’s sequential algorithms. In a second part, we investigate ways to efficiently generate (low-level) transition systems suitable for many verification tools from compact high-level descriptions of the input model. We propose a virtual-machine based approach, which uses an intermediate format to break the translation from high-level to low-level representations of a model into two steps. This well-known compiler technique simplifies the translation and still is very fast in practice.","abstract_has_math":false,"creators":["Weber, Michael"],"institution":"RWTH, Department of Computer Science","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Indermark, Klaus"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2006,"date_issued":"2006","date_published":"2006","updated_at":"2026-07-30T19:43:19Z","subjects":["info:eu-repo/classification/ddc/004","Informatik","Verifikation","paralleler Algorithmus","endlicher Zustandsraum","mu-Kalkül","Model-Checking-Spiele","Zustandsraumgenerierung","mu-calculus","model-checking games","state space generation","model checking"],"languages":["eng"],"rights":["info:eu-repo/semantics/openAccess"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123475%22"],"render_values":[{"text":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123475%22","href":"https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123475%22","code":true}]}]},"links":{"outbound_url":"https://publications.rwth-aachen.de/record/61857","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Indermark, Klaus"]},{"key":"dc:creator","label":"Author","values":["Weber, Michael"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:coverage","label":"Dc Coverage","values":["DE"]},{"key":"dc:date","label":"Dc Date","values":["2006"]},{"key":"dc:publisher","label":"Institution","values":["RWTH, Department of Computer Science"]},{"key":"dc:relation","label":"Dc Relation","values":["info:eu-repo/semantics/altIdentifier/issn/0935-3232","info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-17709"]},{"key":"dc:type","label":"Dc Type","values":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["info:eu-repo/classification/ddc/004","Informatik","Verifikation","paralleler Algorithmus","endlicher Zustandsraum","mu-Kalkül","Model-Checking-Spiele","Zustandsraumgenerierung","mu-calculus","model-checking games","state space generation","model checking"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["info:eu-repo/semantics/openAccess"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://publications.rwth-aachen.de/record/61857","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123475%22"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["The model-checking problem is the question whether a given system model satisfies a property. The property is usually given as formula of a temporal logic, and the system model as labelled transition system. However, the well-known state-space explosion effect is responsible for yielding transition systems of exponential size when compared to their description, and common sequential algorithms often are not capable to solve the model-checking problem with resources available on a single computer. In this thesis, we develop parallel and, in particular, distributed algorithms which exploit the combined resources of a network of commodity workstations to solve problem instances which are beyond the capabilities of today’s sequential algorithms. In a second part, we investigate ways to efficiently generate (low-level) transition systems suitable for many verification tools from compact high-level descriptions of the input model. We propose a virtual-machine based approach, which uses an intermediate format to break the translation from high-level to low-level representations of a model into two steps. This well-known compiler technique simplifies the translation and still is very fast in practice."]},{"key":"dc:source","label":"Dc Source","values":["Aachen : RWTH, Department of Computer Science, Aachener Informatik-Berichte 2006,2 II, 133 S. : graph. Darst. (2006). = Aachen, Techn. Hochsch., Diss., 2006"]},{"key":"dc:title","label":"Title","values":["Parallel algorithms for verification of large systems"]}]}],"canonical_facts":{"dc:contributor":["Indermark, Klaus"],"dc:coverage":["DE"],"dc:creator":["Weber, Michael"],"dc:date":["2006"],"dc:description":["The model-checking problem is the question whether a given system model satisfies a property. The property is usually given as formula of a temporal logic, and the system model as labelled transition system. However, the well-known state-space explosion effect is responsible for yielding transition systems of exponential size when compared to their description, and common sequential algorithms often are not capable to solve the model-checking problem with resources available on a single computer. In this thesis, we develop parallel and, in particular, distributed algorithms which exploit the combined resources of a network of commodity workstations to solve problem instances which are beyond the capabilities of today’s sequential algorithms. In a second part, we investigate ways to efficiently generate (low-level) transition systems suitable for many verification tools from compact high-level descriptions of the input model. We propose a virtual-machine based approach, which uses an intermediate format to break the translation from high-level to low-level representations of a model into two steps. This well-known compiler technique simplifies the translation and still is very fast in practice."],"dc:identifier":["https://publications.rwth-aachen.de/record/61857","https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-123475%22"],"dc:language":["eng"],"dc:publisher":["RWTH, Department of Computer Science"],"dc:relation":["info:eu-repo/semantics/altIdentifier/issn/0935-3232","info:eu-repo/semantics/altIdentifier/urn/urn:nbn:de:hbz:82-opus-17709"],"dc:rights":["info:eu-repo/semantics/openAccess"],"dc:source":["Aachen : RWTH, Department of Computer Science, Aachener Informatik-Berichte 2006,2 II, 133 S. : graph. Darst. (2006). = Aachen, Techn. Hochsch., Diss., 2006"],"dc:subject":["info:eu-repo/classification/ddc/004","Informatik","Verifikation","paralleler Algorithmus","endlicher Zustandsraum","mu-Kalkül","Model-Checking-Spiele","Zustandsraumgenerierung","mu-calculus","model-checking games","state space generation","model checking"],"dc:title":["Parallel algorithms for verification of large systems"],"dc:type":["info:eu-repo/semantics/doctoralThesis","info:eu-repo/semantics/publishedVersion"]},"updated_at":"2026-07-30T19:43:19Z"}