text:
@inproceedings{CH11,
  author    = {Krishnendu Chatterjee and
               Monika Henzinger},
  title     = {Faster and Dynamic Algorithms for Maximal End-Component
               Decomposition and Related Graph Problems in Probabilistic
               Verification},
  booktitle = {SODA},
  year      = {2011},
  pages     = {1318-1336}
}

@inproceedings{CT12,
  author    = {Krishnendu Chatterjee and
               Mathieu Tracol},
  title     = {Decidable Problems for Probabilistic Automata on Infinite
               Words},
  booktitle = {LICS},
  year      = {2012},
  pages     = {185-194}
}

@inproceedings{BBG08,
  author    = {C. Baier and N. Bertrand and M. Gr{\"o}{\ss}er},
  title     = {On Decision Problems for Probabilistic {B}{\"u}chi Automata},
  booktitle = {FoSSaCS},
  year      = {2008},
  pages     = {287--301},
  publisher = {Springer},
  series    = {LNCS 4962}
}

@inproceedings{BGG09,
  author    = "N. Bertrand and B. Genest and H. Gimbert",
  title     = "Qualitative Determinacy and Decidability of Stochastic Games with Signals",
  booktitle = "Proc. of LICS",
  year      = "2009",
  pages     = "319-328",
  publisher = "IEEE Computer Society"
}

@inproceedings{CDHR06,
        author="K.~Chatterjee and  L. Doyen and T.~A.~Henzinger and J.F. Raskin",
        title="Algorithms for omega-regular games with Imperfect Information",
        booktitle="CSL'06",
	publisher="LNCS 4207, Springer",
	pages="287--302",
        year="2006"
        }

@phdthesis{ChaThesis,
        author="K. Chatterjee",
        title="Stochastic $\omega$-Regular Games",
        school="UC Berkeley",
        year="2007"
        }

@inproceedings{CJH03,
  author = "K.~Chatterjee  and M.~Jurdzi{\'n}ski and T.~A.~Henzinger",
  title =  "Simple Stochastic Parity Games",
  booktitle = 	 {CSL'03},
  pages = 	 {100--113},
  year = 	 {2003},
  volume = 	 {2803},
  series = 	 {LNCS},
  publisher = {Springer},
}

@article{CHJS11,
  author    = {Krishnendu Chatterjee and
               Monika Henzinger and
               Manas Joglekar and
               Nisarg Shah},
  title     = {Symbolic algorithms for qualitative analysis of {M}arkov decision
               processes with {B}{\"u}chi objectives},
  journal   = {Formal Methods in System Design},
  volume    = {42},
  number    = {3},
  year      = {2013},
  pages     = {301-327}
}

@inproceedings{CDNV14,
  author    = {Krishnendu Chatterjee and
               Laurent Doyen and
               Sumit Nain and
               Moshe Y. Vardi},
  title     = {The Complexity of Partial-Observation Stochastic Parity
               Games with Finite-Memory Strategies},
  booktitle = {FoSSaCS},
  year      = {2014},
  pages     = {242-257}
}

@article{CDH13,
  author    = {Krishnendu Chatterjee and
               Laurent Doyen and
               Thomas A. Henzinger},
  title     = {A survey of partial-observation stochastic parity games},
  journal   = {Formal Methods in System Design},
  volume    = {43},
  number    = {2},
  year      = {2013},
  pages     = {268-284}
}

@inproceedings{CH12,
  author    = {Krishnendu Chatterjee and
               Monika Henzinger},
  title     = {An {{\it O}}({\it n}$^{\mbox{2}}$) time algorithm for alternating
	  {B}{\"u}chi games},
  booktitle = {SODA},
  year      = {2012},
  pages     = {1386-1399}
}

@inproceedings{NV13,
  author    = {S. Nain and
               M. Y. Vardi},
  title     = {Solving Partial-Information Stochastic Parity Games},
  booktitle = {LICS},
  year      = {2013},
  pages     = {341-348}
}

@inproceedings{CDH10a,
  author    = {Chatterjee, K. and Doyen, L. and Henzinger, T.~A.},
  title     = {Qualitative Analysis of Partially-observable {M}arkov Decision Processes},
  booktitle = {Proc. of MFCS},
  publisher = {Springer},
  series    = {LNCS 6281},
  year      = {2010},
  pages     = {258-269},
  isbn      = {978-3-642-15154-5}
}

@inproceedings{CCT13,
  author    = {K. Chatterjee and M. Chmelik and M. Tracol},
  title     = {What is Decidable about Partially Observable {M}arkov Decision Processes with omega-Regular Objectives},
  booktitle = {Proceedings of CSL 2013: Computer Science Logic},
  year      = {2013},
}

@inproceedings{CD12,
  author    = {K. Chatterjee and L. Doyen},
  title     = {Partial-Observation Stochastic Games: How to Win when Belief Fails},
  booktitle = {Proceedings of LICS 2012: Logic in Computer Science},
  publisher = {IEEE Computer Society Press},
  year      = {2012},
  pages     = {175-184},
  isbn      = {}
}

@article{CdAH11,
  author    = {Krishnendu Chatterjee and
               Luca de Alfaro and
               Thomas A. Henzinger},
  title     = {Qualitative concurrent parity games},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {12},
  number    = {4},
  year      = {2011},
  pages     = {28}
}

@inproceedings{Zie98,
author="W. Zielonka",
title= "Infinite games on finitely coloured graphs with applications to
automata on infinite trees",
booktitle="Theoretical Computer Science",
volume="200(1-2)",
pages="135--183",
year="1998"
}

@article{raptureTool,
  title={{Rapture}: A tool for verifying {Markov} decision processes},
  author={Jeannet, Bertrand and d’Argenio, P and Larsen, K},
  journal={Tools Day},
  volume={2},
  pages={149},
  year={2002}
}

@inproceedings{Komuravelli12,
  author    = {Anvesh Komuravelli and
               Corina S. Pasareanu and
               Edmund M. Clarke},
  title     = {Assume-Guarantee Abstraction Refinement for Probabilistic
               Systems},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {LNCS 7358},
  year      = {2012},
  pages     = {310-326},
  ee        = {http://dx.doi.org/10.1007/978-3-642-31424-7_25},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{ist153,
           month = {January},
            type = {Technical Report},
           title = {{CEGAR for Qualitative Analysis of Probabilistic Systems}},
          author = {Krishnendu Chatterjee and Przemyslaw Daca and Martin Chmel{\'i}k},
       publisher = {IST Austria},
            year = {2014},
             url = {http://repository.ist.ac.at/153/}
}

@article{fullVersion,
  author = {Krishnendu Chatterjee and Martin Chmel{\'i}k and Przemyslaw Daca },
  title = {{CEGAR} for Qualitative Analysis of Probabilistic Systems},
  journal   = {CoRR},
  volume    = {abs/1405.0835},
  year      = {2014},
  ee        = {http://arxiv.org/abs/1405.0835}
}

@misc{RajeevTomBook,
title={Computer-Aided Verification},
author={Rajeev Alur and Thomas A.\ Henzinger},
year=2004,
note={Unpublished, available at \url{http://www.cis.upenn.edu/cis673/}}
}

@inproceedings{Cleaveland91,
  author    = {Rance Cleaveland and
               Bernhard Steffen},
  title     = {Computing Behavioural Relations, Logically},
  booktitle = {ICALP},
  year      = {1991},
  publisher = {Springer},
  series    = {LNCS 510},
  pages     = {127-138},
  ee        = {http://dx.doi.org/10.1007/3-540-54233-7_129},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DArgenioJJL01,
  author    = {Pedro R. D'Argenio and
               Bertrand Jeannet and
               Henrik Ejersbo Jensen and
               Kim Guldstrand Larsen},
  title     = {Reachability Analysis of Probabilistic Systems by Successive
               Refinements},
  booktitle = {PAPM-PROBMIV},
  year      = {2001},
  publisher = {Springer},
  series    = {LNCS 2165},
  pages     = {39-56},
  ee        = {http://dx.doi.org/10.1007/3-540-44804-7_3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DArgenioJJL02,
  author    = {Pedro R. D'Argenio and
               Bertrand Jeannet and
               Henrik Ejersbo Jensen and
               Kim Guldstrand Larsen},
  title     = {Reduction and Refinement Strategies for Probabilistic Analysis},
  booktitle = {PAPM-PROBMIV},
  year      = {2002},
  publisher = {Springer},
  series    = {LNCS 2399},
  pages     = {57-76},
  ee        = {http://dx.doi.org/10.1007/3-540-45605-8_5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{CCHR12,
  author    = {Pavol Cern{\'y} and
               Martin Chmelik and
               Thomas A. Henzinger and
               Arjun Radhakrishna},
  title     = {Interface Simulation Distances},
  booktitle = {GandALF},
  series    = {EPTCS 96},
  year      = {2012},
  pages     = {29-42}
}

@inproceedings{KNP06,
  author    = {Marta Z. Kwiatkowska and
               Gethin Norman and
               David Parker},
  title     = {Game-based Abstraction for {M}arkov Decision Processes},
  booktitle = {QEST},
  year      = {2006},
  pages     = {157-166},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/QEST.2006.19},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{EKVY08,
  author    = {Kousha Etessami and
               Marta Z. Kwiatkowska and
               Moshe Y. Vardi and
               Mihalis Yannakakis},
  title     = {Multi-Objective Model Checking of {M}arkov Decision Processes},
  journal   = {Logical Methods in Computer Science},
  volume    = {4},
  number    = {4},
  year      = {2008},
  ee        = {http://dx.doi.org/10.2168/LMCS-4(4:8)2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{CCST05,
  author    = {Sagar Chaki and
               Edmund M. Clarke and
               Nishant Sinha and
               Prasanna Thati},
  title     = {Automated Assume-Guarantee Reasoning for Simulation Conformance},
  booktitle = {CAV},
  year      = {2005},
  series    = {LNCS 3576},
  publisher = {Springer},
  pages     = {534-547},
  ee        = {http://dx.doi.org/10.1007/11513988_51},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{CV10,
  author    = {Rohit Chadha and
               Mahesh Viswanathan},
  title     = {A counterexample-guided abstraction-refinement framework
               for {M}arkov decision processes},
  journal   = {ACM Trans. Comput. Log. 12},
  year      = {2010},
  pages     = {1},
  ee        = {http://doi.acm.org/10.1145/1838552.1838553},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{HWZ08,
  author    = {Holger Hermanns and
               Bj{\"o}rn Wachter and
               Lijun Zhang},
  title     = {Probabilistic {CEGAR}},
  booktitle = {CAV},
 publisher = {Springer},
  series    = {LNCS 5123},
  year      = {2008},
  pages     = {162-175},
  ee        = {http://dx.doi.org/10.1007/978-3-540-70545-1_16},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{gradel2002automata,
  title={Automata, logics, and infinite games: a guide to current research},
  author={Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke, Thomas},
publisher = {Springer},
  year = {2002},
  series    = {LNCS 2500}
}

@article{Immerman81,
        author="N. Immerman",
  title="Number of quantifiers is better than number of tape cells",
  journal="Journal of Computer and System Sciences",
        volume="22",
        year="1981",
  pages="384--406"
        }

@article{Beeri,
        author      = "C. Beeri",
        title       = "On the membership problem for functional and
                         multivalued dependencies in relational databases",
        journal     = "ACM Trans. on Database Systems",
        volume      = 5,
        pages       = "241--259",
        year        = 1980
}

@inproceedings{FengKP11,
  author    = {Lu Feng and
               Marta Z. Kwiatkowska and
               David Parker},
  title     = {Automated Learning of Probabilistic Assumptions for Compositional
               Reasoning},
  booktitle = {FASE},
  year      = {2011},
 publisher = {Springer},
  series    = {LNCS 6603},
  pages     = {2-17},
  ee        = {http://dx.doi.org/10.1007/978-3-642-19811-3_2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{HJMQ03,
  author    = {Thomas A. Henzinger and
               Ranjit Jhala and
               Rupak Majumdar and
               Shaz Qadeer},
  title     = {Thread-Modular Abstraction Refinement},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {LNCS 2725},
  year      = {2003},
  pages     = {262-274},
  ee        = {http://dx.doi.org/10.1007/978-3-540-45069-6_27},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{ClarkeBook,
        author="E.M. Clarke and O. Grumberg and D. Peled",
        title = "Model Checking",
        year= 1999,
        publisher= "MIT Press"
        }

	@incollection{Pnu85a,
        author      =   "A. Pnueli",
        title       =   "In transition from global to modular temporal
                         reasoning about programs",
        booktitle   =   "Logics and Models of Concurrent Systems",
        series      =   "{NATO}  Advanced Summer Institutes F-13",
        publisher   =   "Springer",
        year        =   "1985",
        pages       =   "123--144",
}

@article{PGBCB08,
  author    = {C. S. Pasareanu and
               D. Giannakopoulou and
               M. G. Bobaru and
               J. M. Cobleigh and
               H. Barringer},
  title     = {Learning to divide and conquer: applying the L* algorithm
               to automate assume-guarantee reasoning},
  journal   = {Formal Methods in System Design},
  volume    = {32},
  number    = {3},
  year      = {2008},
  pages     = {175-205},
  ee        = {http://dx.doi.org/10.1007/s10703-008-0049-6}
}

@inproceedings{AdHJ01,
  author    = {Luca de Alfaro and
               Thomas A. Henzinger and
               Ranjit Jhala},
  title     = {Compositional Methods for Probabilistic Systems},
  booktitle = {CONCUR},
  year      = {2001},
  series    = {LNCS 2154},
  publisher = {Springer},
  pages     = {351-365},
  ee        = {http://dx.doi.org/10.1007/3-540-44685-0_24},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{KNPQ10,
  author    = {Marta Z. Kwiatkowska and
               Gethin Norman and
               David Parker and
               Hongyang Qu},
  title     = {Assume-Guarantee Verification for Probabilistic Systems},
  booktitle = {TACAS},
  year      = {2010},
publisher = {Springer},
  series    = {LNCS 6015},
  pages     = {23-37},
  ee        = {http://dx.doi.org/10.1007/978-3-642-12002-2_3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{P81,
  title={Myths about the mutual exclusion problem},
  author={Peterson, Gary L.},
  journal={Information Processing Letters},
  volume={12},
  number={3},
  pages={115--116},
  year={1981},
  publisher={Elsevier}
}

@phdthesis{SegalaT,
    	author = "R. Segala",
    	title = "Modeling and Verification of Randomized Distributed
    	    	Real-Time Systems",
    	school = "MIT Press",
    	year = 1995,
    	note = "Technical Report MIT/LCS/TR-676"
    	}

@article{CdAFMR13,
  author    = {Krishnendu Chatterjee and
               Luca de Alfaro and
               Marco Faella and
               Rupak Majumdar and
               Vishwanath Raman},
  title     = {Code-aware resource management},
  journal   = {Formal Methods in System Design},
  volume    = {42},
  number    = {2},
  year      = {2013},
  pages     = {146-174},
  ee        = {http://dx.doi.org/10.1007/s10703-012-0170-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{PSL00,
	author = "A. Pogosyants and R. Segala and N. Lynch",
	title = "Verification of the Randomized Consensus Algorithm of {A}spnes and {H}erlihy: a Case Study",
	journal = "Distributed Computing",
	volume = "13",
	number = "3",
	pages = "155-186",
	year = "2000"
	}

@inproceedings{Sto02b,
        author =        {M.I.A. Stoelinga},
        booktitle =     {Formal Aspects of Computing},
        title =         {Fun with {FireWire}: Experiments with Verifying
                         the {IEEE1394} Root Contention Protocol},
        year =          "2002"
}

@inproceedings{BerkP95,
    	author = "A. Aziz and V. Singhal and F. Balarin and
    	    R.K. Brayton and A.L. Sangiovanni-Vincentelli",
    	title = "It Usually Works: The Temporal Logic of Stochastic Systems",
    	booktitle = "CAV",
	pages     = {155-165},
    	series = "LNCS 939",
    	publisher = "Springer",
    	year = 1995
 }

@book{FV97,
	author = "J. Filar and K. Vrieze",
	title = "Competitive {Markov} Decision Processes",
	publisher = "Springer",
	year = 1997
	}

@inproceedings{HHK95,
  author    = {Monika Rauch Henzinger and
               Thomas A. Henzinger and
               Peter W. Kopke},
  title     = {Computing Simulations on Finite and Infinite Graphs},
  booktitle = {FOCS},
  year      = {1995},
  pages     = {453-462},
}
@inproceedings{dAHK98,
  author    = {Luca de Alfaro and
               Thomas A. Henzinger and
               Orna Kupferman},
  title     = {Concurrent Reachability Games},
  booktitle = {FOCS},
  year      = {1998},
  pages     = {564-575},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/SFCS.1998.743507}
}
@inproceedings{Clarke00,
  author    = {Edmund M. Clarke and
               Orna Grumberg and
               Somesh Jha and
               Yuan Lu and
               Helmut Veith},
  title     = {Counterexample-Guided Abstraction Refinement},
  booktitle = {CAV},
  year      = {2000},
  pages     = {154-169},
  series    = {LNCS 1855},
  ee        = {http://dx.doi.org/10.1007/10722167_15},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{CCK12,
  author    = {Krishnendu Chatterjee and
               Siddhesh Chaubal and
               Pritish Kamath},
  title     = {Faster Algorithms for Alternating Refinement Relations},
  booktitle = {CSL},
publisher = {Schloss Dagstuhl},
  series    = {LIPIcs 16},
  year      = {2012},
  pages     = {167-182},
}
@article{AHK02,
  author    = {Rajeev Alur and
               Thomas A. Henzinger and
               Orna Kupferman},
  title     = {Alternating-time temporal logic},
  journal   = {J. ACM},
  volume    = {49},
  number    = {5},
  year      = {2002},
  pages     = {672-713},
}
@inproceedings{CDH10,
  author    = {Krishnendu Chatterjee and
               Laurent Doyen and
               Thomas A. Henzinger},
  title     = {Qualitative Analysis of Partially-Observable {M}arkov Decision
               Processes},
  booktitle = {MFCS},
  year      = {2010},
publisher = {Springer},
  series    = {LNCS 6281},
  pages     = {258-269},
}

@inproceedings{Henzinger03,
  author    = {Thomas A. Henzinger and
               Ranjit Jhala and
               Rupak Majumdar},
  title     = {Counterexample-Guided Control},
  booktitle = {ICALP},
  year      = {2003},
  pages     = {886-902},
 publisher = {Springer},
  series    = {LNCS 2719},
  ee        = {http://dx.doi.org/10.1007/3-540-45061-0_69},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

        @inproceedings{AHKV98,
        author="R. Alur and T.A. Henzinger and O. Kupferman and M.Y. Vardi",
        title="Alternating Refinement Relations",
        booktitle="CONCUR",
        series="LNCS 1466",
        publisher="Springer",
        year="1998",
        pages="163--178"
        }

@inproceedings{Milner71,
  author    = {Robin Milner},
  title     = {An Algebraic Definition of Simulation Between Programs},
  booktitle = {IJCAI},
  year      = {1971},
  pages     = {481-489},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{HJ94,
  author    = {Hans Hansson and
               Bengt Jonsson},
  title     = {A Logic for Reasoning about Time and Reliability},
  journal   = {Formal Asp. Comput.},
  volume    = {6},
  number    = {5},
  year      = {1994},
  pages     = {512-535},
  ee        = {http://dx.doi.org/10.1007/BF01211866},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{BdA95,
  author    = {Andrea Bianco and
               Luca de Alfaro},
  title     = {Model Checking of Probabalistic and Nondeterministic Systems},
  booktitle = {FSTTCS},
  year      = {1995},
  pages     = {499-513},
  series    = {LNCS 1026},
  publisher = {Springer},
  ee        = {http://dx.doi.org/10.1007/3-540-60692-0_7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{CDFL09,
  author    = {Krishnendu Chatterjee and
               Luca de Alfaro and
               Marco Faella and
               Axel Legay},
  title     = {Qualitative Logics and Equivalences for Probabilistic Systems},
  journal   = {Logical Methods in Computer Science},
  volume    = {5},
  number    = {2},
  year      = {2009},
  ee        = {http://arxiv.org/abs/0903.2445},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{Vazirani01,
 author = {Vazirani, Vijay V.},
 title = {Approximation Algorithms},
 year = {2001},
 isbn = {3-540-65367-8},
 publisher = {Springer-Verlag New York, Inc.},
 address = {New York, NY, USA},
}

@article{SL95,
  author    = {Roberto Segala and
               Nancy A. Lynch},
  title     = {Probabilistic Simulations for Probabilistic Processes},
  journal   = {Nord. J. Comput.},
  volume    = {2},
  number    = {2},
  year      = {1995},
  pages     = {250-273},
}

@book{Howard,
    author = {Howard, Ronald A.},
    citeulike-article-id = {1431073},
    keywords = {bibtex-import, schaal-phd},
    posted-at = {2007-07-03 16:31:45},
    priority = {2},
    publisher = {MIT Press},
    title = {{Dynamic Programming and {M}arkov Processes}},
    year = {1960}
}

@InProceedings{LR81,
author={D. Lehmann and M. Rabin},
title={On the Advantage of Free Choice: {A} Symmetric and Fully Distributed Solution to the Dining Philosophers Problem (Extended Abstract)},
booktitle={Proc. 8th Annual ACM Symposium on Principles of Programming Languages (POPL'81)},
year={1981},

editor={},
pages={133--138},
organization={},
publisher={},
address={},
month={},
note={},
key={}
}

@article{IR90,
author={A. Itai and M. Rodeh},
title={Symmetry Breaking in Distributed Networks},
journal={Information and Computation},
year={1990},

volume={88},
number={1},
pages={},
month={},
note={},
key={}
}

@inproceedings{DBLP:conf/sefm/LegayST14,
	author    = {Axel Legay and
	Sean Sedwards and
	Louis{-}Marie Traonouez},
	title     = {Scalable Verification of Markov Decision Processes},
	booktitle = {SEFM},
	pages     = {350--362},
	year      = {2014},
	doi       = {10.1007/978-3-319-15201-1_23},
	timestamp = {Thu, 05 Feb 2015 11:00:54 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sefm/LegayST14},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}  crossref  = {DBLP:conf/sefm/2014w},

url       = {http://dx.doi.org/10.1007/978-3-319-15201-1_23},

@proceedings{DBLP:conf/sefm/2014w,
	editor    = {Carlos Canal and
	Akram Idani},
	title     = {Software Engineering and Formal Methods - {SEFM} 2014 Collocated Workshops:
	HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September
	1-2, 2014, Revised Selected Papers},
	series    = {Lecture Notes in Computer Science},
	volume    = {8938},
	publisher = {Springer},
	year      = {2015},
	url       = {http://dx.doi.org/10.1007/978-3-319-15201-1},
	doi       = {10.1007/978-3-319-15201-1},
	isbn      = {978-3-319-15200-4},
	timestamp = {Thu, 05 Feb 2015 10:57:53 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sefm/2014w},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{arxiv,
	author    = {Tom{\'a}\v{s} Br{\'a}zdil and
	Krishnendu Chatterjee and
	Martin Chmel\i{i}k and
	Vojt\v{e}ch Forejt and
	Jan K\v{r}et\'{\i}nsk{\'y} and
	Marta Z. Kwiatkowska and
	David Parker and
	Mateusz Ujma},
	title     = {Verification of {M}arkov Decision Processes using Learning
	Algorithms},
	journal   = {CoRR},
	volume    = {abs/1402.2967},
	year      = {2014},
	ee        = {http://arxiv.org/abs/1402.2967},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{ DBLP:conf/cav/YounesS02,
	author = "H{\aa}kan L. S. Younes and Reid G. Simmons",
	title = "Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling",
	booktitle = "CAV",
	year = "2002",
	pages = "223--235",
	ee = "http://dx.doi.org/10.1007/3-540-45657-0\\\_17",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/tacas/YounesKNP04,
	author = "H{\aa}kan L. S. Younes and Marta Z. Kwiatkowska and Gethin Norman and David Parker",
	title = "Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study",
	booktitle = "TACAS",
	year = "2004",
	pages = "46--60",
	ee = "http://dx.doi.org/10.1007/978-3-540-24730-2\\\\_4",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/cav/SenVA04,
	author = "Koushik Sen and Mahesh Viswanathan and Gul Agha",
	title = "Statistical Model Checking of Black-Box Probabilistic Systems",
	booktitle = "CAV",
	year = "2004",
	pages = "202--215",
	ee = "http://dx.doi.org/10.1007/978-3-540-27813-9\\\\_16",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

proceedings{DBLP:conf/cav/2004,
	editor    = {Rajeev Alur and
	Doron Peled},
	title     = {Computer Aided Verification, 16th International Conference,
	CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
	booktitle = {CAV},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {3114},
	year      = {2004},
	isbn      = {3-540-22342-8},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{ DBLP:conf/hybrid/ZulianiPC10,
	author = "Paolo Zuliani and Andr{\'e} Platzer and Edmund M. Clarke",
	title = "Bayesian statistical model checking with application to Simulink/Stateflow verification",
	booktitle = "HSCC",
	year = "2010",
	pages = "243--252",
	ee = "http://doi.acm.org/10.1145/1755952.1755987",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/cmsb/JhaCLLPZ09,
	author = "Sumit Kumar Jha and Edmund M. Clarke and Christopher James Langmead and Axel Legay and Andr{\'e} Platzer and Paolo Zuliani",
	title = "A Bayesian Approach to Model Checking Biological Systems",
	booktitle = "CMSB",
	year = "2009",
	pages = "218--234",
	ee = "http://dx.doi.org/10.1007/978-3-642-03845-7\\_15",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/forte/BasuBBCDL10,
	author = "Ananda Basu and Saddek Bensalem and Marius Bozga and Beno\^{\i}t Caillaud and Beno\^{\i}t Delahaye and Axel Legay",
	title = "Statistical Abstraction and Model-Checking of Large Heterogeneous Systems",
	booktitle = "FMOODS/FORTE",
	year = "2010",
	pages = "32--46",
	ee = "http://dx.doi.org/10.1007/978-3-642-13464-7\\\\_4",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/kbse/HeJBGW10,
	author = "Ru He and Paul Jennings and Samik Basu and Arka P. Ghosh and Huaiqing Wu",
	title = "A bounded statistical approach for model checking of unbounded until properties",
	booktitle = "ASE",
	year = "2010",
	pages = "225--234",
	ee = "http://doi.acm.org/10.1145/1858996.1859043",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/sbmf/YounesCZ10,
	author = "H{\aa}kan L. S. Younes and Edmund M. Clarke and Paolo Zuliani",
	title = "Statistical Verification of Probabilistic Properties with Unbounded Until",
	booktitle = "SBMF",
	year = "2010",
	pages = "144--160",
	ee = "http://dx.doi.org/10.1007/978-3-642-19829-8\\_10",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/atva/ClarkeZ11,
	author = "Edmund M. Clarke and Paolo Zuliani",
	title = "Statistical Model Checking for Cyber-Physical Systems",
	booktitle = "ATVA",
	year = "2011",
	pages = "1--12",
	ee = "http://dx.doi.org/10.1007/978-3-642-24372-1\\\\_1",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/tacas/BarbotHP12,
	author = "Beno\^{\i}t Barbot and Serge Haddad and Claudine Picaronny",
	title = "Coupling and Importance Sampling for Statistical Model Checking",
	booktitle = "TACAS",
	year = "2012",
	pages = "331--346",
	ee = "http://dx.doi.org/10.1007/978-3-642-28756-5\\\\_23",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

proceedings{DBLP:conf/tacas/2012,
	editor    = {Cormac Flanagan and
	Barbara K{\"o}nig},
	title     = {Tools and Algorithms for the Construction and Analysis of
	Systems - 18th International Conference, TACAS 2012, Held
	as Part of the European Joint Conferences on Theory and
	Practice of Software, ETAPS 2012, Tallinn, Estonia, March
	24 - April 1, 2012. Proceedings},
	booktitle = {TACAS},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {7214},
	year      = {2012},
	isbn      = {978-3-642-28755-8},
	ee        = {http://dx.doi.org/10.1007/978-3-642-28756-5},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{ DBLP:conf/cav/JegourelLS12,
	author = "Cyrille J{\'e}gourel and Axel Legay and Sean Sedwards",
	title = "Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking",
	booktitle = "CAV",
	year = "2012",
	pages = "327--342",
	ee = "http://dx.doi.org/10.1007/978-3-642-31424-7\\_26",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/cav/JegourelLS13,
	author = "Cyrille J{\'e}gourel and Axel Legay and Sean Sedwards",
	title = "Importance Splitting for Statistical Model Checking Rare Properties",
	booktitle = "CAV",
	year = "2013",
	pages = "576--591",
	ee = "http://dx.doi.org/10.1007/978-3-642-39799-8\\\\_38",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/cmsb/PalaniappanG0HT13,
	author = "Sucheendra K. Palaniappan and Benjamin M. Gyori and Bing Liu and David Hsu and P. S. Thiagarajan",
	title = "Statistical Model Checking Based Calibration and Analysis of Bio-pathway Models",
	booktitle = "CMSB",
	year = "2013",
	pages = "120--134",
	ee = "http://dx.doi.org/10.1007/978-3-642-40708-6\\\\_10",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

proceedings{DBLP:conf/cav/2013,
	editor    = {Natasha Sharygina and
	Helmut Veith},
	title     = {Computer Aided Verification - 25th International Conference,
	CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
	booktitle = {CAV},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {8044},
	year      = {2013},
	isbn      = {978-3-642-39798-1},
	ee        = {http://dx.doi.org/10.1007/978-3-642-39799-8},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

proceedings{DBLP:conf/cav/2012,
	editor    = {P. Madhusudan and
	Sanjit A. Seshia},
	title     = {Computer Aided Verification - 24th International Conference,
	CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings},
	booktitle = {CAV},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {7358},
	year      = {2012},
	isbn      = {978-3-642-31423-0},
	ee        = {http://dx.doi.org/10.1007/978-3-642-31424-7},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

proceedings{DBLP:conf/kbse/2010,
	editor    = {Charles Pecheur and
	Jamie Andrews and
	Elisabetta Di Nitto},
	title     = {ASE 2010, 25th IEEE/ACM International Conference on Automated
	Software Engineering,  Antwerp, Belgium, September 20-24,
	2010},
	booktitle = {ASE},
	publisher = {ACM},
	year      = {2010},
	isbn      = {978-1-4503-0116-9},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

proceedings{DBLP:conf/sbmf/2010,
	editor    = {Jim Davies and
	Leila Silva and
	Adenilso da Silva Sim{\~a}o},
	title     = {Formal Methods: Foundations and Applications - 13th Brazilian
	Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November
	8-11, 2010, Revised Selected Papers},
	booktitle = {SBMF},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {6527},
	year      = {2011},
	isbn      = {978-3-642-19828-1},
	ee        = {http://dx.doi.org/10.1007/978-3-642-19829-8},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{ DBLP:conf/forte/BogdollFHH11,
	author = "Jonathan Bogdoll and Luis Mar{\'i}a Ferrer Fioriti and Arnd Hartmanns and Holger Hermanns",
	title = "Partial Order Methods for Statistical Model Checking and Simulation",
	booktitle = "FMOODS/FORTE",
	year = "2011",
	pages = "59--74",
	ee = "http://dx.doi.org/10.1007/978-3-642-21461-5\\\_4",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/qest/HenriquesMZPC12,
	author = "David Henriques and Jo{\~a}o Martins and Paolo Zuliani and Andr{\'e} Platzer and Edmund M. Clarke",
	title = "Statistical Model Checking for {Markov} Decision Processes",
	booktitle = "QEST",
	year = "2012",
	pages = "84--93",
	ee = "http://doi.ieeecomputersociety.org/10.1109/QEST.2012.19",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/mmb/BogdollHH12,
	author = "Jonathan Bogdoll and Arnd Hartmanns and Holger Hermanns",
	title = "Simulation and Statistical Model Checking for Modestly Nondeterministic Models",
	booktitle = "MMB/DFT",
	year = "2012",
	pages = "249--252",
	ee = "http://dx.doi.org/10.1007/978-3-642-28540-0\\\_20",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/nfm/DavidDLLM13,
	author = "Alexandre David and Dehui Du and Kim Guldstrand Larsen and Axel Legay and Marius Mikucionis",
	title = "Optimizing Control Strategy Using Statistical Model Checking",
	booktitle = "NASA Formal Methods",
	year = "2013",
	pages = "352--367",
	ee = "http://dx.doi.org/10.1007/978-3-642-38088-4\\\_24",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ DBLP:conf/sac/LassaigneP12,
	author = "Richard Lassaigne and Sylvain Peyronnet",
	title = "Approximate planning and verification for large {Markov} decision processes",
	booktitle = "SAC",
	year = "2012",
	pages = "1314--1319",
	ee = "http://doi.acm.org/10.1145/2245276.2231984",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@Article{ DBLP:journals/corr/LegayS13,
	author = "Axel Legay and Sean Sedwards",
	title = "Lightweight {Monte} {Carlo} Algorithm for {Markov} Decision Processes",
	journal = "CoRR",
	volume = "abs/1310.3609",
	year = "2013",
	ee = "http://arxiv.org/abs/1310.3609",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

proceedings{DBLP:conf/qest/2012,
	title     = {Ninth International Conference on Quantitative Evaluation
	of Systems, QEST 2012, London, United Kingdom, September
	17-20, 2012},
	booktitle = {QEST},
	publisher = {IEEE Computer Society},
	year      = {2012},
	isbn      = {978-1-4673-2346-8},
	ee        = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6354262},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

proceedings{DBLP:conf/forte/2011,
	editor    = {Roberto Bruni and
	J{\"u}rgen Dingel},
	title     = {Formal Techniques for Distributed Systems - Joint 13th IFIP
	WG 6.1 International Conference, FMOODS 2011, and 31st IFIP
	WG 6.1 International Conference, FORTE 2011, Reykjavik,
	Iceland, June 6-9, 2011. Proceedings},
	booktitle = {FMOODS/FORTE},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {6722},
	year      = {2011},
	isbn      = {978-3-642-21460-8},
	ee        = {http://dx.doi.org/10.1007/978-3-642-21461-5},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
proceedings{DBLP:conf/mmb/2012,
	editor    = {Jens B. Schmitt},
	title     = {Measurement, Modelling, and Evaluation of Computing Systems
	and Dependability and Fault Tolerance - 16th International
	GI/ITG Conference, MMB {\&} DFT 2012, Kaiserslautern, Germany,
	March 19-21, 2012. Proceedings},
	booktitle = {MMB/DFT},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {7201},
	year      = {2012},
	isbn      = {978-3-642-28539-4},
	ee        = {http://dx.doi.org/10.1007/978-3-642-28540-0},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/formats/DavidLLMPVW11,
	author    = {Alexandre David and
	Kim G. Larsen and
	Axel Legay and
	Marius Mikucionis and
	Danny B{\o}gsted Poulsen and
	Jonas van Vliet and
	Zheng Wang},
	title     = {Statistical Model Checking for Networks of Priced Timed
	Automata},
	booktitle = {FORMATS},
	year      = {2011},
	_pages     = {80-96},
	ee        = {http://dx.doi.org/10.1007/978-3-642-24310-3_7},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/cav/DavidLLMW11,
	author    = {Alexandre David and
	Kim G. Larsen and
	Axel Legay and
	Marius Mikucionis and
	Zheng Wang},
	title     = {Time for Statistical Model Checking of Real-Time Systems},
	booktitle = {CAV},
	year      = {2011},
	pages     = {349-355},
	ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1_27},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:journals/corr/abs-1208-3856,
	author    = {Alexandre David and
	Dehui Du and
	Kim G. Larsen and
	Axel Legay and
	Marius Mikucionis and
	Danny B{\o}gsted Poulsen and
	Sean Sedwards},
	title     = {Statistical Model Checking for Stochastic Hybrid Systems},
	booktitle = {HSB},
	year      = {2012},
	pages     = {122-136},
	ee        = {http://dx.doi.org/10.4204/EPTCS.92.9},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/formats/EllenGF12,
	author    = {Christian Ellen and
	Sebastian Gerwinn and
	Martin Fr{\"a}nzle},
	title     = {Confidence Bounds for Statistical Model Checking of Probabilistic
	Hybrid Systems},
	booktitle = {FORMATS},
	year      = {2012},
	pages     = {123-138},
	ee        = {http://dx.doi.org/10.1007/978-3-642-33365-1_10},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/formats/Larsen12,
	author    = {Kim G. Larsen},
	title     = {Statistical Model Checking, Refinement Checking, Optimization,
	... for Stochastic Hybrid Systems},
	booktitle = {FORMATS},
	year      = {2012},
	pages     = {7-10},
	ee        = {http://dx.doi.org/10.1007/978-3-642-33365-1_2},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/ifm/Larsen13,
	author    = {Kim Guldstrand Larsen},
	title     = {Priced Timed Automata and Statistical Model Checking},
	booktitle = {IFM},
	year      = {2013},
	_pages     = {154-161},
	ee        = {http://dx.doi.org/10.1007/978-3-642-38613-8_11},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

proceedings{DBLP:conf/cav/2011,
	editor    = {Ganesh Gopalakrishnan and
	Shaz Qadeer},
	title     = {Computer Aided Verification - 23rd International Conference,
	CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
	booktitle = {CAV},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {6806},
	year      = {2011},
	isbn      = {978-3-642-22109-5},
	ee        = {http://dx.doi.org/10.1007/978-3-642-22110-1},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

proceedings{DBLP:conf/formats/2011,
	editor    = {Uli Fahrenberg and
	Stavros Tripakis},
	title     = {Formal Modeling and Analysis of Timed Systems - 9th International
	Conference, FORMATS 2011, Aalborg, Denmark, September 21-23,
	2011. Proceedings},
	booktitle = {FORMATS},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {6919},
	year      = {2011},
	isbn      = {978-3-642-24309-7},
	ee        = {http://dx.doi.org/10.1007/978-3-642-24310-3},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

proceedings{DBLP:conf/ifm/2013,
	editor    = {Einar Broch Johnsen and
	Luigia Petre},
	title     = {Integrated Formal Methods, 10th International Conference,
	IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings},
	booktitle = {IFM},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {7940},
	year      = {2013},
	isbn      = {978-3-642-38612-1, 978-3-642-38613-8},
	ee        = {http://dx.doi.org/10.1007/978-3-642-38613-8},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:journals/corr/abs-1207-1272,
	author    = {Peter E. Bulychev and
	Alexandre David and
	Kim Guldstrand Larsen and
	Marius Mikucionis and
	Danny B{\o}gsted Poulsen and
	Axel Legay and
	Zheng Wang},
	title     = {{UPPAAL-SMC}: Statistical Model Checking for Priced Timed
	Automata},
	booktitle = {QAPL},
	year      = {2012},
	_pages     = {1-16},
	ee        = {http://dx.doi.org/10.4204/EPTCS.85.1},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/qest/BoyerCLS13,
	author    = {Beno\^{\i}t Boyer and
	Kevin Corre and
	Axel Legay and
	Sean Sedwards},
	title     = {{PLASMA-lab}: A Flexible, Distributable Statistical Model
	Checking Library},
	booktitle = {QEST},
	year      = {2013},
	pages     = {160-164},
	ee        = {http://dx.doi.org/10.1007/978-3-642-40196-1_12},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
@InProceedings{FKP11,
	author={L. Feng and M. Kwiatkowska and D. Parker},
	title={Automated Learning of Probabilistic Assumptions for Compositional Reasoning},
	booktitle={FASE},
	year={2011},
	pages={2-17}
}

proceedings{DBLP:conf/tacas/2012,
	editor    = {Cormac Flanagan and
	Barbara K{\"o}nig},
	title     = {Tools and Algorithms for the Construction and Analysis of
	Systems - 18th International Conference, TACAS 2012, Held
	as Part of the European Joint Conferences on Theory and
	Practice of Software, ETAPS 2012, Tallinn, Estonia, March
	24 - April 1, 2012. Proceedings},
	booktitle = {TACAS},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {7214},
	year      = {2012},
	isbn      = {978-3-642-28755-8},
	ee        = {http://dx.doi.org/10.1007/978-3-642-28756-5},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
proceedings{DBLP:conf/qest/2013,
	editor    = {Kaustubh R. Joshi and
	Markus Siegle and
	Mari{\"e}lle Stoelinga and
	Pedro R. D'Argenio},
	title     = {Quantitative Evaluation of Systems - 10th International
	Conference, QEST 2013, Buenos Aires, Argentina, August 27-30,
	2013. Proceedings},
	booktitle = {QEST},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {8054},
	year      = {2013},
	isbn      = {978-3-642-40195-4},
	ee        = {http://dx.doi.org/10.1007/978-3-642-40196-1},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
proceedings{DBLP:journals/corr/abs-1207-0559,
	editor    = {Herbert Wiklicky and
	Mieke Massink},
	title     = {Proceedings 10th Workshop on Quantitative Aspects of Programming
	Languages and Systems, QAPL 2012, Tallinn, Estonia, 31 March
	and 1 April 2012},
	booktitle = {QAPL},
	series    = {EPTCS},
	volume    = {85},
	year      = {2012},
	ee        = {http://dx.doi.org/10.4204/EPTCS.85},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{CGKM12,
	author={R. Calinescu and C. Ghezzi and M. Kwiatkowska and R. Mirandola},
	title={Self-adaptive software needs quantitative verification at runtime},
	journal={Communications of the ACM},
	year={2012},

	volume={55},
	number={9},
	pages={69-77 },
	publisher={ACM}
}

@article{H63,
	title={Probability inequalities for sums of bounded random variables},
	author={Hoeffding, Wassily},
	journal={Journal of the American statistical association},
	volume={58},
	number={301},
	pages={13-30},
	year={1963},
	publisher={Taylor \& Francis Group}
}

@InProceedings{HNP+11,
	author={E. M. Hahn and G. Norman and D. Parker and B. Wachter and L. Zhang},
	title={Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems},
	booktitle={QEST},
	year={2011},

	editor={},
	pages={69-78}
}

@inproceedings{MBLG05,
	title={Bounded real-time dynamic programming: {RTDP} with monotone upper bounds and performance guarantees},
	author={McMahan, H Brendan and Likhachev, Maxim and Gordon, Geoffrey J},
	booktitle={ICML},
	_pages={569--576},
	year={2005}
}

@inproceedings{BKK11,
	title={Efficient analysis of probabilistic programs with an unbounded counter},
	author={Br{\'a}zdil, Tom{\'a}{\v{s}} and Kiefer, Stefan and Ku{\v{c}}era, Anton{\'\i}n},
	booktitle={CAV},
	pages={208--224},
	year={2011},
}

@article{AV79,
	title={Fast probabilistic algorithms for Hamiltonian circuits and matchings},
	author={Angluin, Dana and Valiant, Leslie G},
	journal={Journal of Computer and system Sciences},
	volume={18},
	number={2},
	pages={155-193},
	year={1979},
	publisher={Elsevier}
}

@inproceedings{Strehl,
	author = {Strehl, Alexander L. and Li, Lihong and Wiewiora, Eric and Langford, John and Littman, Michael L.},
	title = {{PAC} Model-free Reinforcement Learning},
	booktitle = {ICML},
	series = {},
	year = {2006},
	pages = {881-888}
}

@inproceedings{CH11,
	title={Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification},
	author={Chatterjee, Krishnendu and Henzinger, Monika},
	booktitle={SODA},
	_pages={1318--1336},
	year={2011}
}

@inproceedings{CH12,
	author = "K. Chatterjee and M. Henzinger",
	title = "An {O}$(n^2)$ Algorithm for Alternating {B}{\"u}chi Games",
	booktitle ="SODA",
	year = "2012",
	pages     = {1386-1399}
}

@inproceedings{CBGK08,
	title={Reduction techniques for model checking {Markov} decision processes},
	author={Ciesinski, Frank and Baier, Christel and Grosser, Marcus and Klein, Joachim},
	booktitle={QEST},
	pages={45--54},
	year={2008}
}

@phdthesis{DeA97,
	title={Formal verification of probabilistic systems},
	author={De Alfaro, Luca},
	year={1997},
	_school={Stanford University}
}

@article{BBS95,
	title = "Learning to act using real-time dynamic programming ",
	journal = "Artificial Intelligence ",
	volume = "72",
	number = "1–2",
	pages = "81 - 138",
	year = "1995",
	note = "",
	issn = "0004-3702",
	doi = "http://dx.doi.org/10.1016/0004-3702(94)00011-O",
	author = "Andrew G. Barto and Steven J. Bradtke and Satinder P. Singh"
}
@inproceedings{BG03,
	title={Labeled {RTDP}: Improving the Convergence of Real-Time Dynamic Programming},
	author={Bonet, Blai and Geffner, Hector},
	booktitle = {ICAPS},
	year      = {2003},
	pages     = {12-21}
}
@inproceedings{STSR06,
	title={Focused real-time dynamic programming for {MDPs}: Squeezing more out of a heuristic},
	author={Smith, Trey and Simmons, Reid},
	booktitle = {AAAI},
	year      = {2006},
	pages     = {1227-1232}
}

@inproceedings{HMZ+12,
	author    = {David Henriques and
	Jo{\~a}o Martins and
	Paolo Zuliani and
	Andr{\'e} Platzer and
	Edmund M. Clarke},
	title     = {Statistical Model Checking for {Markov} Decision Processes},
	booktitle = {QEST},
	publisher = {IEEE Computer Society},
	year      = {2012},
	pages     = {84-93},
}

@inproceedings{LP12,
	author    = {Richard Lassaigne and Sylvain Peyronnet},
	title     = {Approximate planning and verification for large {Markov} decision processes},
	booktitle = {SAC},
	year      = {2012},
	pages     = {1314-1319},
}

@inproceedings{BHH12,
	author    = {Jonathan Bogdoll and
	Arnd Hartmanns and
	Holger Hermanns},
	title     = {Simulation and Statistical Model Checking for Modestly Nondeterministic
	Models},
	booktitle = {MMB/DFT},
	year      = {2012},
	pages     = {249-252}
}
@inproceedings{KNP11,
	author={M. Kwiatkowska and G. Norman and D. Parker},
	title={{PRISM} 4.0: Verification of Probabilistic Real-time Systems},
	booktitle={CAV},
	year={2011},
	pages={585-591}
}
@article{KNPS06,
	author={M. Kwiatkowska and G. Norman and D. Parker and J. Sproston},
	title={Performance Analysis of Probabilistic Timed Automata using Digital Clocks},
	journal={Formal Methods in System Design},
	year={2006},

	volume={29},
	number={},
	pages={33-78},
	month={},
	note={},
	key={}
}
@Article{KNS03b,
	author={M. Kwiatkowska and G. Norman and J. Sproston},
	title={Probabilistic Model Checking of Deadline Properties in the {IEEE 1394 FireWire} Root Contention Protocol},
	journal={Formal Aspects of Computing},
	year={2003},

	volume={14},
	number={3},
	pages={295--318},
	_month={April},
	note={},
	key={}
}
@InProceedings{KNS02a,
	author={M. Kwiatkowska and G. Norman and J. Sproston},
	title={Probabilistic Model Checking of the {IEEE} 802.11 Wireless Local Area Network Protocol},
	booktitle={PAPM/PROBMIV},
	year={2002},
	pages={169--187},
	organization={},
	publisher={Springer}
}
@InProceedings{YS02,
	author={H. Younes and R. Simmons},
	title={Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling},
	booktitle={CAV},
	year={2002},
	pages={223--235},
}
@InProceedings{HLMP04,
	author={T. H\'erault and R. Lassaigne and F. Magniette and S. Peyronnet},
	title={Approximate Probabilistic Model Checking},
	booktitle={VMCAI},
	year={2004},

	editor={},
	pages={307-329},
}

@InProceedings{HJB+10,
	author={Ru He and Paul Jennings and Samik Basu and Arka P. Ghosh and Huaiqing Wu},
	title={A bounded statistical approach for model checking of unbounded until properties},
	booktitle={ASE},
	year={2010},

	editor={},
	pages={225--234},
	organization={},
	publisher={},
	series={},
	volume={},
	address={},
	month={},
	note={},
	key={}
}

InProceedings{YCZ10,
	author={Haakan Younes and Edmund M. Clarke and Paolo Zuliani},
	title={Statistical verification of probabilistic properties with unbounded until},
	booktitle={SBMF},
	year={2010},

	editor={},
	pages={144--160},
	organization={},
	publisher={},
	series={},
	volume={},
	address={},
	month={},
	note={},
	key={}
}
@InProceedings{SVA05,
	author={K. Sen and M. Viswanathan and G. Agha},
	title={On statistical model checking of stochastic systems},
	booktitle={CAV},
	year={2005},

	editor={},
	pages={266--280},
}
@InProceedings{RP09,
	author={D. E. Rabih and N. Pekergin},
	title={Statistical model checking using perfect simulation},
	booktitle={ATVA},
	year={2009},

	editor={},
	pages={120--134},
	organization={},
}
@InProceedings{KNS01a,
	author={M. Kwiatkowska and G. Norman and R. Segala},
	title={Automated Verification of a Randomized Distributed Consensus Protocol Using {Cadence SMV} and {PRISM}},
	booktitle={CAV},
	year={2001},
	pages={194--206},
	organization={},
}
@InProceedings{BdA95,
	author={A. Bianco and L. de Alfaro},
	title={Model Checking of Probabilistic and Nondeterministic Systems},
	booktitle={FSTTCS},
	year={1995},

	_editor={P. Thiagarajan},
	pages={499--513},
	organization={},
}
@InProceedings{Var85,
	author={M. Vardi},
	title={Automatic Verification of Probabilistic Concurrent Finite State Programs},
	booktitle={FOCS},
	year={1985},

	editor={},
	pages={327--338},
	organization={},
}
@InProceedings{BCHG+97,
	author={C. Baier and E. Clarke and V. Hartonas-Garmhausen and M. Kwiatkowska and M. Ryan},
	title={Symbolic Model Checking for Probabilistic Processes},
	booktitle={ICALP},
	year={1997},

	_editor={P. Degano and R. Gorrieri and A. Marchetti-Spaccamela},
	pages={430--440},
	organization={},
}
@InProceedings{DJJL01,
	author={P. D{'A}rgenio and B. Jeannet and H. Jensen and K. Larsen},
	title={Reachability analysis of probabilistic systems by successive refinements},
	booktitle={PPAPM/PROBMIV},
	year={2001},
	pages={39--56},
	organization={},
}
@inproceedings{HWZ08,
	author={H. Hermanns and B. Wachter and L. Zhang},
	title={Probabilistic {CEGAR}},
	booktitle={CAV},
	year={2008},
	pages={162-175},
	organization={},
}
@Article{KKNP10,
	author={M. Kattenbelt and M. Kwiatkowska and G. Norman and D. Parker},
	title={A Game-based Abstraction-Refinement Framework for {Markov} Decision Processes},
	journal={Formal Methods in System Design},
	year={2010},

	volume={36},
	number={3},
	pages={246-280},
	publisher={Springer},
	month={},
	note={},
	key={}
}
@Book{MK12,
	author={Masuam and A. Kolobov},
	title={Planning with {Markov} Decision Processes: An {AI} Perspective},
	publisher={Morgan \& Claypool},
	year={2012},

	volume={},
	series={},
	address={},
	edition={},
	month={},
	note={},
	key={}
}
@Book{SB98,
	author={R. Sutton and A. Barto},
	title={Reinforcement Learning: An Introduction},
	publisher={MIT Press},
	year={1998},

	volume={},
	series={},
	address={},
	edition={},
	month={},
	note={},
	key={}
}
@Book{KSK76,
	author={J. Kemeny and J. Snell and A. Knapp},
	title={Denumerable {M}arkov Chains},
	publisher={Springer-Verlag},
	year={1976},

	volume={},
	series={},
	address={},
	_edition={2nd},
	month={},
	note={},
	key={}
}
@inproceedings{KMWG11,
	author    = {Andrey Kolobov and
	Mausam and
	Daniel S. Weld and
	Hector Geffner},
	title     = {Heuristic Search for Generalized Stochastic Shortest Path
	MDPs},
	booktitle = {ICAPS},
	year      = {2011},
	ee        = {http://aaai.org/ocs/index.php/ICAPS/ICAPS11/paper/view/2682},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

proceedings{DBLP:conf/aips/2011,
	editor    = {Fahiem Bacchus and
	Carmel Domshlak and
	Stefan Edelkamp and
	Malte Helmert},
	title     = {Proceedings of the 21st International Conference on Automated
	Planning and Scheduling, ICAPS 2011, Freiburg, Germany June
	11-16, 2011},
	booktitle = {ICAPS},
	publisher = {AAAI},
	year      = {2011},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{KNP12b,
	author={M. Kwiatkowska and G. Norman and D. Parker},
	title={The {PRISM} Benchmark Suite},
	booktitle={QEST},
	year={2012},

	editor={},
	pages={203--204},
	organization={},

}

@Unpublished{files,
	author={},
	title={},
	note={\url{http://www.prismmodelchecker.org/files/atva14learn/}},

	month={},
	year={},
	key={Zzz}
}
@InProceedings{AL12,
	author={H. Aljazzar and S. Leue},
	title={Generation of Counterexamples for Model Checking of {Markov} Decision Processes},
	booktitle={QEST},
	year={2009},

	editor={},
	pages={197--206},
	organization={},
	series={},
	volume={},
	address={},
	month={},
	note={},
	key={}
}

@inproceedings{DBLP:conf/focs/Safra88,
	author = "Safra, Shmuel",
	bibsource = "DBLP, http://dblp.uni-trier.de",
	booktitle = "{FOCS}",
	ee = "http://doi.ieeecomputersociety.org/10.1109/SFCS.1988.21948",
	pages = "319–327",
	title = "{On the Complexity of $\omega$-Automata}",
	year = "1988"
}

@inproceedings{DBLP:conf/lics/VardiW86,
	author    = {Moshe Y. Vardi and
	Pierre Wolper},
	title     = {An Automata-Theoretic Approach to Automatic Program Verification
	(Preliminary Report)},
	booktitle = {LICS},
	year      = {1986},
	pages     = {332-344},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{ CGK13,
	author = "Krishnendu Chatterjee and Andreas Gaiser and Jan K\v{r}et{\'i}nsk{\'y}",
	title = "Automata with Generalized {R}abin Pairs for Probabilistic Model Checking and {LTL} Synthesis",
	booktitle = "CAV",
	year = "2013",
	pages = "559--575"
}

@InProceedings{ KE12,
	author = "Jan K\v{r}et{\'i}nsk{\'y} and Javier Esparza",
	title = "Deterministic Automata for the ({F},{G})-Fragment of {LTL}",
	booktitle = "CAV",
	year = "2012",
	pages = "7--22",
	ee = "http://dx.doi.org/10.1007/978-3-642-31424-7\\\\\\\\\\\\\\_7",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@INPROCEEDINGS{Thomas96languages,
	author = {Wolfgang Thomas},
	title = {Languages, Automata, and Logic},
	booktitle = {Handbook of Formal Languages},
	year = {1996},
	_pages = {389--455},
}

@inproceedings{DBLP:conf/icalp/CourcoubetisY90,
	author    = {Costas Courcoubetis and
	Mihalis Yannakakis},
	title     = {Markov Decision Processes and Regular Events (Extended Abstract)},
	booktitle = {ICALP},
	year      = {1990},
	pages     = {336-349},
	ee        = {http://dx.doi.org/10.1007/BFb0032043},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{DBLP:books/daglib/0020348,
	author = "Baier, Christel and Katoen, Joost-Pieter",
	bibsource = "DBLP, http://dblp.uni-trier.de",
	isbn = "978-0-262-02649-9",
	pages = "I–XVII, 1–975",
	publisher = "MIT Press",
	title = "{Principles of model checking}",
	year = "2008"
}

% This file was created with JabRef 2.10.
% Encoding: Cp1252

% Part of abstract: We present a provably efficient and near-optimal algorithm for reinforcement learning in Markov decision processes (MDPs) whose transition model can be factored as a dynamic Bayesian network (DBN).

@inproceedings{KK99,
	author = {M. Kearns and D. Koller},
	title = {Efficient Reinforcement Learning in Factored {MDP}s},
	series = {IJCAI},
	year = {1999},
	location = {Stockholm, Sweden},
	pages = {740--747},
	numpages = {8},
	url = {http://dl.acm.org/citation.cfm?id=1624312.1624325},
	acmid = {1624325},
	publisher = {Morgan Kaufmann Publishers Inc.},
	address = {San Francisco, CA, USA},
}

%Important point: prob. STRIPS representation

@inproceedings{KHW94,
	author = {N. Kushmerick and S. Hanks and D. Weld},
	title = {An algorithm for probabilistic least-commitment planning},
	booktitle = {Proceedings of AAAI-94},
	year = {1994},
	pages = {1073--1078},
}

%Part of abstract: We present an algorithm, called structured policy iteration (SPI), that constructs optimal policies without explicit enumeration of the state space. The algorithm retains the fundamental computational steps of the commonly used modified policy iteration algorithm, but exploitsthe variable and propositionalindependencies reflected in a temporal Bayesian network representation of MDPs.

@INPROCEEDINGS{BDG95,
	author = {C. Boutilier and R. Dearden and M. Goldszmidt},
	title = {Exploiting structure in policy construction},
	booktitle = {IJCAI-95, pp.1104–1111},
	year = {1995}
}

%Representation of MDP using algebraic decision diagrams

@INPROCEEDINGS{HSHB99,
	author = {J. Hoey and R. St-aubin and A. Hu and C. Boutilier},
	title = {SPUDD: Stochastic planning using decision diagrams},
	booktitle = {In Proceedings of the Fifteenth Conference on Uncertainty in Artificial Intelligence},
	year = {1999},
	pages = {279--288},
	publisher = {Morgan Kaufmann}
}

%MTBDDs
@InProceedings{dAKNPS00,
	author={L. de Alfaro and M. Kwiatkowska and G. Norman and D. Parker and R. Segala},
	title={Symbolic Model Checking of Probabilistic Processes Using {MTBDD}s and the {K}ronecker Representation},
	booktitle={TACAS},
	year={2000},
	editor={S. Graf and M. Schwartzbach},
	pages={395--410},
	organization={},
	publisher={Springer},
	series={LNCS},
	volume={1785},
	_address={Berlin},
	_month={March},
	note={},
	key={}
}

@Article{HKNPS03,
	author={H. Hermanns and M. Kwiatkowska and G. Norman and D. Parker and M. Siegle},
	title={On the use of {MTBDD}s for Performability Analysis and Verification of Stochastic Systems},
	journal={Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems},
	year={2003},
	volume={56},
	number={1-2},
	pages={23--67},
	month={},
	note={},
	key={}
}

%decision tree repres. policies
@INPROCEEDINGS{CK91,
	author = {D. Chapman and L. P. Kaelbling},
	title = {Input generalization in delayed reinforcement learning: An algorithm and performance comparisons},
	booktitle = {},
	year = {1991},
	pages = {726--731},
	publisher = {Morgan Kaufmann}
}

@INPROCEEDINGS{KP99,
	author = {D. Koller and R. Parr},
	title = {Computing factored value functions for policies in structured {MDP}s},
	booktitle = {In Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence},
	year = {1999},
	pages = {1332--1339},
	publisher = {Morgan Kaufmann}
}

@inbook{MP04,
	author={A. Miner and D. Parker},
	chapter={Symbolic Representations and Analysis of Large Probabilistic Systems},
	title={Validation of Stochastic Systems: A Guide to Current Research},
	year={2004},
	editor={C. Baier and B. Haverkort and H. Hermanns and J-P. Katoen and M. Siegle},
	pages={296--338},
	organization={},
	publisher={Springer},
	series={Lecture Notes in Computer Science (Tutorial Volume)},
	volume={2925},
	month={},
	note={},
	key={}
}

%BDD policies

@inproceedings{WBB+10,
	author = {Wimmer, Ralf and Braitling, Bettina and Becker, Bernd and Hahn, Ernst Moritz and Crouzen, Pepijn and Hermanns, Holger and Dhama, Abhishek and Theel, Oliver},
	title = {Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems},
	booktitle = {QEST},
	year = {2010},
	isbn = {978-0-7695-4188-4},
	pages = {27--36},
	numpages = {10},
	url = {http://dx.doi.org/10.1109/QEST.2010.12},
	doi = {10.1109/QEST.2010.12},
	acmid = {1906834},
	publisher = {IEEE Computer Society},
	address = {Washington, DC, USA},
	keywords = {Markov decision processes, long-run average rewards, lumping, symbolic methods},
}

% Survey of EVERYTHING! :-)

@ARTICLE{BDH99,
	author = {C. Boutilier and T. Dean and S. Hanks},
	title = {Decision-Theoretic Planning: Structural Assumptions and Computational Leverage},
	journal = {JAIR},
	year = {1999},
	volume = {11},
	pages = {1--94}
}

@INPROCEEDINGS{BD96,
	author = {C. Boutilier and R. Dearden},
	title = {Approximating value trees in structured dynamic programming},
	booktitle = {In Proceedings of the Thirteenth International Conference on Machine Learning},
	year = {1996},
	pages = {54--62}
}

%Decision trees in reinforcement learning

@inproceedings{DBLP:conf/appinf/Pyeatt03,
	author    = {Larry D. Pyeatt},
	title     = {Reinforcement Learning with Decision Trees},
	booktitle = {The 21st {IASTED} International Multi-Conference on Applied Informatics
	{(AI} 2003), February 10-13, 2003, Innsbruck, Austria},
	pages     = {26--31},
	year      = {2003},
	timestamp = {Tue, 15 Jul 2003 16:03:54 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/appinf/Pyeatt03},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/appinf/2003,
	editor    = {M. H. Hamza},
	title     = {The 21st {IASTED} International Multi-Conference on Applied Informatics
	{(AI} 2003), February 10-13, 2003, Innsbruck, Austria},
	publisher = {{IASTED/ACTA} Press},
	year      = {2003},
	isbn      = {0-88986-345-8},
	timestamp = {Tue, 15 Jul 2003 16:03:54 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/appinf/2003},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

%Decision trees learning policy

@INPROCEEDINGS{LPRT10,
	author = {S. Liu, A. Panangadan, C. S. Raghavendra, and A. Talukder},
	title = {Compact representation of coordinated sampling policies for body sensor networks},
	booktitle = {In Proceedings of Workshop on Advances in Communication and Networks (Smart Homes for Tele-Health)},
	publisher = {IEEE},
	year = {2010},
	pages = {6--10}
}

%Counterexamples

% Journal paper 2014 (Katoen et al), SMT & MILP

@article{WJAKB14,
	author    = {R. Wimmer and
	N. Jansen and
	E. {\'{A}}brah{\'{a}}m and
	J.{-}P. Katoen and
	B. Becker},
	title     = {Minimal counterexamples for linear-time probabilistic verification},
	journal   = {TCS},
	volume    = {549},
	pages     = {61--100},
	year      = {2014},
	url       = {http://dx.doi.org/10.1016/j.tcs.2014.06.020},
	doi       = {10.1016/j.tcs.2014.06.020},
	timestamp = {Thu, 18 Sep 2014 10:13:13 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tcs/WimmerJAKB14},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DJWAK14,
	author    = {C. Dehnert and
	N. Jansen and
	R. Wimmer and
	E. {\'{A}}brah{\'{a}}m and
	J.{-}P. Katoen},
	title     = {Fast Debugging of {PRISM} Models},
	booktitle = {Automated Technology for Verification and Analysis - 12th International
	Symposium, {ATVA} 2014, Sydney, NSW, Australia, November 3-7, 2014,
	Proceedings},
	pages     = {146--162},
	year      = {2014},
	crossref  = {DBLP:conf/atva/2014},
	url       = {http://dx.doi.org/10.1007/978-3-319-11936-6_11},
	doi       = {10.1007/978-3-319-11936-6_11},
	timestamp = {Mon, 03 Nov 2014 14:32:36 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/DehnertJWAK14},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/atva/2014,
	editor    = {Franck Cassez and
	Jean{-}Fran{\c{c}}ois Raskin},
	title     = {Automated Technology for Verification and Analysis - 12th International
	Symposium, {ATVA} 2014, Sydney, NSW, Australia, November 3-7, 2014,
	Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {8837},
	publisher = {Springer},
	year      = {2014},
	url       = {http://dx.doi.org/10.1007/978-3-319-11936-6},
	doi       = {10.1007/978-3-319-11936-6},
	isbn      = {978-3-319-11935-9},
	timestamp = {Mon, 03 Nov 2014 14:29:05 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/2014},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{KH09,
	author    = {M. Kattenbelt and
	M. Huth},
	title     = {Verification and Refutation of Probabilistic Specifications via Games},
	booktitle = {{IARCS} Annual Conference on Foundations of Software Technology and
	Theoretical Computer Science, {FSTTCS} 2009, December 15-17, 2009,
	{IIT} Kanpur, India},
	pages     = {251--262},
	year      = {2009},
	url       = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2009.2323},
	doi       = {10.4230/LIPIcs.FSTTCS.2009.2323},
	timestamp = {Wed, 20 Jan 2010 11:13:33 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/fsttcs/KattenbeltH09},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fsttcs/2009,
	editor    = {Ravi Kannan and
	K. Narayan Kumar},
	title     = {{IARCS} Annual Conference on Foundations of Software Technology and
	Theoretical Computer Science, {FSTTCS} 2009, December 15-17, 2009,
	{IIT} Kanpur, India},
	series    = {LIPIcs},
	volume    = {4},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
	year      = {2009},
	isbn      = {978-3-939897-13-2},
	timestamp = {Wed, 20 Jan 2010 11:13:33 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/fsttcs/2009},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{ABDJKW14,
	author    = {E. {\'{A}}brah{\'{a}}m and
	B. Becker and
	C. Dehnert and
	N. Jansen and
	J.{-}P. Katoen and
	R. Wimmer},
	title     = {Counterexample Generation for Discrete-Time Markov Models: An Introductory
	Survey},
	booktitle = {Formal Methods for Executable Software Models - 14th International
	School on Formal Methods for the Design of Computer, Communication,
	and Software Systems, {SFM} 2014, Bertinoro, Italy, June 16-20, 2014},
	pages     = {65--121},
	year      = {2014},
	url       = {http://dx.doi.org/10.1007/978-3-319-07317-0_3},
	doi       = {10.1007/978-3-319-07317-0_3},
	timestamp = {Mon, 26 May 2014 12:24:47 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sfm/AbrahamBDJKW14},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/sfm/2014,
	editor    = {Marco Bernardo and
	Ferruccio Damiani and
	Reiner H{\"{a}}hnle and
	Einar Broch Johnsen and
	Ina Schaefer},
	title     = {Formal Methods for Executable Software Models - 14th International
	School on Formal Methods for the Design of Computer, Communication,
	and Software Systems, {SFM} 2014, Bertinoro, Italy, June 16-20, 2014,
	Advanced Lectures},
	series    = {Lecture Notes in Computer Science},
	volume    = {8483},
	publisher = {Springer},
	year      = {2014},
	url       = {http://dx.doi.org/10.1007/978-3-319-07317-0},
	doi       = {10.1007/978-3-319-07317-0},
	isbn      = {978-3-319-07316-3},
	timestamp = {Mon, 26 May 2014 12:21:35 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sfm/2014},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

%Counterexamples - Markov chains

@article{HKD09,
	author    = {T. Han and
	J.{-}P. Katoen and
	B. Damman},
	title     = {Counterexample Generation in Probabilistic Model Checking},
	journal   = {{IEEE} Trans. Software Eng.},
	volume    = {35},
	number    = {2},
	pages     = {241--257},
	year      = {2009},
	url       = {http://doi.ieeecomputersociety.org/10.1109/TSE.2009.5},
	doi       = {10.1109/TSE.2009.5},
	timestamp = {Fri, 19 Dec 2014 07:21:58 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tse/HanKD09},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{ADR08,
	author    = {M. E. Andr{\'{e}}s and
	P. R. D'Argenio and
	P. van Rossum},
	title     = {Significant Diagnostic Counterexamples in Probabilistic Model Checking},
	booktitle = {Hardware and Software: Verification and Testing, 4th International
	Haifa Verification Conference, {HVC} 2008, Haifa, Israel, October
	27-30, 2008. Proceedings},
	pages     = {129--148},
	year      = {2008},
	url       = {http://dx.doi.org/10.1007/978-3-642-01702-5_15},
	doi       = {10.1007/978-3-642-01702-5_15},
	timestamp = {Thu, 23 Apr 2009 22:35:45 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/hvc/AndresDR08},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/hvc/2008,
	editor    = {Hana Chockler and
	Alan J. Hu},
	title     = {Hardware and Software: Verification and Testing, 4th International
	Haifa Verification Conference, {HVC} 2008, Haifa, Israel, October
	27-30, 2008. Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {5394},
	publisher = {Springer},
	year      = {2009},
	url       = {http://dx.doi.org/10.1007/978-3-642-01702-5},
	doi       = {10.1007/978-3-642-01702-5},
	isbn      = {978-3-642-01701-8},
	timestamp = {Thu, 23 Apr 2009 22:32:13 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/hvc/2008},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{JAKWKB11,
	author    = {N. Jansen and
	E. {\'{A}}brah{\'{a}}m and
	J. Katelaan and
	R. Wimmer and
	J.{-}P. Katoen and
	B. Becker},
	title     = {Hierarchical Counterexamples for Discrete-Time Markov Chains},
	booktitle = {Automated Technology for Verification and Analysis, 9th International
	Symposium, {ATVA} 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings},
	pages     = {443--452},
	year      = {2011},
	crossref  = {DBLP:conf/atva/2011},
	url       = {http://dx.doi.org/10.1007/978-3-642-24372-1_33},
	doi       = {10.1007/978-3-642-24372-1_33},
	timestamp = {Fri, 14 Oct 2011 20:11:29 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/JansenAKWKB11},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/atva/2011,
	editor    = {Tevfik Bultan and
	Pao{-}Ann Hsiung},
	title     = {Automated Technology for Verification and Analysis, 9th International
	Symposium, {ATVA}, Taipei, Taiwan, October 11-14, 2011. Proceedings},
	series    = {LNCS},
	volume    = {6996},
	publisher = {Springer},
	year      = {2011},
	url       = {http://dx.doi.org/10.1007/978-3-642-24372-1},
	doi       = {10.1007/978-3-642-24372-1},
	isbn      = {978-3-642-24371-4},
	timestamp = {Fri, 14 Oct 2011 20:11:00 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/2011},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DHKK08,
	author    = {B. Damman and
	T. Han and
	J.{-}P. Katoen},
	title     = {Regular Expressions for {PCTL} Counterexamples},
	booktitle = {
	QEST},
	pages     = {179--188},
	year      = {2008},
	crossref  = {DBLP:conf/qest/2008},
	url       = {http://dx.doi.org/10.1109/QEST.2008.11},
	doi       = {10.1109/QEST.2008.11},
	timestamp = {Fri, 19 Dec 2014 07:21:57 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/qest/DammanHK08},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/qest/2008,
	title     = {Fifth International Conference on the Quantitative Evaluaiton of Systems
	{(QEST} 2008), 14-17 September 2008, Saint-Malo, France},
	publisher = {{IEEE} Computer Society},
	year      = {2008},
	url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=4634932},
	isbn      = {978-0-7695-3360-5},
	timestamp = {Fri, 08 Aug 2014 15:28:23 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/qest/2008},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{FHPW10,
	author    = {H. Fecher and
	M. Huth and
	N. Piterman and
	D. Wagner},
	title     = {{PCTL} model checking of Markov chains: Truth and falsity as winning
	strategies in games},
	journal   = {Perform. Eval.},
	volume    = {67},
	number    = {9},
	pages     = {858--872},
	year      = {2010},
	url       = {http://dx.doi.org/10.1016/j.peva.2009.07.002},
	doi       = {10.1016/j.peva.2009.07.002},
	timestamp = {Thu, 16 Sep 2010 09:55:51 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/pe/FecherHPW10},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{KPC12,
	author    = {A. Komuravelli and
	C. S. Pasareanu and
	E. M. Clarke},
	title     = {Assume-Guarantee Abstraction Refinement for Probabilistic Systems},
	booktitle = {CAV},
	pages     = {310--326},
	year      = {2012},
	url       = {http://dx.doi.org/10.1007/978-3-642-31424-7_25},
	doi       = {10.1007/978-3-642-31424-7_25},
	timestamp = {Tue, 03 Jul 2012 08:52:37 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/KomuravelliPC12},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cav/2012,
	editor    = {P. Madhusudan and
	Sanjit A. Seshia},
	title     = {Computer Aided Verification - 24th International Conference, {CAV}
	2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {7358},
	publisher = {Springer},
	year      = {2012},
	url       = {http://dx.doi.org/10.1007/978-3-642-31424-7},
	doi       = {10.1007/978-3-642-31424-7},
	isbn      = {978-3-642-31423-0},
	timestamp = {Tue, 03 Jul 2012 08:38:09 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/2012},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{ALLS11,
	author              = {H. Aljazzar and
	F. Leitner-Fischer and
	S. Leue and
	D. Simeonov},
	title               = {DiPro - A Tool for Probabilistic Counterexample Generation.},
	booktitle           = {SPIN},
	year                = {2011},
	pages               = {183-187},
	ee                  = {http://dx.doi.org/10.1007/978-3-642-22306-8_13},
	crossref            = {2011},
}
@proceedings{DBLP:conf/spin/2011,
	editor    = {Alex Groce and
	Madanlal Musuvathi},
	title     = {Model Checking Software - 18th International {SPIN} Workshop, Snowbird,
	UT, USA, July 14-15, 2011. Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {6823},
	publisher = {Springer},
	year      = {2011},
	url       = {http://dx.doi.org/10.1007/978-3-642-22306-8},
	doi       = {10.1007/978-3-642-22306-8},
	isbn      = {978-3-642-22305-1},
	timestamp = {Mon, 11 Jul 2011 14:46:19 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/spin/2011},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{JAVWKB12,
	author    = {N. Jansen and
	E. {\'{A}}brah{\'{a}}m and
	M. Volk and
	R. Wimmer and
	J.{-}P. Katoen and
	B. Becker},
	title     = {The {COMICS} Tool - Computing Minimal Counterexamples for DTMCs},
	booktitle = {{ATVA}},
	pages     = {349--353},
	year      = {2012},
	url       = {http://dx.doi.org/10.1007/978-3-642-33386-6_27},
	doi       = {10.1007/978-3-642-33386-6_27},
	timestamp = {Sun, 14 Oct 2012 17:23:28 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/JansenAVWKB12},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/atva/2012,
	editor    = {Supratik Chakraborty and
	Madhavan Mukund},
	title     = {Automated Technology for Verification and Analysis - 10th International
	Symposium, {ATVA} 2012, Thiruvananthapuram, India, October 3-6, 2012.
	Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {7561},
	publisher = {Springer},
	year      = {2012},
	url       = {http://dx.doi.org/10.1007/978-3-642-33386-6},
	doi       = {10.1007/978-3-642-33386-6},
	isbn      = {978-3-642-33385-9},
	timestamp = {Sun, 14 Oct 2012 17:14:43 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/2012},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{AL09,
	author    = {Husain Aljazzar and
	Stefan Leue},
	title     = {Generation of Counterexamples for Model Checking of Markov Decision
	Processes},
	booktitle = {{QEST}},
	pages     = {197--206},
	year      = {2009},
	crossref  = {DBLP:conf/qest/2009},
	url       = {http://dx.doi.org/10.1109/QEST.2009.10},
	doi       = {10.1109/QEST.2009.10},
	timestamp = {Fri, 08 Aug 2014 15:28:23 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/qest/AljazzarL09},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/qest/2009,
	title     = {{QEST} 2009, Sixth International Conference on the Quantitative Evaluation
	of Systems, Budapest, Hungary, 13-16 September 2009},
	publisher = {{IEEE} Computer Society},
	year      = {2009},
	url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5290656},
	isbn      = {978-0-7695-3808-2},
	timestamp = {Fri, 08 Aug 2014 15:28:22 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/qest/2009},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{AL11,
	author    = {Husain Aljazzar and
	Stefan Leue},
	title     = {K*: {A} heuristic search algorithm
	for finding the k shortest paths},
	journal   = {Artif. Intell.},
	volume    = {175},
	number    = {18},
	pages     = {2129--2154},
	year      = {2011},
	url       = {http://dx.doi.org/10.1016/j.artint.2011.07.003},
	doi       = {10.1016/j.artint.2011.07.003},
	timestamp = {Fri, 23 Sep 2011 01:00:00 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/ai/AljazzarL11},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/spin/AljazzarLLS11,
	author    = {Husain Aljazzar and
	Florian Leitner{-}Fischer and
	Stefan Leue and
	Dimitar Simeonov},
	title     = {DiPro - {A} Tool for Probabilistic Counterexample Generation},
	booktitle = {Model Checking Software - 18th International {SPIN} Workshop, Snowbird,
	UT, USA, July 14-15, 2011. Proceedings},
	pages     = {183--187},
	year      = {2011},
	crossref  = {DBLP:conf/spin/2011},
	url       = {http://dx.doi.org/10.1007/978-3-642-22306-8_13},
	doi       = {10.1007/978-3-642-22306-8_13},
	timestamp = {Mon, 11 Jul 2011 14:46:19 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/spin/AljazzarLLS11},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{AL10,
	author    = {Husain Aljazzar and
	Stefan Leue},
	title     = {Directed Explicit State-Space Search in the Generation of Counterexamples
	for Stochastic Model Checking},
	journal   = {{IEEE} Trans. Software Eng.},
	volume    = {36},
	number    = {1},
	pages     = {37--60},
	year      = {2010},
	url       = {http://doi.ieeecomputersociety.org/10.1109/TSE.2009.57},
	doi       = {10.1109/TSE.2009.57},
	timestamp = {Tue, 02 Feb 2010 13:56:49 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tse/AljazzarL10},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{LL13,
	author    = {F. Leitner{-}Fischer and
	S. Leue},
	title     = {Probabilistic fault tree synthesis using causality computation},
	journal   = {{IJCCBS}},
	volume    = {4},
	number    = {2},
	pages     = {119--143},
	year      = {2013},
	url       = {http://dx.doi.org/10.1504/IJCCBS.2013.056492},
	doi       = {10.1504/IJCCBS.2013.056492},
	timestamp = {Fri, 15 Nov 2013 09:32:57 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/ijccbs/Leitner-FischerL13},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

% This file was created with JabRef 2.10.
% Encoding: Cp1252

@InProceedings{AL12,
	Title                    = {Generation of Counterexamples for Model Checking of {Markov} Decision Processes},
	Author                   = {H. Aljazzar and S. Leue},
	Booktitle                = {QEST},
	Year                     = {2009},
	Pages                    = {197--206}
}

@Article{AV79,
	Title                    = {Fast probabilistic algorithms for Hamiltonian circuits and matchings},
	Author                   = {Angluin, Dana and Valiant, Leslie G},
	Journal                  = {Journal of Computer and system Sciences},
	Year                     = {1979},
	Number                   = {2},
	Pages                    = {155-193},
	Volume                   = {18},

	Publisher                = {Elsevier}
}

@InProceedings{BCHG+97,
	Title                    = {Symbolic Model Checking for Probabilistic Processes},
	Author                   = {C. Baier and E. Clarke and V. Hartonas-Garmhausen and M. Kwiatkowska and M. Ryan},
	Booktitle                = {ICALP},
	Year                     = {1997},
	Pages                    = {430--440},

	_editor                  = {P. Degano and R. Gorrieri and A. Marchetti-Spaccamela}
}

@Book{DBLP:books/daglib/0020348,
	Title                    = {{Principles of model checking}},
	Author                   = {Baier, Christel and Katoen, Joost-Pieter},
	Publisher                = {MIT Press},
	Year                     = {2008},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	ISBN                     = {978-0-262-02649-9},
	Pages                    = {I–XVII, 1–975}
}

@InProceedings{DBLP:conf/tacas/BarbotHP12,
	Title                    = {Coupling and Importance Sampling for Statistical Model Checking},
	Author                   = {Beno\^{\i}t Barbot and Serge Haddad and Claudine Picaronny},
	Booktitle                = {TACAS},
	Year                     = {2012},
	Pages                    = {331--346},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://dx.doi.org/10.1007/978-3-642-28756-5\\\\_23}
}

@Article{BBS95,
	Title                    = {Learning to act using real-time dynamic programming },
	Author                   = {Andrew G. Barto and Steven J. Bradtke and Satinder P. Singh},
	Journal                  = {Artificial Intelligence },
	Year                     = {1995},
	Number                   = {1–2},
	Pages                    = {81 - 138},
	Volume                   = {72},

	Doi                      = {http://dx.doi.org/10.1016/0004-3702(94)00011-O},
	ISSN                     = {0004-3702}
}

@InProceedings{BdA95,
	Title                    = {Model Checking of Probabilistic and Nondeterministic Systems},
	Author                   = {A. Bianco and L. de Alfaro},
	Booktitle                = {FSTTCS},
	Year                     = {1995},
	Pages                    = {499--513},

	_editor                  = {P. Thiagarajan}
}

@InProceedings{BHH12,
	Title                    = {Simulation and Statistical Model Checking for Modestly Nondeterministic
	Models},
	Author                   = {Jonathan Bogdoll and
	Arnd Hartmanns and
	Holger Hermanns},
	Booktitle                = {MMB/DFT},
	Year                     = {2012},
	Pages                    = {249-252}
}

@InProceedings{BG03,
	Title                    = {Labeled {RTDP}: Improving the Convergence of Real-Time Dynamic Programming},
	Author                   = {Bonet, Blai and Geffner, Hector},
	Booktitle                = {ICAPS},
	Year                     = {2003},
	Pages                    = {12-21}
}

@Article{arxiv,
	Title                    = {Verification of {M}arkov Decision Processes using Learning
	Algorithms},
	Author                   = {Tom{\'a}\v{s} Br{\'a}zdil and
	Krishnendu Chatterjee and
	Martin Chmel\i{i}k and
	Vojt\v{e}ch Forejt and
	Jan K\v{r}et\'{\i}nsk{\'y} and
	Marta Z. Kwiatkowska and
	David Parker and
	Mateusz Ujma},
	Journal                  = {CoRR},
	Year                     = {2014},
	Volume                   = {abs/1402.2967},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://arxiv.org/abs/1402.2967}
}

@InProceedings{BKK11,
	Title                    = {Efficient analysis of probabilistic programs with an unbounded counter},
	Author                   = {Br{\'a}zdil, Tom{\'a}{\v{s}} and Kiefer, Stefan and Ku{\v{c}}era, Anton{\'\i}n},
	Booktitle                = {CAV},
	Year                     = {2011},
	Pages                    = {208--224}
}

@Article{CGKM12,
	Title                    = {Self-adaptive software needs quantitative verification at runtime},
	Author                   = {R. Calinescu and C. Ghezzi and M. Kwiatkowska and R. Mirandola},
	Journal                  = {Communications of the ACM},
	Year                     = {2012},
	Number                   = {9},
	Pages                    = {69-77 },
	Volume                   = {55},

	Publisher                = {ACM}
}

@InProceedings{CGK13,
	Title                    = {Automata with Generalized {R}abin Pairs for Probabilistic Model Checking and {LTL} Synthesis},
	Author                   = {Krishnendu Chatterjee and Andreas Gaiser and Jan K\v{r}et{\'i}nsk{\'y}},
	Booktitle                = {CAV},
	Year                     = {2013},
	Pages                    = {559--575}
}

@InProceedings{CH12,
	Title                    = {An {O}$(n^2)$ Algorithm for Alternating {B}{\"u}chi Games},
	Author                   = {K. Chatterjee and M. Henzinger},
	Booktitle                = {SODA},
	Year                     = {2012},
	Pages                    = {1386-1399}
}

@InProceedings{CH11,
	Title

repository: kushgrover/apt-vs-dift

repo_name: kushgrover/apt-vs-dift