Iterative Variable Reordering: Taming Huge System Families

Clemens DubslaffClemens Dubslaff, Andrey MorozovAndrey Morozov, Christel BaierChristel Baier, Klaus JanschekKlaus Janschek

DOI Link

Clemens Dubslaff, Andrey Morozov, Christel Baier, Klaus Janschek
Iterative Variable Reordering: Taming Huge System Families
Electronic Proceedings in Theoretical Computer Science, 316:121--133, 2020

Details
Bibtex

KurzfassungAbstract
For the verification of systems using model-checking techniques, symbolic representations based on binary decision diagrams (BDDs) often help to tackle the well-known state-space explosion problem. Symbolic BDD-based representations have been also shown to be successful for the analysis of families of systems that arise, e.g., through configurable parameters or following the feature-oriented modeling approach. The state space of such system families face an additional exponential blowup in the number of parameters or features. It is well known that the order of variables in ordered BDDs is crucial for the size of the model representation. Especially for automatically generated models from real-world systems, family models might even be not constructible due to bad variable orders. In this paper we describe a technique, called iterative variable reordering, that can enable the construction of large-scale family models. We exemplify feasibility of our approach by means of an aircraft velocity control system with redundancy mechanisms modeled in the input language of the probabilistic model checker PRISM. We show that standard reordering and dynamic reordering techniques fail to construct the family model due to memory and time constraints, respectively, while the new iterative approach succeeds to generate a symbolic family model.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{DMBJ2020,
  author    = {Clemens Dubslaff and Andrey Morozov and Christel Baier and Klaus
               Janschek},
  title     = {Iterative Variable Reordering: Taming Huge System Families},
  journal   = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {316},
  publisher = {Open Publishing Association},
  year      = {2020},
  pages     = {121--133},
  doi       = {10.4204/eptcs.316.5}
}