32 Quirós Araya, Gustavo 120000 121310 Publikationsserver der RWTH Aachen University Aachen English VIII, 101 S. NIPS is a virtual machine for the generation of state-transition systems of concurrent models, and is designed to serve as a foundation for the development of model checking applications. Like any explicit-state representation, the transition systems produced by NIPS suffer from the state-explosion problem, by which models have exponentially large state spaces. This work is dedicated to the reduction of the effect of the state-explosion problem in NIPS. State space reduction works by obtaining a reduced state-transition system from a model, which is equivalent to the original system under a given specification, or a given set of specifications. Model checking may be applied to the reduced system instead of to the original one, thus obtaining the same result in a more efficient manner. NIPS features a byte-code language for encoding concurrent models. High-level modeling languages may be compiled to this byte-code, and the interpretation of the byte-code by the machine results in the construction of the model’s state space representation. This architecture allows us to implement on-the-fly reductions merely by transforming the byte-code to another whose state-transition system is a reduced version of the original, and employing information gathered from static analysis of the byte-code in the process. Veröffentlicht auf dem Publikationsserver der RWTH Aachen University ; Aachen, Techn. Hochsch., Masterarbeit, 2006 ; PUB:(DE-HGF)19, ; 2, ; Programmanalyse Compiler Model Checking Zustandsraum Programmoptimierung Verteiltes System Master Thesis 2011 RWTH-CONV-144790 2011 https://publications.rwth-aachen.de/record/229985