h1

%0 Thesis
%A Sharma, Arpit
%T Reduction Techniques for Nondeterministic and Probabilistic Systems
%V 2015,3
%N AIB-2015-03
%I RWTH Aachen University
%V Dissertation
%C Aachen
%M RWTH-2015-00556
%M AIB-2015-03
%B Aachener Informatik-Berichte
%P XIV, 175 S.
%D 2015
%Z Zugl.: Aachen, Techn. Hochsch., Diss., 2015
%X Model checking is an automated verification method guaranteeing that a mathematical model of a system satisfies a formally described property. It can be used to assess both qualitative and quantitative properties of complex software and hardware systems. Model checking suffers from the well-known state space explosion problem where the number of states grows exponentially in the number of program variables, channels and parallel components. Reduction techniques can be used to shrink the state space of system models by hiding redundant information and removing irrelevant details. The reduced state space can then be used for analysis provided it preserves a rich class of properties of interest. This thesis presents reduction techniques for a wide range of nondeterministic and probabilistic models. Our reduction techniques are based on the notions of equivalence relations and layering.Equivalence relations reduce the state space of system models, by aggregating equivalent states into a single state. The reduced state space obtained under an equivalence relation, is called a quotient system. An example equivalence relation that is widely used to reduce the state space of nondeterministic and probabilistic models is bisimulation. On the other hand, layering involves carrying out structural transformations for the systems that are modeled as a network of system models, e.g., distributed systems. As a result of these structural transformations, the new state space obtained is smaller than the original non-layered one. The first part of this thesis focuses on developing new equivalence relations for nondeterministic and Markovian models. For each of these relations, we define a quotient system, investigate its relationship with bisimulation and prove that it preserves interesting linear-time properties. In the second part of this thesis we focus on layering based state space reduction for more expressive specification formalisms that support a stepwise refinement methodology. We develop a framework of layering for modal transition systems and probabilistic versions thereof. This involves a layered composition operator, formulating communication closed layer (CCL) laws and defining a partial order (po) equivalence between modal transition systems. We also prove that the reduced model obtained as a result of applying layered transformation preserves reachability properties. As a result, reachability properties can be checked on the layered, typically smaller, model.To summarize, this thesis presents the theoretical underpinnings of a number of novel reduction techniques for nondeterministic and probabilistic systems.
%F PUB:(DE-HGF)11 ; PUB:(DE-HGF)29 ; PUB:(DE-HGF)3
%9 Dissertation / PhD ThesisReportBook
%U https://publications.rwth-aachen.de/record/462319