@misc(aircraft,
 title        = {Verify Model Using Simulink Control Design and Simulink Verification Blocks (accessed 19/02/2019)},
 howpublished = {{\relax\fontsize {8}{9.5}\selectfont\url {https://mathworks.com/help/slcontrol/ug/model-verification-using-simulink-control-design-and-simulink-verification-blocks-.html}}},
)
@article(Akers78,
 author       = {S. B. Akers},
 year         = {1978},
 title        = {Binary Decision Diagrams},
 journal      = {IEEE Transactions Computers},
 volume       = {27},
 number       = {6},
 pages        = {509--516},
 doi          = {10.1109/TC.1978.1675141},
)
@article(Hachtel-Som-et-al-ADD97,
 author       = {R. I. Bahar and E. A. Frohm and C. M. Gaona and G. D. Hachtel and E. Macii and A. Pardo and F. Somenzi},
 year         = {1997},
 title        = {Algebraic Decision Diagrams and Their Applications},
 journal      = {Formal Methods in System Design},
 volume       = {10},
 number       = {2/3},
 pages        = {171--206},
 doi          = {10.1023/A:1008699807402},
)
@article(BD18,
 author       = {C. Baier and C. Dubslaff},
 year         = {2018},
 title        = {From Verification to Synthesis under Cost-Utility Constraints},
 journal      = {ACM {SIGLOG} News},
 volume       = {5},
 number       = {4},
 pages        = {26--46},
 doi          = {10.1145/3292048.3292052},
)
@book(BK08,
 author       = {C. Baier and J.-P. Katoen},
 year         = {2008},
 title        = {Principles of Model Checking},
 publisher    = {MIT Press},
)
@article(Bryant86,
 author       = {R. E. Bryant},
 year         = {1986},
 title        = {{Graph-Based Algorithms for Boolean Function Manipulation}},
 journal      = {IEEE Transactions on Computers},
 volume       = {35},
 pages        = {677--691},
 doi          = {10.1109/TC.1986.1676819},
)
@article(BCMcMDH92,
 author       = {J. R. Burch and E. M. Clarke and K. L. McMillan and D. L. Dill and L. J. Hwang},
 year         = {1992},
 title        = {Symbolic Model Checking: 10$^{20}$ States and Beyond},
 journal      = {Inform. and Comp.},
 volume       = {98},
 number       = {2},
 pages        = {142--170},
 doi          = {10.1016/0890-5401(92)90017-A},
)
@article(CDKB18,
 author       = {P. Chrszon and C. Dubslaff and S. Kl{\"{u}}ppelholz and C. Baier},
 year         = {2018},
 title        = {ProFeat: feature-oriented engineering for family-based probabilistic model checking},
 journal      = {Formal Aspects of Computing},
 volume       = {30},
 number       = {1},
 pages        = {45--75},
 doi          = {10.1007/s00165-017-0432-4},
)
@book(CGP00,
 author       = {E. Clarke and O. Grumberg and D. Peled},
 year         = {2000},
 title        = {Model Checking},
 publisher    = {MIT Press},
)
@inproceedings(CFMcGMcMY93,
 author       = {E. M. Clarke and M. Fujita and P. C. McGeers and K. L. McMillan and J. C.{-}Y. Yang and X.{-}J. Zhao},
 year         = {1993},
 title        = {Multi-terminal binary decision diagrams: An efficient data structure for matrix representation},
 booktitle    = {Proc. International Workshop on Logic \& Synthesis},
 doi          = {10.1023/A:1008647823331},
)
@inproceedings(ClassenHSL11,
 author       = {A. Classen and P. Heymans and P.{-}Y. Schobbens and A. Legay},
 year         = {2011},
 title        = {Symbolic model checking of software product lines},
 booktitle    = {Proceedings of the 33rd International Conference on Software Engineering, {ICSE} 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011},
 pages        = {321--330},
 doi          = {10.1145/1985793.1985838},
)
@inproceedings(DJKV-CAV17,
 author       = {C. Dehnert and S. Junges and J.{-}P. Katoen and M. Volk},
 year         = {2017},
 title        = {A {Storm} is Coming: A Modern Probabilistic Model Checker},
 booktitle    = {29th Int.~Conf. on Computer Aided Verification (CAV)},
 series       = {LNCS},
 volume       = {10427},
 publisher    = {Springer},
 pages        = {592--600},
 doi          = {10.1007/978-3-319-63390-9\_31},
)
@article(Dijkstra1975,
 author       = {E. W. Dijkstra},
 year         = {1975},
 title        = {Guarded Commands, Nondeterminacy and Formal Derivation of Programs},
 journal      = {Commun. {ACM}},
 volume       = {18},
 number       = {8},
 pages        = {453--457},
 doi          = {10.1145/360933.360975},
)
@article(DBK15,
 author       = {C. Dubslaff and C. Baier and S. Kl{\"{u}}ppelholz},
 year         = {2015},
 title        = {Probabilistic Model Checking for Feature-Oriented Systems},
 journal      = {Transactions on Aspect-Oriented Software Development},
 volume       = {12},
 pages        = {180--220},
 doi          = {10.1007/978-3-662-46734-3\_5},
)
@inproceedings(DDMBJ19,
 author       = {C. Dubslaff and K. Ding and A. Morozov and C. Baier and K. Janschek},
 year         = {2019},
 title        = {Breaking the Limits of Redundancy Systems Analysis},
 booktitle    = {Proceedings of the 29th European Safety and Reliability Conference},
 publisher    = {Research Publishing, Singapore},
 pages        = {2317--2325},
 doi          = {10.3850/978-981-11-2724-3\_0618-cd},
)
@article(DubMorBai20,
 author       = {C. Dubslaff and A. Morozov and C. Baier and K. Janschek},
 year         = {2020},
 title        = {Reduction Methods on Probabilistic Control-flow Programs for Reliability Analysis},
 journal      = {CoRR},
 volume       = {abs/2004.06637},
 url          = {https://arxiv.org/abs/2004.06637},
)
@inproceedings(FelYorBra93a,
 author       = {E. {Felt} and G. {York} and R. {Brayton} and {Sangiovanni-Vincentelli}, A.},
 year         = {1993},
 title        = {Dynamic variable reordering for BDD minimization},
 booktitle    = {Proceedings of EURO-DAC 93 and EURO-VHDL 93- European Design Automation Conference},
 pages        = {130--135},
 doi          = {10.1109/EURDAC.1993.410627},
)
@article(mtbdds,
 author       = {M. Fujita and P.C. McGeer and J.C.-Y. Yang},
 year         = {1997},
 title        = {Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation},
 journal      = {Formal Methods in System Design},
 volume       = {10},
 number       = {2-3},
 pages        = {149--169},
 doi          = {10.1023/A:1008647823331},
)
@article(GarSer06a,
 author       = {H. Garavel and W. Serwe},
 year         = {2006},
 title        = {State space reduction for process algebra specifications},
 journal      = {Theoretical Computer Science},
 volume       = {351},
 number       = {2},
 pages        = {131 -- 145},
 doi          = {10.1016/j.tcs.2005.09.064},
 note         = {Algebraic Methodology and Software Technology},
)
@book(GJ79,
 author       = {M. R. Garey and D. S. Johnson},
 year         = {1979},
 title        = {Computers and Intractability: A Guide to the Theory of NP-Completeness},
 publisher    = {W. H. Freeman \& Company},
)
@article(KBCDDKMM18,
 author       = {J. Klein and C. Baier and P. Chrszon and M. Daum and C. Dubslaff and S. Kl{\"u}ppelholz and S. M{\"a}rcker and D. M{\"u}ller},
 year         = {2018},
 title        = {Advances in probabilistic model checking with {PRISM}: variable reordering, quantiles and weak deterministic {B\"uchi} automata},
 journal      = {Intern. Journal on Software Tools for Technology Transfer},
 volume       = {20},
 number       = {2},
 pages        = {179--194},
 doi          = {10.1007/s10009-017-0456-3},
)
@inproceedings(KNP11,
 author       = {M. Kwiatkowska and G. Norman and D. Parker},
 year         = {2011},
 title        = {{PRISM} 4.0: Verification of Probabilistic Real-time Systems},
 editor       = {G. Gopalakrishnan and S. Qadeer},
 booktitle    = {Proc. 23rd International Conference on Computer Aided Verification (CAV'11)},
 series       = {LNCS},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {585--591},
 doi          = {10.1007/978-3-642-22110-1\_47},
)
@article(Lee59,
 author       = {C. Y. Lee},
 year         = {1959},
 title        = {Representation of Switching Circuits by Binary-Decision Programs},
 journal      = {Bell System Technical Journal},
 volume       = {38},
 number       = {4},
 pages        = {985--999},
 doi          = {10.1002/j.1538-7305.1959.tb01585.x},
)
@inproceedings(MalWanBraSan1988,
 author       = {S. Malik and A.R. Wang and R.K. Brayton and Sangiovanni-Vincentelli, A.},
 year         = {1988},
 title        = {Logic verification using binary decision diagrams in a logic synthesis environment},
 booktitle    = {Computer-Aided Design, 1988. ICCAD-88. Digest of Technical Papers., IEEE International Conference on},
 pages        = {6--9},
 doi          = {10.1109/ICCAD.1988.122451},
)
@book(McMillan,
 author       = {K. L. McMillan},
 year         = {1993},
 title        = {Symbolic Model Checking},
 publisher    = {Kluwer},
 doi          = {10.1007/978-1-4615-3190-6},
)
@inproceedings(MorDinSte19a,
 author       = {A. Morozov and K. Ding and M. Steurer and K. Janschek},
 year         = {2019},
 title        = {OpenErrorPro: {A} New Tool for Stochastic Model-Based Reliability and Resilience Analysis},
 booktitle    = {30th {IEEE} International Symposium on Software Reliability Engineering, {ISSRE} 2019, Berlin, Germany, October 28-31, 2019},
 pages        = {303--312},
 doi          = {10.1109/ISSRE.2019.00038},
)
@inproceedings(MorJanKru16a,
 author       = {A. Morozov and K. Janschek and T. Kr\"{u}ger and A. Schiele},
 year         = {2016},
 title        = {Stochastic Error Propagation Analysis of Model-Driven Space Robotic Software Implemented in Simulink},
 booktitle    = {Proceedings of the 3rd Workshop on Model-Driven Robot Software Engineering},
 series       = {MORSE '16},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {24--31},
 doi          = {10.1145/3022099.3022103},
)
@inproceedings(Panda95,
 author       = {S. Panda and F. Somenzi},
 year         = {1995},
 title        = {Who Are the Variables in Your Neighborhood},
 booktitle    = {Proc. Computer-Aided Design (ICCAD'95)},
 publisher    = {IEEE},
 pages        = {74--77},
 doi          = {10.5555/224841.224862},
)
@book(Puterman:book,
 author       = {M. L. Puterman},
 year         = {1994},
 title        = {{Markov} Decision Processes},
 publisher    = {Wiley},
 doi          = {10.1002/9780470316887},
)
@inproceedings(Rud1993,
 author       = {R. Rudell},
 year         = {1993},
 title        = {Dynamic variable ordering for ordered binary decision diagrams},
 booktitle    = {IEEE/ACM International Conference on Computer-Aided Design (ICCAD-93).},
 pages        = {42--47},
 doi          = {10.1109/ICCAD.1993.580029},
)
@inproceedings(Somenzi99binarydecision,
 author       = {F. Somenzi},
 year         = {1999},
 title        = {Binary Decision Diagrams},
 booktitle    = {Calculational System Design, volume 173 of NATO Science Series F: Computer and Systems Sciences},
 publisher    = {IOS Press},
 pages        = {303--366},
)
@manual(Simulink,
 author       = {{The MathWorks Inc.}},
 year         = {2018},
 title        = {MATLAB and Statistics Toolbox Release 2018b},
 address      = {Natick, Massachusetts, United States},
)
@article(Thum14,
 author       = {T. Th\"{u}m and S. Apel and C. K\"{a}stner and I. Schaefer and G. Saake},
 year         = {2014},
 title        = {A Classification and Survey of Analysis Strategies for Software Product Lines},
 journal      = {ACM Comput. Surv.},
 volume       = {47},
 pages        = {1--45},
 doi          = {10.1145/2580950},
)
@book(Wegener00,
 author       = {I. Wegener},
 year         = {2000},
 title        = {{Branching Programs and Binary Decision Diagrams: Theory and Applications}},
 publisher    = {Monographs on Discrete Mathematics and Applications. SIAM},
 doi          = {10.1137/1.9780898719789},
)