text:
= {Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification},
	Author                   = {Chatterjee, Krishnendu and Henzinger, Monika},
	Booktitle                = {SODA},
	Year                     = {2011},

	_pages                   = {1318--1336}
}

@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},
	Year                     = {2008},
	Pages                    = {45--54}
}

@InProceedings{DBLP:conf/icalp/CourcoubetisY90,
	Title                    = {Markov Decision Processes and Regular Events (Extended Abstract)},
	Author                   = {Costas Courcoubetis and
	Mihalis Yannakakis},
	Booktitle                = {ICALP},
	Year                     = {1990},
	Pages                    = {336-349},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://dx.doi.org/10.1007/BFb0032043}
}

@InProceedings{DJJL01,
	Title                    = {Reachability analysis of probabilistic systems by successive refinements},
	Author                   = {P. D{'A}rgenio and B. Jeannet and H. Jensen and K. Larsen},
	Booktitle                = {PPAPM/PROBMIV},
	Year                     = {2001},
	Pages                    = {39--56}
}

@PhdThesis{DeA97,
	Title                    = {Formal verification of probabilistic systems},
	Author                   = {De Alfaro, Luca},
	Year                     = {1997},

	_school                  = {Stanford University}
}

@Article{Drazin2012,
	Title                    = {Decision tree analysis using WEKA},
	Author                   = {Drazin, Sam and Montag, Matt},
	Journal                  = {Machine Learning-Project II, University of Miami},
	Year                     = {2012},
	Pages                    = {1--3},

	__markedentry            = {[afellner:]},
	Owner                    = {afellner},
	Timestamp                = {2014.11.18}
}

@InProceedings{FKP11,
	Title                    = {Automated Learning of Probabilistic Assumptions for Compositional Reasoning},
	Author                   = {L. Feng and M. Kwiatkowska and D. Parker},
	Booktitle                = {FASE},
	Year                     = {2011},
	Pages                    = {2-17}
}

@InProceedings{HLMP04,
	Title                    = {Approximate Probabilistic Model Checking},
	Author                   = {T. H\'erault and R. Lassaigne and F. Magniette and S. Peyronnet},
	Booktitle                = {VMCAI},
	Year                     = {2004},
	Pages                    = {307-329}
}

@InProceedings{HNP+11,
	Title                    = {Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems},
	Author                   = {E. M. Hahn and G. Norman and D. Parker and B. Wachter and L. Zhang},
	Booktitle                = {QEST},
	Year                     = {2011},
	Pages                    = {69-78}
}

@Article{Hall2009,
	Title                    = {The WEKA data mining software: an update},
	Author                   = {Hall, Mark and Frank, Eibe and Holmes, Geoffrey and Pfahringer, Bernhard and Reutemann, Peter and Witten, Ian H},
	Journal                  = {ACM SIGKDD explorations newsletter},
	Year                     = {2009},
	Number                   = {1},
	Pages                    = {10--18},
	Volume                   = {11},

	__markedentry            = {[afellner:]},
	Owner                    = {afellner},
	Publisher                = {ACM},
	Timestamp                = {2015.01.30}
}

@InProceedings{DBLP:conf/kbse/HeJBGW10,
	Title                    = {A bounded statistical approach for model checking of unbounded until properties},
	Author                   = {Ru He and Paul Jennings and Samik Basu and Arka P. Ghosh and Huaiqing Wu},
	Booktitle                = {ASE},
	Year                     = {2010},
	Pages                    = {225--234},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://doi.acm.org/10.1145/1858996.1859043}
}

@InProceedings{HJB+10,
	Title                    = {A bounded statistical approach for model checking of unbounded until properties},
	Author                   = {Ru He and Paul Jennings and Samik Basu and Arka P. Ghosh and Huaiqing Wu},
	Booktitle                = {ASE},
	Year                     = {2010},
	Pages                    = {225--234}
}

@InProceedings{HMZ+12,
	Title                    = {Statistical Model Checking for {Markov} Decision Processes},
	Author                   = {David Henriques and
	Jo{\~a}o Martins and
	Paolo Zuliani and
	Andr{\'e} Platzer and
	Edmund M. Clarke},
	Booktitle                = {QEST},
	Year                     = {2012},
	Pages                    = {84-93},
	Publisher                = {IEEE Computer Society}
}

@InProceedings{HWZ08,
	Title                    = {Probabilistic {CEGAR}},
	Author                   = {H. Hermanns and B. Wachter and L. Zhang},
	Booktitle                = {CAV},
	Year                     = {2008},
	Pages                    = {162-175}
}

@Article{H63,
	Title                    = {Probability inequalities for sums of bounded random variables},
	Author                   = {Hoeffding, Wassily},
	Journal                  = {Journal of the American statistical association},
	Year                     = {1963},
	Number                   = {301},
	Pages                    = {13-30},
	Volume                   = {58},

	Publisher                = {Taylor \& Francis Group}
}

@InProceedings{DBLP:conf/cav/JegourelLS13,
	Title                    = {Importance Splitting for Statistical Model Checking Rare Properties},
	Author                   = {Cyrille J{\'e}gourel and Axel Legay and Sean Sedwards},
	Booktitle                = {CAV},
	Year                     = {2013},
	Pages                    = {576--591},

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

@InProceedings{DBLP:conf/cav/JegourelLS12,
	Title                    = {Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking},
	Author                   = {Cyrille J{\'e}gourel and Axel Legay and Sean Sedwards},
	Booktitle                = {CAV},
	Year                     = {2012},
	Pages                    = {327--342},

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

@InProceedings{KE12,
	Title                    = {Deterministic Automata for the ({F},{G})-Fragment of {LTL}},
	Author                   = {Jan K\v{r}et{\'i}nsk{\'y} and Javier Esparza},
	Booktitle                = {CAV},
	Year                     = {2012},
	Pages                    = {7--22},

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

@Article{KKNP10,
	Title                    = {A Game-based Abstraction-Refinement Framework for {Markov} Decision Processes},
	Author                   = {M. Kattenbelt and M. Kwiatkowska and G. Norman and D. Parker},
	Journal                  = {Formal Methods in System Design},
	Year                     = {2010},
	Number                   = {3},
	Pages                    = {246-280},
	Volume                   = {36},

	Publisher                = {Springer}
}

@Book{KSK76,
	Title                    = {Denumerable {M}arkov Chains},
	Author                   = {J. Kemeny and J. Snell and A. Knapp},
	Publisher                = {Springer-Verlag},
	Year                     = {1976},

	_edition                 = {2nd}
}

@InProceedings{KMWG11,
	Title                    = {Heuristic Search for Generalized Stochastic Shortest Path
	MDPs},
	Author                   = {Andrey Kolobov and
	Mausam and
	Daniel S. Weld and
	Hector Geffner},
	Booktitle                = {ICAPS},
	Year                     = {2011},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://aaai.org/ocs/index.php/ICAPS/ICAPS11/paper/view/2682}
}

@InProceedings{KNP12b,
	Title                    = {The {PRISM} Benchmark Suite},
	Author                   = {M. Kwiatkowska and G. Norman and D. Parker},
	Booktitle                = {QEST},
	Year                     = {2012},
	Pages                    = {203--204}
}

@InProceedings{KNP11,
	Title                    = {{PRISM} 4.0: Verification of Probabilistic Real-time Systems},
	Author                   = {M. Kwiatkowska and G. Norman and D. Parker},
	Booktitle                = {CAV},
	Year                     = {2011},
	Pages                    = {585-591}
}

@Article{KNPS06,
	Title                    = {Performance Analysis of Probabilistic Timed Automata using Digital Clocks},
	Author                   = {M. Kwiatkowska and G. Norman and D. Parker and J. Sproston},
	Journal                  = {Formal Methods in System Design},
	Year                     = {2006},
	Pages                    = {33-78},
	Volume                   = {29}
}

@InProceedings{KNS01a,
	Title                    = {Automated Verification of a Randomized Distributed Consensus Protocol Using {Cadence SMV} and {PRISM}},
	Author                   = {M. Kwiatkowska and G. Norman and R. Segala},
	Booktitle                = {CAV},
	Year                     = {2001},
	Pages                    = {194--206}
}

@Article{KNS03b,
	Title                    = {Probabilistic Model Checking of Deadline Properties in the {IEEE 1394 FireWire} Root Contention Protocol},
	Author                   = {M. Kwiatkowska and G. Norman and J. Sproston},
	Journal                  = {Formal Aspects of Computing},
	Year                     = {2003},
	Number                   = {3},
	Pages                    = {295--318},
	Volume                   = {14},

	_month                   = {April}
}

@InProceedings{KNS02a,
	Title                    = {Probabilistic Model Checking of the {IEEE} 802.11 Wireless Local Area Network Protocol},
	Author                   = {M. Kwiatkowska and G. Norman and J. Sproston},
	Booktitle                = {PAPM/PROBMIV},
	Year                     = {2002},
	Pages                    = {169--187},
	Publisher                = {Springer}
}

@InCollection{Kwiatkowska2013,
	Title                    = {Automated verification and strategy synthesis for probabilistic systems},
	Author                   = {Kwiatkowska, Marta and Parker, David},
	Booktitle                = {Automated Technology for Verification and Analysis},
	Publisher                = {Springer},
	Year                     = {2013},
	Pages                    = {5--22},

	__markedentry            = {[afellner:6]},
	Owner                    = {afellner},
	Timestamp                = {2015.02.08}
}

@InProceedings{DBLP:conf/sac/LassaigneP12,
	Title                    = {Approximate planning and verification for large {Markov} decision processes},
	Author                   = {Richard Lassaigne and Sylvain Peyronnet},
	Booktitle                = {SAC},
	Year                     = {2012},
	Pages                    = {1314--1319},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://doi.acm.org/10.1145/2245276.2231984}
}

@Article{DBLP:journals/corr/LegayS13,
	Title                    = {Lightweight {Monte} {Carlo} Algorithm for {Markov} Decision Processes},
	Author                   = {Axel Legay and Sean Sedwards},
	Journal                  = {CoRR},
	Year                     = {2013},
	Volume                   = {abs/1310.3609},

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

@Book{MK12,
	Title                    = {Planning with {Markov} Decision Processes: An {AI} Perspective},
	Author                   = {Masuam and A. Kolobov},
	Publisher                = {Morgan \& Claypool},
	Year                     = {2012}
}

@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},
	Year                     = {2005},

	_pages                   = {569--576}
}

@Book{Mitchell1997,
	Title                    = {Machine Learning},
	Author                   = {Thomas M. Mitchell},
	Publisher                = {McGraw-Hill, Inc.},
	Year                     = {1997},

	Address                  = {New York, NY, USA},
	Edition                  = {1},

	ISBN                     = {0070428077, 9780070428072}
}

@Book{Quinlan93,
	Title                    = {{C4.5:} Programs for Machine Learning},
	Author                   = {J. Ross Quinlan},
	Publisher                = {Morgan Kaufmann},
	Year                     = {1993},

	Bibsource                = {dblp computer science bibliography, http://dblp.org},
	Biburl                   = {http://dblp.uni-trier.de/rec/bib/books/mk/Quinlan93},
	ISBN                     = {1-55860-238-0},
	Owner                    = {afellner},
	Timestamp                = {Fri, 14 Nov 2014 12:54:33 +0100}
}

@Article{Quin86,
	Title                    = {Induction of Decision Trees},
	Author                   = {J. Ross Quinlan},
	Journal                  = {Mach. Learn.},
	Year                     = {1986},
	Number                   = {1},
	Pages                    = {81--106},
	Volume                   = {1}
}

@InProceedings{RP09,
	Title                    = {Statistical model checking using perfect simulation},
	Author                   = {D. E. Rabih and N. Pekergin},
	Booktitle                = {ATVA},
	Year                     = {2009},
	Pages                    = {120--134}
}

@InProceedings{DBLP:conf/focs/Safra88,
	Title                    = {{On the Complexity of $\omega$-Automata}},
	Author                   = {Safra, Shmuel},
	Booktitle                = {{FOCS}},
	Year                     = {1988},
	Pages                    = {319–327},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://doi.ieeecomputersociety.org/10.1109/SFCS.1988.21948}
}

@InProceedings{SVA05,
	Title                    = {On statistical model checking of stochastic systems},
	Author                   = {K. Sen and M. Viswanathan and G. Agha},
	Booktitle                = {CAV},
	Year                     = {2005},
	Pages                    = {266--280}
}

@InProceedings{DBLP:conf/cav/SenVA04,
	Title                    = {Statistical Model Checking of Black-Box Probabilistic Systems},
	Author                   = {Koushik Sen and Mahesh Viswanathan and Gul Agha},
	Booktitle                = {CAV},
	Year                     = {2004},
	Pages                    = {202--215},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://dx.doi.org/10.1007/978-3-540-27813-9\\\\_16}
}

@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{Thomas96languages,
	Title                    = {Languages, Automata, and Logic},
	Author                   = {Wolfgang Thomas},
	Booktitle                = {Handbook of Formal Languages},
	Year                     = {1996},

	_pages                   = {389--455}
}

@InProceedings{Var85,
	Title                    = {Automatic Verification of Probabilistic Concurrent Finite State Programs},
	Author                   = {M. Vardi},
	Booktitle                = {FOCS},
	Year                     = {1985},
	Pages                    = {327--338}
}

@InProceedings{DBLP:conf/lics/VardiW86,
	Title                    = {An Automata-Theoretic Approach to Automatic Program Verification
	(Preliminary Report)},
	Author                   = {Moshe Y. Vardi and
	Pierre Wolper},
	Booktitle                = {LICS},
	Year                     = {1986},
	Pages                    = {332-344},

	Bibsource                = {DBLP, http://dblp.uni-trier.de}
}

InProceedings{YCZ10,
	Title                    = {Statistical verification of probabilistic properties with unbounded until},
	Author                   = {Haakan Younes and Edmund M. Clarke and Paolo Zuliani},
	Booktitle                = {SBMF},
	Year                     = {2010},
	Pages                    = {144--160}
}

InProceedings{DBLP:conf/sbmf/YounesCZ10,
	Title                    = {Statistical Verification of Probabilistic Properties with Unbounded Until},
	Author                   = {H{\aa}kan L. S. Younes and Edmund M. Clarke and Paolo Zuliani},
	Booktitle                = {SBMF},
	Year                     = {2010},
	Pages                    = {144--160},

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

@InProceedings{DBLP:conf/tacas/YounesKNP04,
	Title                    = {Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study},
	Author                   = {H{\aa}kan L. S. Younes and Marta Z. Kwiatkowska and Gethin Norman and David Parker},
	Booktitle                = {TACAS},
	Year                     = {2004},
	Pages                    = {46--60},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://dx.doi.org/10.1007/978-3-540-24730-2\\\\_4}
}

@InProceedings{DBLP:conf/cav/YounesS02,
	Title                    = {Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling},
	Author                   = {H{\aa}kan L. S. Younes and Reid G. Simmons},
	Booktitle                = {CAV},
	Year                     = {2002},
	Pages                    = {223--235},

	Bibsource                = {DBLP, http://dblp.uni-trier.de},
	Ee                       = {http://dx.doi.org/10.1007/3-540-45657-0\\\_17}
}

@Proceedings{DBLP:conf/atva/2014,
	Title                    = {Automated Technology for Verification and Analysis - 12th International
	Symposium, {ATVA} 2014, Sydney, NSW, Australia, November 3-7, 2014,
	Proceedings},
	Year                     = {2014},
	Editor                   = {Franck Cassez and
	Jean{-}Fran{\c{c}}ois Raskin},
	Publisher                = {Springer},
	Series                   = {Lecture Notes in Computer Science},
	Volume                   = {8837},

	Bibsource                = {dblp computer science bibliography, http://dblp.org},
	Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/atva/2014},
	Doi                      = {10.1007/978-3-319-11936-6},
	ISBN                     = {978-3-319-11935-9},
	Timestamp                = {Mon, 03 Nov 2014 14:29:05 +0100},
	Url                      = {http://dx.doi.org/10.1007/978-3-319-11936-6}
}

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

	Key                      = {Zzz}
}

@article{DBLP:journals/sttt/DavidLLMP15,
	author    = {Alexandre David and
	Kim G. Larsen and
	Axel Legay and
	Marius Mikucionis and
	Danny B{\o}gsted Poulsen},
	title     = {Uppaal {SMC} tutorial},
	journal   = {{STTT}},
	volume    = {17},
	number    = {4},
	pages     = {397--415},
	year      = {2015},
	url       = {http://dx.doi.org/10.1007/s10009-014-0361-y},
	doi       = {10.1007/s10009-014-0361-y},
	timestamp = {Tue, 07 Jul 2015 11:08:47 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/sttt/DavidLLMP15},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@proceedings{DBLP:conf/cmsb/2009,
	editor    = {Pierpaolo Degano and
	Roberto Gorrieri},
	title     = {Computational Methods in Systems Biology, 7th International Conference,
	{CMSB} 2009, Bologna, Italy, August 31-September 1, 2009. Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = 5688,
	publisher = {Springer},
	year      = 2009,
	url       = {http://dx.doi.org/10.1007/978-3-642-03845-7},
	doi       = {10.1007/978-3-642-03845-7},
	isbn      = {978-3-642-03844-0},
	timestamp = {Mon, 12 Oct 2009 22:04:43 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cmsb/2009},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{BK08,
	author    = {Christel Baier and
	Joost{-}Pieter Katoen},
	title     = {Principles of model checking},
	publisher = {{MIT} Press},
	year      = {2008},
	isbn      = {978-0-262-02649-9},
	timestamp = {Tue, 15 Feb 2011 11:22:37 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/books/daglib/0020348},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{wald1945sequential,
	title={Sequential tests of statistical hypotheses},
	author={Wald, Abraham},
	journal={The Annals of Mathematical Statistics},
	volume={16},
	number={2},
	pages={117--186},
	year={1945},
	publisher={JSTOR}
}

@article{DBLP:journals/apal/LassaigneP08,
	author    = {Richard Lassaigne and
	Sylvain Peyronnet},
	title     = {Probabilistic verification and approximation},
	journal   = {Ann. Pure Appl. Logic},
	volume    = {152},
	number    = {1-3},
	pages     = {122--131},
	year      = {2008},
	url       = {http://dx.doi.org/10.1016/j.apal.2007.11.006},
	doi       = {10.1016/j.apal.2007.11.006},
	timestamp = {Wed, 29 Oct 2008 14:53:35 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/apal/LassaigneP08},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{pnueli1977temporal,
	title={The temporal logic of programs},
	author={Pnueli, Amir},
	booktitle={FOCS},
	pages={46--57},
	year={1977},
}

@article{solan2003continuity,
	title={Continuity of the value of competitive {M}arkov decision processes},
	author={Solan, Eilon},
	journal={Journal of Theoretical Probability},
	volume={16},
	number={4},
	pages={831--845},
	year={2003},
	publisher={Springer}
}

@book{norris1998markov,
	title={Markov chains},
	author={Norris, James R},
	year={1998},
	publisher={Cambridge university press}
}

@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},
	series    = {{EPTCS}},
	volume    = {85},
	year      = {2012},
	url       = {http://dx.doi.org/10.4204/EPTCS.85},
	doi       = {10.4204/EPTCS.85},
	timestamp = {Mon, 28 Oct 2013 16:56:55 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1207-0559},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/sttt/YounesKNP06,
	author    = {H{\aa}kan L. S. Younes and
	Marta Z. Kwiatkowska and
	Gethin Norman and
	David Parker},
	title     = {Numerical vs. statistical probabilistic model checking},
	journal   = {{STTT}},
	volume    = {8},
	number    = {3},
	pages     = {216--228},
	year      = {2006},
	url       = {http://dx.doi.org/10.1007/s10009-005-0187-8},
	doi       = {10.1007/s10009-005-0187-8},
	timestamp = {Wed, 07 Feb 2007 07:57:06 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/sttt/YounesKNP06},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/tacas/JegourelLS12,
	author    = {Cyrille J{\'{e}}gourel and
	Axel Legay and
	Sean Sedwards},
	title     = {A Platform for High Performance Statistical Model Checking - {PLASMA}},
	booktitle = {TACAS},
	pages     = {498--503},
	year      = {2012},
	url       = {http://dx.doi.org/10.1007/978-3-642-28756-5_37},
	doi       = {10.1007/978-3-642-28756-5_37},
	timestamp = {Wed, 07 Jan 2015 18:21:20 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tacas/JegourelLS12},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}  crossref  = {DBLP:conf/tacas/2012},
@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},
	series    = {Lecture Notes in Computer Science},
	volume    = {7214},
	publisher = {Springer},
	year      = {2012},
	url       = {http://dx.doi.org/10.1007/978-3-642-28756-5},
	doi       = {10.1007/978-3-642-28756-5},
	isbn      = {978-3-642-28755-8},
	timestamp = {Wed, 07 Jan 2015 18:21:20 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tacas/2012},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{sbmf11,
	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},
	pages     = {144--160},
	year      = 2010,
	url       = {http://dx.doi.org/10.1007/978-3-642-19829-8_10},
	doi       = {10.1007/978-3-642-19829-8_10},
	timestamp = {Tue, 22 Mar 2011 09:38:31 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sbmf/YounesCZ10},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}  crossref  = {DBLP:conf/sbmf/2010},

@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},
	series    = {Lecture Notes in Computer Science},
	volume    = {6527},
	publisher = {Springer},
	year      = {2011},
	url       = {http://dx.doi.org/10.1007/978-3-642-19829-8},
	doi       = {10.1007/978-3-642-19829-8},
	isbn      = {978-3-642-19828-1},
	timestamp = {Tue, 22 Mar 2011 09:36:28 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/sbmf/2010},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{ase10,
	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}},
	pages     = {225--234},
	year      = {2010},
	url       = {http://doi.acm.org/10.1145/1858996.1859043},
	doi       = {10.1145/1858996.1859043},
	timestamp = {Sat, 25 Sep 2010 13:52:22 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/kbse/HeJBGW10},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@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},
	publisher = {{ACM}},
	year      = {2010},
	isbn      = {978-1-4503-0116-9},
	timestamp = {Sat, 25 Sep 2010 13:51:12 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/kbse/2010},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{Bickel00,
	title={Mathematical statistics: basic ideas and selected topics},
	author={Bickel, P.J. and Doksum, K.A.},
	number={Bd. 1},
	isbn={9780138503635},
	lccn={00031377},
	series={Mathematical Statistics: Basic Ideas and Selected Topics},
	url={http://books.google.at/books?id=8poZAQAAIAAJ},
	year={2000},
	publisher={Prentice Hall}
}

@inproceedings{Legay10,
	author    = {Axel Legay and
	Beno\^{\i}t Delahaye and
	Saddek Bensalem},
	title     = {Statistical Model Checking: An Overview},
	booktitle = {RV},
	year      = {2010},
	pages     = {122-135},
	ee        = {http://dx.doi.org/10.1007/978-3-642-16612-9_11},
	crossref  = {DBLP:conf/rv/2010},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{Younes02,
	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},
	publisher = {Springer}
}

@inproceedings{YounesThesis,
	author = {Younes, H{\aa}kan L. S.},
	title = {Planning and verification for stochastic processes with asynchronous events},
	booktitle = {AAAI},
	year = {2004},
	isbn = {0-262-51183-5},
	location = {San Jose, California},
	pages = {1001--1002},
	numpages = {2},
	url = {http://dl.acm.org/citation.cfm?id=1597148.1597299},
	acmid = {1597299}
}

@book{Rudin76,
	title={Principles of Mathematical Analysis},
	author={Rudin, W.},
	isbn={9780070542358},
	lccn={75017903},
	series={International Series in Pure and Applied Mathematics},
	url={http://books.google.at/books?id=PzynSwAACAAJ},
	year={1976},
	publisher={McGraw-Hill}
}

@inproceedings{cav05,
	author    = {Koushik Sen and
	Mahesh Viswanathan and
	Gul Agha},
	title     = {On Statistical Model Checking of Stochastic Systems},
	booktitle = {CAV},
	pages     = {266--280},
	year      = {2005},
	url       = {http://dx.doi.org/10.1007/11513988_26},
	doi       = {10.1007/11513988_26},
	timestamp = {Thu, 28 Jul 2005 14:48:28 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/SenVA05},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cav/2005,
	editor    = {Kousha Etessami and
	Sriram K. Rajamani},
	title     = {Computer Aided Verification, 17th International Conference, {CAV}
	2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {3576},
	publisher = {Springer},
	year      = {2005},
	isbn      = {3-540-27231-3},
	timestamp = {Thu, 28 Jul 2005 14:48:28 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/2005},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@incollection{chatterjee2012robustness,
	title={Robustness of structurally equivalent concurrent parity games},
	author={Chatterjee, Krishnendu},
	booktitle={FoSSaCS},
	pages={270--285},
	year={2012},
	publisher={Springer}
}

@inproceedings{atva14,
	author    = {Tom{\'{a}}{\v s} Br{\'{a}}zdil and
	Krishnendu Chatterjee and
	Martin Chmel\'ik 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},
	booktitle = {{ATVA}},
	pages     = {98--114},
	year      = 2014,
	url       = {http://dx.doi.org/10.1007/978-3-319-11936-6_8},
	doi       = {10.1007/978-3-319-11936-6_8},
	timestamp = {Mon, 03 Nov 2014 14:32:36 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/BrazdilCCFKKPU14},
	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{vmcai04,
	author    = {Thomas H{\'{e}}rault and
	Richard Lassaigne and
	Fr{\'{e}}d{\'{e}}ric Magniette and
	Sylvain Peyronnet},
	title     = {Approximate Probabilistic Model Checking},
	booktitle = {{VMCAI}},
	pages     = {73--84},
	year      = {2004},
	url       = {http://dx.doi.org/10.1007/978-3-540-24622-0_8},
	doi       = {10.1007/978-3-540-24622-0_8},
	timestamp = {Wed, 06 Jul 2011 21:21:03 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/HeraultLMP04},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/vmcai/2004,
	editor    = {Bernhard Steffen and
	Giorgio Levi},
	title     = {Verification, Model Checking, and Abstract Interpretation, 5th International
	Conference, {VMCAI} 2004, Venice, January 11-13, 2004, Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {2937},
	publisher = {Springer},
	year      = {2004},
	isbn      = {3-540-20803-8},
	timestamp = {Thu, 08 Jan 2004 11:12:01 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/2004},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{Sen04,
	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}
}

@inproceedings{atva09,
	author    = {Diana El Rabih and
	Nihal Pekergin},
	title     = {Statistical Model Checking Using Perfect Simulation},
	booktitle = {{ATVA}},
	pages     = {120--134},
	year      = {2009},
	url       = {http://dx.doi.org/10.1007/978-3-642-04761-9_11},
	doi       = {10.1007/978-3-642-04761-9_11},
	timestamp = {Sat, 03 May 2014 07:56:09 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/RabihP09},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/atva/2009,
	editor    = {Zhiming Liu and
	Anders P. Ravn},
	title     = {Automated Technology for Verification and Analysis, 7th International
	Symposium, {ATVA} 2009, Macao, China, October 14-16, 2009. Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {5799},
	publisher = {Springer},
	year      = {2009},
	url       = {http://dx.doi.org/10.1007/978-3-642-04761-9},
	doi       = {10.1007/978-3-642-04761-9},
	isbn      = {978-3-642-04760-2},
	timestamp = {Sat, 03 May 2014 07:56:09 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/2009},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@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}
}

@proceedings{DBLP:conf/rv/2010,
	editor    = {Howard Barringer and
	Yli{\`e}s Falcone and
	Bernd Finkbeiner and
	Klaus Havelund and
	Insup Lee and
	Gordon J. Pace and
	Grigore Rosu and
	Oleg Sokolsky and
	Nikolai Tillmann},
	title     = {Runtime Verification - First International Conference, RV
	2010, St. Julians, Malta, November 1-4, 2010. Proceedings},
	booktitle = {RV},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {6418},
	year      = {2010},
	isbn      = {978-3-642-16611-2},
	ee        = {http://dx.doi.org/10.1007/978-3-642-16612-9},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{prism,
	author    = {Marta Z. Kwiatkowska and
	Gethin Norman and
	David Parker},
	title     = {PRISM 4.0: Verification of Probabilistic Real-Time Systems},
	booktitle = {CAV},
	year      = {2011},
	pages     = {585-591},
}

@article{CourcoubetisY95,
	author    = {Costas Courcoubetis and
	Mihalis Yannakakis},
	title     = {The Complexity of Probabilistic Verification},
	journal   = {J. {ACM}},
	volume    = {42},
	number    = {4},
	pages     = {857--907},
	year      = {1995},
	url       = {http://doi.acm.org/10.1145/210332.210339},
	doi       = {10.1145/210332.210339},
	timestamp = {Thu, 20 Nov 2003 12:28:06 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jacm/CourcoubetisY95},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{GrosuS05,
	author    = {Radu Grosu and
	Scott A. Smolka},
	title     = {Monte {C}arlo Model Checking},
	booktitle = {TACAS},
	pages     = {271--286},
	year      = {2005},
	url       = {http://dx.doi.org/10.1007/978-3-540-31980-1_18},
	doi       = {10.1007/978-3-540-31980-1_18},
	timestamp = {Mon, 08 Aug 2011 15:24:03 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tacas/GrosuS05},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{OudinetDGLP11,
	author    = {Johan Oudinet and
	Alain Denise and
	Marie{-}Claude Gaudel and
	Richard Lassaigne and
	Sylvain Peyronnet},
	title     = {Uniform {M}onte-{C}arlo Model Checking},
	booktitle = {FASE},
	pages     = {127--140},
	year      = 2011,
	url       = {http://dx.doi.org/10.1007/978-3-642-19811-3_10},
	doi       = {10.1007/978-3-642-19811-3_10},
	timestamp = {Tue, 22 Mar 2011 10:19:25 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/fase/OudinetDGLP11},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{hermanns1999multi,
	title={Multi terminal binary decision diagrams to represent and analyse continuous time {M}arkov chains},
	author={Hermanns, Holger and Meyer-Kayser, Joachim and Siegle, Markus},
	booktitle={3rd Int. Workshop on the Numerical Solution of Markov Chains},
	pages={188--207},
	year=1999,
	organization={Citeseer}
}

@misc{tool,
	title = {Tool for the paper},
	howpublished = {\url{http://pub.ist.ac.at/~przemek/pa_tool.html}}
}

@inproceedings{submitted,
	author    = {Przemyslaw Daca and
	Thomas A. Henzinger and
	Jan K{\v{r}}et{\'{\i}}nsk{\'{y}} and
	Tatjana Petrov},
	title     = {Linear Distances between {M}arkov Chains},
	booktitle = {{CONCUR}},
	year      = {2016},
}

@inproceedings{cav15,
	author    = {Tom{\'{a}}s Br{\'{a}}zdil and
	Krishnendu Chatterjee and
	Martin Chmelik and
	Andreas Fellner and
	Jan K{\v {r}}et{\'{\i}}nsk{\'{y}}},
	title     = {Counterexample Explanation by Learning Small Strategies in Markov
	Decision Processes},
	booktitle = {{CAV}},
	pages     = {158--177},
	year      = {2015},
}

@inproceedings{DBLP:conf/icalp/LehmannS83,
	author    = {Daniel J. Lehmann and
	Saharon Shelah},
	title     = {Reasoning with Time and Chance (Extended Abstract)},
	booktitle = {{ICALP}},
	pages     = {445--457},
	year      = {1983},
}

@article{DBLP:journals/fac/HanssonJ94,
	author    = {Hans Hansson and
	Bengt Jonsson},
	title     = {A Logic for Reasoning about Time and Reliability},
	journal   = {Formal Asp. Comput.},
	volume    = {6},
	number    = {5},
	pages     = {512--535},
	year      = {1994},
	url       = {http://dx.doi.org/10.1007/BF01211866},
	doi       = {10.1007/BF01211866},
	timestamp = {Wed, 25 May 2011 16:31:57 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/fac/HanssonJ94},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/focs/Vardi85,
	author    = {Moshe Y. Vardi},
	title     = {Automatic Verification of Probabilistic Concurrent Finite-State Programs},
	booktitle = {{FOCS}},
	pages     = {327--338},
	year      = {1985},
}

@inproceedings{DBLP:conf/qest/WimmerJVAKB13,
	author    = {Ralf Wimmer and
	Nils Jansen and
	Andreas Vorpahl and
	Erika {\'{A}}brah{\'{a}}m and
	Joost{-}Pieter Katoen and
	Bernd Becker},
	title     = {High-Level Counterexamples for Probabilistic Automata},
	booktitle = {
	{QEST}},
	pages     = {39--54},
	year      = {2013},
	url       = {http://dx.doi.org/10.1007/978-3-642-40196-1_4},
	doi       = {10.1007/978-3-642-40196-1_4},
	timestamp = {Wed, 24 Jul 2013 20:32:30 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/qest/WimmerJVAKB13},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@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},
	series    = {Lecture Notes in Computer Science},
	volume    = {8054},
	publisher = {Springer},
	year      = {2013},
	url       = {http://dx.doi.org/10.1007/978-3-642-40196-1},
	doi       = {10.1007/978-3-642-40196-1},
	isbn      = {978-3-642-40195-4},
	timestamp = {Wed, 24 Jul 2013 20:28:51 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/qest/2013},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@techreport{EJPV12,
	author = {C. Von Essen and B. Jobstmann and D. Parker and R. Varshneya},
	title = {Semi-Symbolic Computation of Efficient Controllers in Probabilistic Environments},
	institution = {Verimag},
	year = {2012}
}

@article{BKK14,
	author    = {	T. Br\'{a}zdil and
	S. Kiefer and
	A. Ku\v{c}era	},
	title     = {Efficient Analysis of Probabilistic Programs with an Unbounded Counter},
	journal   = {{Journal of the ACM}},
	volume    = {61},
	number    = {6},
	pages     = {41:1--41:35},
	year      = {2014},
}

@article{DBLP:journals/ita/BernetJW02,
	author    = {Julien Bernet and
	David Janin and
	Igor Walukiewicz},
	title     = {Permissive strategies: from parity games to safety games},
	journal   = {{ITA}},
	volume    = {36},
	number    = {3},
	pages     = {261--275},
	year      = {2002},
	url       = {http://dx.doi.org/10.1051/ita:2002013},
	doi       = {10.1051/ita:2002013},
	timestamp = {Tue, 17 Feb 2004 10:46:43 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/ita/BernetJW02},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/atva/BouyerMOU11,
	author    = {Patricia Bouyer and
	Nicolas Markey and
	J{\"{o}}rg Olschewski and
	Michael Ummels},
	title     = {Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games
	Revisited},
	booktitle = {Automated Technology for Verification and Analysis, 9th International
	Symposium, {ATVA} 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings},
	pages     = {135--149},
	year      = {2011},
	crossref  = {DBLP:conf/atva/2011},
	url       = {http://dx.doi.org/10.1007/978-3-642-24372-1_11},
	doi       = {10.1007/978-3-642-24372-1_11},
	timestamp = {Fri, 14 Oct 2011 20:11:29 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/atva/BouyerMOU11},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/tacas/DragerFKPU14,
	author    = {Klaus Dr{\"{a}}ger and
	Vojtech Forejt and
	Marta Z. Kwiatkowska and
	David Parker and
	Mateusz Ujma},
	title     = {Permissive Controller Synthesis for Probabilistic Systems},
	booktitle = {{TACAS}},
	pages     = {531--546},
	year      = {2014},
	url       = {http://dx.doi.org/10.1007/978-3-642-54862-8_44},
	doi       = {10.1007/978-3-642-54862-8_44},
	timestamp = {Sun, 23 Mar 2014 11:19:21 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/tacas/DragerFKPU14},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{CCD14,
	author    = {Krishnendu Chatterjee and
	Martin Chmelik and
	Przemyslaw Daca},
	title     = {{CEGAR} for Qualitative Analysis of Probabilistic Systems},
	booktitle = {CAV},
	pages     = {473--490},
	year      = {2014},
	url       = {http://dx.doi.org/10.1007/978-3-319-08867-9_31},
	doi       = {10.1007/978-3-319-08867-9_31},
	timestamp = {Mon, 30 Jun 2014 11:31:20 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/ChatterjeeCD14},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cav/2014,
	editor    = {Armin Biere and
	Roderick Bloem},
	title     = {Computer Aided Verification - 26th International Conference, {CAV}
	2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
	Austria, July 18-22, 2014. Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {8559},
	publisher = {Springer},
	year      = {2014},
	url       = {http://dx.doi.org/10.1007/978-3-319-08867-9},
	doi       = {10.1007/978-3-319-08867-9},
	isbn      = {978-3-319-08866-2},
	timestamp = {Mon, 30 Jun 2014 11:23:38 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cav/2014},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{KNP11,
	author={M. Kwiatkowska and G. Norman and D. Parker},
	title={{PRISM} 4.0: Verification of Probabilistic Real-time Systems},
	booktitle={Proc. 23rd International Conference on Computer Aided Verification (CAV'11)},
	year={2011},

	editor={G. Gopalakrishnan and S. Qadeer},
	pages={585--591},
	organization={},
	publisher={Springer},
	series={LNCS},
	volume={6806},
	address={},
	month={},
	note={},
	key={}
}

@book{Howard60,
	title = "Dynamic programming and Markov processes",
	author = "Howard, Ronald A.",
	publisher = "The MIT press, New York London",
	address = "Cambridge, MA",
	url = "http://opac.inria.fr/record=b1117485",
	year = 1960
}

@book{BK08,
	author = {C. Baier and J.-P. Katoen},
	title = {Principles of Model Checking (Representation and Mind Series)},
	year = {2008},
	isbn = {026202649X, 9780262026499},
	publisher = {The MIT Press},
}

@article{IC08,
	author    = {Tom{\'a}\v{s} Br{\'a}zdil and
	V{\'a}clav Bro\v{z}ek and
	Vojt\c{e}ch Forejt and
	Anton\'{\i}n Ku\v{c}era},
	title     = {Reachability in recursive Markov decision processes},
	journal   = {Inf. Comput.},
	volume    = {206},
	number    = {5},
	year      = {2008},
	pages     = {520-537},
	ee        = {http://dx.doi.org/10.1016/j.ic.2007.09.002},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{Boyd04,
	author = {Boyd, Stephen and Vandenberghe, Lieven},
	title = {Convex Optimization},
	year = {2004},
	isbn = {0521833787},
	publisher = {Cambridge Univ. Press},
	_address = {New York, NY, USA},
}

@inproceedings{lics2011,
	author    = {Tom{\'a}s Br{\'a}zdil and
	V{\'a}clav Bro\v{z}ek and
	Krishnendu Chatterjee and
	Vojt\v{e}ch Forejt and
	Anton\'{\i}n Ku\v{c}era},
	title     = {Two Views on Multiple Mean-Payoff Objectives in Markov Decision
	Processes},
	booktitle = {LICS},
	year      = {2011},
	pages     = {33-42},
	ee        = {http://dx.doi.org/10.1109/LICS.2011.10},
	crossref  = {DBLP:conf/lics/2011},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/lics/2011,
	title     = {Proceedings of the 26th Annual IEEE Symposium on Logic in
	Computer Science, LICS 2011, June 21-24, 2011, Toronto,
	Ontario, Canada},
	booktitle = {LICS},
	publisher = {IEEE Computer Society},
	year      = {2011},
	isbn      = {978-0-7695-4412-0}
}

@comment{This file has been generated by Pybliographer}
@techreport{techreport,
	author    = {Tom{\'a}\v{s} Br{\'a}zdil and
	V{\'a}clav Bro\v{z}ek and
	Krishnendu Chatterjee and
	Vojt\v{e}ch Forejt and
	Anton\'in Ku\v{c}era},
	title     = {Two Views on Multiple Mean-Payoff Objectives in {Markov} Decision Processes},
	year      = 2011,
	institution = {FI MU, Brno, Czech Rep.},
	number    = {FIMU-RS-2011-02}
}
@inproceedings{BBE10,
	author    = {Tom{\'a}\v{s} Br{\'a}zdil and
	V{\'a}clav Bro\v{z}ek and
	Kousha Etessami},
	title     = {One-Counter Stochastic Games},
	booktitle = {FSTTCS},
	year      = {2010},
	pages     = {108-119},
	ee        = {http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.108},
	crossref  = {DBLP:conf/fsttcs/2010},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/fsttcs/2010,
	editor    = {Kamal Lodaya and
	Meena Mahajan},
	title     = {IARCS Annual Conference on Foundations of Software Technology
	and Theoretical Computer Science, FSTTCS 2010, December
	15-18, 2010, Chennai, India},
	booktitle = {FSTTCS},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum f\"ur Informatik},
	series    = {LIPIcs},
	volume    = {8},
	year      = {2010},
	isbn      = {978-3-939897-23-1},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{GH10,
	author    = {Hugo Gimbert and
	Florian Horn},
	title     = {Solving Simple Stochastic Tail Games},
	booktitle = {SODA},
	year      = {2010},
	pages     = {847-862},
	ee        = {http://www.siam.org/proceedings/soda/2010/SODA10_069_gimberth.pdf},
	crossref  = {DBLP:conf/soda/2010},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/soda/2010,
	editor    = {Moses Charikar},
	title     = {Proceedings of the Twenty-First Annual ACM-SIAM Symposium
	on Discrete Algorithms, SODA 2010, Austin, Texas, USA, January
	17-19, 2010},
	booktitle = {SODA},
	publisher = {SIAM},
	year      = {2010},
	ee        = {http://dl.acm.org/citation.cfm?id=1873601},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Cha07b,
	author = {Chatterjee, Krishnendu},
	title = {Concurrent games with tail objectives},
	journal = {Theor. Comput. Sci.},
	volume = {388},
	issue = {1-3},
	month = {December},
	year = {2007},
	issn = {0304-3975},
	pages = {181--198},
	numpages = {18},
	url = {http://portal.acm.org/citation.cfm?id=1316093.1316369},
	doi = {10.1016/j.tcs.2007.07.047},
	acmid = {1316369},
	publisher = {Elsevier Science Publishers Ltd.},
	address = {Essex, UK},
	keywords = {Concurrent games, Muller objectives, Omega-regular objectives, Tail objectives},
}

@InProceedings{FKN+11,
	author    = {Vojtech Forejt and
	Marta Z. Kwiatkowska and
	Gethin Norman and
	David Parker and
	Hongyang Qu},
	title     = {Quantitative Multi-objective Verification for Probabilistic
	Systems},
	booktitle = {TACAS},
	year      = {2011},
	pages     = {112-127},
	ee        = {http://dx.doi.org/10.1007/978-3-642-19835-9_11},
	crossref  = {DBLP:conf/tacas/2011},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tacas/2011,
	editor    = {Parosh Aziz Abdulla and
	K. Rustan M. Leino},
	title     = {Tools and Algorithms for the Construction and Analysis of
	Systems - 17th International Conference, TACAS 2011, Held
	as Part of the Joint European Conferences on Theory and
	Practice of Software, ETAPS 2011, Saarbr{\"u}cken, Germany,
	March 26-April 3, 2011. Proceedings},
	booktitle = {TACAS},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {6605},
	year      = {2011},
	isbn      = {978-3-642-19834-2},
	ee        = {http://dx.doi.org/10.1007/978-3-642-19835-9},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{BBPM99,
	Author         = {L. Benini and A. Bogliolo and G. Paleologo and G. De
	Micheli},
	Title          = {Policy optimization for dynamic power management},
	Journal        = {IEEE Transactions on Computer-Aided Design of
	Integrated Circuits and Systems},
	Volume         = {8},
	Number         = {3},
	Pages          = {299-316},
	Note           = {},
	key            = {},
	month          = {},
	publisher      = {},
	year           = 2000
}

@InProceedings{CMH06,
	author    = {Krishnendu Chatterjee and
	Rupak Majumdar and
	Thomas A. Henzinger},
	title     = {Markov Decision Processes with Multiple Objectives},
	booktitle = {STACS},
	year      = {2006},
	pages     = {325-336},
	ee        = {http://dx.doi.org/10.1007/11672142_26},
	crossref  = {DBLP:conf/stacs/2006},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/stacs/2006,
	editor    = {Bruno Durand and
	Wolfgang Thomas},
	title     = {STACS 2006, 23rd Annual Symposium on Theoretical Aspects
	of Computer Science, Marseille, France, February 23-25,
	2006, Proceedings},
	booktitle = {STACS},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {3884},
	year      = {2006},
	isbn      = {3-540-32301-5},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{AH90,
	Author         = {J. Aspnes and M. Herlihy},
	Title          = {Fast Randomized Consensus Using Shared Memory},
	Journal        = {Journal of Algorithms},
	Volume         = {15},
	Number         = {1},
	Pages          = {441--460},
	Note           = {},
	key            = {},
	month          = {},
	year           = 1990
}

@InProceedings{BFK08,
	Author         = {T. Br\'{a}zdil and V. Forejt and A. Ku\v{c}era},
	Title          = {Controller Synthesis and Verification for {Markov}
	Decision Processes with Qualitative Branching Time
	Objectives},
	BookTitle      = {Proc. ICALP'08},
	Editor         = {},
	Volume         = {},
	Series         = {},
	Pages          = {148--159},
	Address        = {},
	Organization   = {},
	Publisher      = {},
	Note           = {},
	key            = {},
	month          = {},
	year           = 2008
}

@Book{Royden88,
	Author         = {Royden, H.},
	Title          = {Real analysis},
	Publisher      = {Prentice Hall},
	Edition        = {3rd},
	month          = {12 } # feb,
	year           = 1988
}

@InProceedings{BBL+10,
	Author         = {B. Caillaud and B. Delahaye and K. Larsen and A. Legay
	and M. Pedersen and A. Wasowski},
	Title          = {Compositional design methodology with constraint
	{Markov} chains},
	BookTitle      = {QEST'10},
	Editor         = {},
	Volume         = {},
	Series         = {},
	Pages          = {},
	Address        = {},
	Organization   = {},
	Publisher      = {},
	Note           = {},
	key            = {},
	month          = {},
	year           = 2010
}

@Article{NPK+05,
	Author         = {G. Norman and D. Parker and M. Kwiatkowska and S.
	Shukla and R. Gupta},
	Title          = {Using Probabilistic Model Checking for Dynamic Power
	Management},
	Journal        = {Formal Aspects of Computing},
	Volume         = {17},
	Number         = {2},
	Pages          = {160-176},
	Note           = {},
	key            = {},
	month          = {},
	publisher      = {Springer},
	year           = 2005
}

@InProceedings{CdAF+06,
	Author         = {K. Chatterjee and L. de Alfaro and M. Faella and T.
	Henzinger and R. Majumdar and M. Stoelinga},
	Title          = {Compositional Quantitative Reasoning},
	BookTitle      = {Proc. QEST'06},
	Volume         = {},
	Series         = {},
	Address        = {},
	Organization   = {},
	Note           = {},
	_editor        = {},
	_pages         = {179--188},
	_publisher     = {IEEE CS Press},
	key            = {},
	month          = {},
	year           = 2006
}

@InProceedings{BdA95,
	Author         = {A. Bianco and L. de Alfaro},
	Title          = {Model Checking of Probabilistic and Nondeterministic
	Systems},
	BookTitle      = {Proc. FSTTCS'95},
	Pages          = {499--513},
	Address        = {},
	Organization   = {},
	Publisher      = {Springer},
	Note           = {},
	_editor        = {P. Thiagarajan},
	_series        = {LNCS},
	_volume        = {1026},
	key            = {},
	month          = {},
	year           = 1995
}

@PhdThesis{dA97a,
	Author         = {L. de Alfaro},
	Title          = {Formal Verification of Probabilistic Systems},
	School         = {Stanford University},
	Type           = {},
	Address        = {},
	Note           = {},
	key            = {},
	month          = {},
	year           = 1997
}

@InProceedings{BGL04,
	Author         = {C. Baier and M. Gr{\"o}{\ss}er and M. Leucker and B.
	Bollig and F. Ciesinski},
	Title          = {Controller Synthesis for Probabilistic Systems},
	BookTitle      = {Proc. IFIP TCS'04},
	Editor         = {},
	Volume         = {},
	Series         = {},
	Pages          = {493--5062},
	Address        = {},
	Organization   = {},
	Publisher      = {},
	Note           = {},
	key            = {},
	month          = {},
	year           = 2004
}

@Book{Cli97,
	Author         = {},
	Editor         = {J. Cl\'{i}ımaco},
	Title          = {Multicriteria Analysis},
	Publisher      = {Springer-Verlag},
	Volume         = {},
	Series         = {},
	Address        = {},
	Edition        = {},
	Note           = {},
	key            = {},
	month          = {},
	year           = 1997
}

@Article{BK98,
	Author         = {C. Baier and M. Kwiatkowska},
	Title          = {Model Checking for a Probabilistic Branching Time
	Logic with Fairness},
	Journal        = {Distributed Computing},
	Volume         = {11},
	Number         = {3},
	Pages          = {125--155},
	Note           = {},
	key            = {},
	month          = {},
	year           = 1998
}

@InProceedings{Cha07,
	author    = {Krishnendu Chatterjee},
	title     = {Markov Decision Processes with Multiple Long-Run Average
	Objectives},
	booktitle = {FSTTCS},
	year      = {2007},
	pages     = {473-484},
	ee        = {http://dx.doi.org/10.1007/978-3-540-77050-3_39},
	crossref  = {DBLP:conf/fsttcs/2007},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/fsttcs/2007,
	editor    = {Vikraman Arvind and
	Sanjiva Prasad},
	title     = {FSTTCS 2007: Foundations of Software Technology and Theoretical
	Computer Science, 27th International Conference, New Delhi,
	India, December 12-14, 2007, Proceedings},
	booktitle = {FSTTCS},
	publisher = {Springer},
	series    = {Lecture Notes in Computer Science},
	volume    = {4855},
	year      = {2007},
	isbn      = {978-3-540-77049-7},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@ARTICLE{CY98,
	author={Courcoubetis, C. and Yannakakis, M.},
	journal={Automatic Control, IEEE Transactions on},
	title={Markov decision processes and regular events},
	year={1998},
	month=oct,
	volume={43},
	number={10},
	pages={1399--1418},
	keywords={ omega;-regular sets;finite-state Markov decision processes;optimal policies;regular events;Markov processes;computational complexity;decision theory;discrete event systems;finite automata;formal languages;},
	doi={10.1109/9.720497},
	ISSN={0018-9286},
}

@Unpublished{CAG02,
	Author         = {S. Cheshire and B. Adoba and E. Gutterman},
	Title          = {Dynamic configuration of {IPv}4 link local addresses},
	Note           = {Available from http://www.ietf.org/rfc/rfc3927.txt},
	key            = {},
	month          = {},
	year           = {}
}

@InProceedings{DCL10,
	Author         = {B. Delahaye and B. Caillaud and A. Legay},
	Title          = {Probabilistic Contracts: A Compositional Reasoning
	Methodology for the Design of Stochastic Systems},
	BookTitle      = {ACSD'10},
	Editor         = {},
	Volume         = {},
	Series         = {},
	Pages          = {},
	Address        = {},
	Organization   = {},
	Publisher      = {},
	Note           = {},
	key            = {},
	month          = {},
	year           = 2010
}

@InProceedings{CHJS10,
	Author         = {K. Chatterjee and T. Henzinger and B. Jobstmann and R.
	Singh},
	Title          = {Measuring and Synthesizing Systems in Probabilistic
	Environments},
	BookTitle      = {Proc. CAV'10},
	Editor         = {},
	Volume         = {},
	Organization   = {},
	Note           = {},
	_pages         = {380--395},
	_publisher     = {Springer},
	_series        = {LNCS},
	key            = {},
	month          = {},
	year           = 2010
}

@InProceedings{BGC09,
	Author         = {C. Baier and M. Gr{\"o}{\ss}er and F. Ciesinski},
	Title          = {Quantitative Analysis under Fairness Constraints},
	BookTitle      = {Proc. ATVA'09},
	Editor         = {},
	Volume         = {5799},
	Series         = {LNCS},
	Pages          = {135-150},
	Address        = {},
	Organization   = {},
	Publisher      = {Springer},
	Note           = {},
	key            = {},
	month          = {},
	year           = 2009
}

@InProceedings{Var85,
	Author         = {M. Vardi},
	Title          = {Automatic Verification of Probabilistic Concurrent
	Finite State Programs},
	BookTitle      = {Proc. FOCS'85},
	Editor         = {},
	Pages          = {327--338},
	Address        = {},
	Organization   = {},
	Publisher      = {IEEE Computer Society Press},
	Note           = {},
	key            = {},
	month          = {},
	year           = 1985
}

@Article{KS08,
	Author         = {A. Ku\v{c}era and O. Stra\v{z}ovsk{\'y}},
	Title          = {On the Controller Synthesis for Finite-State {Markov}
	Decision Processes},
	Journal        = {Fundamenta Informaticae},
	Volume         = {82},
	Number         = {1-2},
	Pages          = {141--153},
	Note           = {},
	key            = {},
	month          = {},
	publisher      = {},
	year           = 2008
}

@PhdThesis{Seg95,
	Author         = {R. Segala},
	Title          = {Modelling and Verification of Randomized Distributed
	Real Time Systems},
	School         = {Massachusetts Institute of Technology},
	Type           = {},
	Address        = {},
	Note           = {},
	key            = {},
	month          = {},
	year           = 1995
}

@InProceedings{KNPQ10,
	Author         = {M. Kwiatkowska and G. Norman and D. Parker and H. Qu},
	Title          = {Assume-Guarantee Verification for Probabilistic
	Systems},
	BookTitle      = {Proc. TACAS'10},
	Pages          = {23--37},
	Address        = {},
	Organization   = {},
	Publisher      = {Springer},
	Note           = {},
	_editor        = {J. Esparza and R. Majumdar},
	_series        = {LNCS},
	_volume        = {6105},
	key            = {},
	month          = {},
	year           = 2010
}

@Article{SL95,
	Author         = {R. Segala and N. Lynch},
	Title          = {Probabilistic Simulations for Probabilistic Processes},
	Journal        = {Nordic Journal of Computing},
	Volume         = {2},
	Number         = {2},
	Pages          = {250-273},
	Note           = {},
	key            = {},
	month          = {},
	publisher      = {},
	year           = 1995
}

@Book{Norris98,
	Author         = {Norris, J. R.},
	Title          = {Markov chains},
	Publisher      = {Cambridge University Press},
	year           = 1998
}

@Article{EKVY08,
	Author         = {K. Etessami and M. Kwiatkowska and M. Vardi and M.
	Yannakakis},
	Title          = {Multi-Objective Model Checking of {Markov} Decision
	Processes},
	Journal        = {LMCS},
	Volume         = {4},
	Number         = {4},
	Pages          = {1-21},
	Note           = {},
	_journal       = {Logical Methods in Computer Science},
	key            = {},
	month          = {},
	publisher      = {},
	year           = 2008
}

@InProceedings{PBU09,
	Author         = {E. Pavese and V. Braberman and S. Uchitel},
	Title          = {Probabilistic environments in the quantitative
	analysis of (non-probabilistic) behaviour models},
	BookTitle      = {Proc. ESEC/FSE'09},
	Volume         = {},
	Series         = {},
	Address        = {},
	Organization   = {},
	Publisher      = {},
	Note           = {},
	_editor        = {},
	_pages         = {},
	key            = {},
	month          = {},
	year           = 2009
}

@InProceedings{FKP10,
	Author         = {L. Feng and M. Kwiatkowska and D. Parker},
	Title          = {Compositional Verification of Probabilistic Systems
	using Learning},
	BookTitle      = {Proc. QEST'10},
	Editor         = {},
	Volume         = {},
	Series         = {},
	Pages          = {133--142},
	Address        = {},
	Organization   = {},
	Publisher      = {IEEE},
	Note           = {},
	key            = {},
	month          = {},
	year           = 2010
}

@Book{Ehr05,
	Author         = {M. Ehrgott},
	Editor         = {},
	Title          = {Multicriteria optimization},
	Publisher      = {Springer-Verlag},
	Volume         = {},
	Series         = {},
	Address        = {},
	Edition        = {},
	Note           = {},
	key            = {},
	month          = {},
	year           = 2005
}

}

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

@inproceedings{Szymanek,
	author    = {Radoslaw Szymanek and
	Francky Catthoor and
	Krzysztof Kuchcinski},
	title     = {Time-Energy Design Space Exploration for Multi-Layer Memory
	Architectures},
	booktitle = {DATE},
	year      = {2004},
	pages     = {318-323},
	ee        = {http://doi.ieeecomputersociety.org/10.1109/DATE.2004.1268867},
	crossref  = {DBLP:conf/date/2004},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/date/2004,
	title     = {2004 Design, Automation and Test in Europe Conference and
	Exposition (DATE 2004), 16-20 February 2004, Paris, France},
	booktitle = {DATE},
	publisher = {IEEE Computer Society},
	year      = {2004},
	isbn      = {0-7695-2085-5},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{YC,
	author    = {Peng Yang and
	Francky Catthoor},
	title     = {Pareto-optimization-based run-time task scheduling for embedded
	systems},
	booktitle = {CODES+ISSS},
	year      = {2003},
	pages     = {120-125},
	ee        = {http://doi.acm.org/10.1145/944645.944680},
	crossref  = {DBLP:conf/codes/2003},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/codes/2003,
	editor    = {Rajesh Gupta and
	Yukihiro Nakamura and
	Alex Orailoglu and
	Pai H. Chou},
	title     = {Proceedings of the 1st IEEE/ACM/IFIP International Conference
	on Hardware/Software Codesign and System Synthesis, CODES+ISSS
	2003, Newport Beach, CA, USA, October 1-3, 2003},
	booktitle = {CODES+ISSS},
	publisher = {ACM},
	year      = {2003},
	isbn      = {1-58113-742-7},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@incollection{Koski,
	author = "J. Koski",
	title = "Multicriteria truss optimization",
	booktitle = "Multicriteria Optimization in Engineering and in the Sciences",
	editor = "W. Stadler",
	publisher = "Plenum Press",
	year = 1988
}

@book{Owen95,
	author = "G. Owen",
	title = "Game Theory",
	publisher = "Academic Press",
	year= 1995
}

@inproceedings{PY00,
	author    = {Christos H. Papadimitriou and
	Mihalis Yannakakis},
	title     = {On the Approximability of Trade-offs and Optimal Access
	of Web Sources},
	booktitle = {FOCS},
	year      = {2000},
	pages     = {86-92},
	ee        = {http://doi.ieeecomputersociety.org/10.1109/SFCS.2000.892068},
	crossref  = {DBLP:conf/focs/2000},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/focs/2000,
	title     = {41st Annual Symposium on Foundations of Computer Science,
	FOCS 2000, 12-14 November 2000, Redondo Beach, California,
	USA},
	booktitle = {FOCS},
	publisher = {IEEE Computer Society},
	year      = {2000},
	isbn      = {0-7695-0850-2},
	bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{Altman,
	author = {Altman, Eitan},
	publisher = {Chapman \& Hall/CRC},
	title = {Constrained Markov Decision Processes (Stochastic Modeling)},
	year = {1999}
}

@article{DBLP:journals/corr/DacaHKP15,
	author    = {Przemyslaw Daca and
	Thomas A. Henzinger and
	Jan K{\v r}et{\'{\i}}nsk{\'{y}} and
	Tatjana Petrov},
	title     = {Faster Statistical Model Checking for Unbounded Temporal Properties},
	journal   = {TACAS},
	year      = {2016},
	pages     = {112--129}
}

@inproceedings{KieferMOWW11,
	author    = {Stefan Kiefer and
	Andrzej S. Murawski and
	Jo{\"{e}}l Ouaknine and
	Bj{\"{o}}rn Wachter and
	James Worrell},
	title     = {Language Equivalence for Probabilistic Automata},
	booktitle = {CAV},
	pages     = {526--540},
	year      = {2011},
}

@book{Paz_1971,
	author = {Paz, Azaria},
	title = {Introduction to Probabilistic Automata (Computer Science and Applied Mathematics)},
	year = {1971},
	isbn = {0125476507},
	publisher = {Academic Press, Inc.},
	address = {Orlando, FL, USA},
}

@article{goodman1964,
	title={Simultaneous confidence intervals for contrasts among multinomial populations},
	author={Goodman, Leo A},
	journal={The Annals of Mathematical Statistics},
	pages={716--725},
	year={1964},
	publisher={JSTOR}
}

@inproceedings{DBLP:conf/csl/ChenK14,
	author    = {Taolue Chen and
	Stefan Kiefer},
	title     = {On the total variation distance of labelled {M}arkov chains},
	booktitle = {{CSL-LICS}},
	pages     = {33:1--33:10},
	year      = {2014}
}
@proceedings{DBLP:conf/csl/2014,
	editor    = {Thomas A. Henzinger and
	Dale Miller},
	title     = {{CSL-LICS} '14, Vienna, Austria,
	July 14 - 18, 2014},
	publisher = {{ACM}},
	year      = {2014}
}

@inproceedings{DBLP:conf/tacas/BacciBLM13,
	author    = {Giorgio Bacci and
	Giovanni Bacci and
	Kim G. Larsen and
	Radu Mardare},
	title     = {On-the-Fly Exact Computation of Bisimilarity Distances},
	booktitle = {{TACAS}},
	pages     = {1--15},
	year      = {2013}
}
@proceedings{DBLP:conf/tacas/2013,
	editor    = {Nir Piterman and
	Scott A. Smolka},
	title     = {{TACAS}},
	series    = {Lecture Notes in Computer Science},
	volume    = {7795},
	publisher = {Springer},
	year      = {2013}
}

@inproceedings{DBLP:conf/mfcs/BacciBLM13,
	author    = {Giorgio Bacci and
	Giovanni Bacci and
	Kim G. Larsen and
	Radu Mardare},
	title     = {Computing Behavioral Distances, Compositionally},
	booktitle = {{MFCS}},
	pages     = {74--85},
	year      = {2013}
}
@proceedings{DBLP:conf/mfcs/2013,
	editor    = {Krishnendu Chatterjee and
	Jir{\'{\i}} Sgall},
	title     = {{MFCS} 2013},
	series    = {Lecture Notes in Computer Science},
	volume    = {8087},
	publisher = {Springer},
	year      = {2013}
}

@inproceedings{DBLP:conf/qest/BacciBLM13,
	author    = {Giorgio Bacci and
	Giovanni Bacci and
	Kim G. Larsen and
	Radu Mardare},
	title     = {The {BisimDist} Library: Efficient Computation of Bisimilarity Distances
	for {M}arkovian Models},
	booktitle = {{QEST}},
	pages     = {278--281},
	year      = {2013}
}
@proceedings{DBLP:conf/qest/2013,
	editor    = {Kaustubh R. Joshi and
	Markus Siegle and
	Mari{\"{e}}lle Stoelinga and
	Pedro R. D'Argenio},
	title     = {{QEST}},
	series    = {Lecture Notes in Computer Science},
	volume    = {8054},
	publisher = {Springer},
	year      = {2013}
}

@inproceedings{DBLP:conf/fossacs/BacciBLM15,
	author    = {Giorgio Bacci and
	Giovanni Bacci and
	Kim G. Larsen and
	Radu Mardare},
	title     = {On the Total Variation Distance of Semi-{M}arkov Chains},
	booktitle = {FoSSaCS},
	pages     = {185--199},
	year      = {2015}
}
@proceedings{DBLP:conf/fossacs/2015,
	editor    = {Andrew M. Pitts},
	title     = {FoSSaCS 2015},
	series    = {Lecture Notes in Computer Science},
	volume    = {9034},
	publisher = {Springer},
	year      = {2015}
}

@inproceedings{DBLP:conf/ictac/BacciBLM15,
	author    = {Giorgio Bacci and
	Giovanni Bacci and
	Kim G. Larsen and
	Radu Mardare},
	title     = {Converging from Branching to Linear Metrics on {M}arkov Chains},
	booktitle = {{ICTAC}},
	pages     = {349--367},
	year      = {2015}
}

@proceedings{DBLP:conf/ictac/2015,
	editor    = {Martin Leucker and
	Camilo Rueda and
	Frank D. Valencia},
	title     = {{ICTAC} 2015},
	series    = {Lecture Notes in Computer Science},
	volume    = {9399},
	publisher = {Springer},
	year      = {2015}
}

@inproceedings{2015arXiv151009102F,
	author    = {Nathana{\"{e}}l Fijalkow and
	Stefan Kiefer and
	Mahsa Shirmohammadi},
	title     = {Trace Refinement in Labelled {M}arkov Decision Processes},
	booktitle = {{FOSSACS}},
	pages     = {303--318},
	year      = {2016},
	timestamp = {Tue, 22 Mar 2016 15:58:43 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/fossacs/FijalkowKS16},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}	crossref  = {DBLP:conf/fossacs/2016},
url       = {http://dx.doi.org/10.1007/978-3-662-49630-5_18},
doi       = {10.1007/978-3-662-49630-5_18},
@proceedings{DBLP:conf/fossacs/2016,
	editor    = {Bart Jacobs and
	Christof L{\"{o}}ding},
	title     = {Foundations of Software Science and Computation Structures - 19th
	International Conference, {FOSSACS} 2016, Held as Part of the European
	Joint Conferences on Theory and Practice of Software, {ETAPS} 2016,
	Eindhoven, The Netherlands, April 2-8, 2016, Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {9634},
	publisher = {Springer},
	year      = {2016},
	url       = {http://dx.doi.org/10.1007/978-3-662-49630-5},
	doi       = {10.1007/978-3-662-49630-5},
	isbn      = {978-3-662-49629-9},
	timestamp = {Tue, 22 Mar 2016 15:58:08 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/fossacs/2016},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/ijfcs/DoyenHR08,
	author    = {Laurent Doyen and
	Thomas A. Henzinger and
	Jean{-}Fran{\c{c}}ois Raskin},
	title     = {Equivalence of Labeled {M}arkov Chains},
	journal   = {Int. J. Found. Comput. Sci.},
	volume    = {19},
	number    = {3},
	pages     = {549--563},
	year      = {2008}
}

@inproceedings{DBLP:conf/concur/DesharnaisGJP99,
	author    = {Josee Desharnais and
	Vineet Gupta and
	Radha Jagadeesan and
	Prakash Panangaden},
	title     = {Metrics for Labeled {M}arkov Systems},
	booktitle = {{CONCUR}},
	pages     = {258--273},
	year      = {1999}
}
@proceedings{DBLP:conf/concur/1999,
	editor    = {Jos C. M. Baeten and
	Sjouke Mauw},
	title     = {{CONCUR} '99},
	series    = {Lecture Notes in Computer Science},
	volume    = {1664},
	publisher = {Springer},
	year      = {1999}
}

@inproceedings{DBLP:conf/cav/DeshmukhMP15,
	author    = {Jyotirmoy V. Deshmukh and
	Rupak Majumdar and
	Vinayak S. Prabhu},
	title     = {Quantifying Conformance Using the {S}korokhod Metric},
	booktitle = {CAV},
	pages     = {234--250},
	year      = {2015}
}
@proceedings{DBLP:conf/cav/2015,
	editor    = {Daniel Kroening and
	Corina S. Pasareanu},
	title     = {CAV, 2015},
	series    = {Lecture Notes in Computer Science},
	volume    = {9207},
	publisher = {Springer},
	year      = {2015}
}

@inproceedings{DBLP:conf/hybrid/MajumdarP15,
	author    = {Rupak Majumdar and
	Vinayak S. Prabhu},
	title     = {Computing the {S}korokhod distance between polygonal traces},
	booktitle = {HSCC},
	pages     = {199--208},
	year      = {2015}
}

@proceedings{DBLP:conf/hybrid/2015,
	editor    = {Antoine Girard and
	Sriram Sankaranarayanan},
	title     = {HSCC'15},
	publisher = {{ACM}},
	year      = {2015}
}

============================================

@inproceedings{DBLP:conf/concur/DesharnaisGJP99,
	author    = {Josee Desharnais and
	Vineet Gupta and
	Radha Jagadeesan and
	Prakash Panangaden},
	title     = {Metrics for Labeled {M}arkov Systems},
	booktitle = {{CONCUR}},
	pages     = {258--273},
	year      = {1999}
}

@proceedings{DBLP:conf/concur/1999,
	editor    = {Jos C. M. Baeten and
	Sjouke Mauw},
	title     = {{CONCUR} '99},
	series    = {Lecture Notes in Computer Science},
	volume    = {1664},
	publisher = {Springer},
	year      = {1999}
}

@article{DBLP:journals/tcs/DesharnaisGJP04,
	author    = {Josee Desharnais and
	Vineet Gupta and
	Radha Jagadeesan and
	Prakash Panangaden},
	title     = {Metrics for labelled {M}arkov processes},
	journal   = {Theor. Comput. Sci.},
	volume    = {318},
	number    = {3},
	pages     = {323--354},
	year      = {2004}
}

@inproceedings{DBLP:conf/lics/AlfaroMRS07,
	author    = {Luca de Alfaro and
	Rupak Majumdar and
	Vishwanath Raman and
	Mari{\"{e}}lle Stoelinga},
	title     = {Game Relations and Metrics},
	booktitle = {LICS},
	pages     = {99--108},
	year      = {2007}
}
@proceedings{DBLP:conf/lics/2007,
	title     = {LICS 2007},
	publisher = {{IEEE} Computer Society},
	year      = {2007}
}

@inproceedings{DBLP:conf/icalp/AlfaroFS04,
	author    = {Luca de Alfaro and
	Marco Faella and
	Mari{\"{e}}lle Stoelinga},
	title     = {Linear and Branching Metrics for Quantitative Transition Systems},
	booktitle = {{ICALP}},
	pages     = {97--109},
	year      = {2004}
}

@proceedings{DBLP:conf/icalp/2004,
	editor    = {Josep D{\'{\i}}az and
	Juhani Karhum{\"{a}}ki and
	Arto Lepist{\"{o}} and
	Donald Sannella},
	title     = {{ICALP} 2004},
	series    = {Lecture Notes in Computer Science},
	volume    = {3142},
	publisher = {Springer},
	year      = {2004}
}

@article{DBLP:journals/tcs/BreugelW06,
	author    = {Franck van Breugel and
	James Worrell},
	title     = {Approximating and computing behavioural distances in probabilistic
	transition systems},
	journal   = {Theor. Comput. Sci.},
	volume    = {360},
	number    = {1-3},
	pages     = {373--385},
	year      = {2006}
}

@inproceedings{DBLP:conf/popl/LarsenS89,
	author    = {Kim G. Larsen and Arne Skou},
	title     = {Bisimulation Through Probabilistic Testing},
	booktitle = {POPL},
	pages     = {344--352},
	year      = {1989}
}
@proceedings{DBLP:conf/popl/1989,
	title     = {Conference Record of the Sixteenth Annual {ACM} Symposium on Principles
	of Programming Languages, 1989},
	publisher = {{ACM} Press},
	year      = {1989}
}

@inproceedings{DBLP:conf/fossacs/BreugelSW07,
	author    = {F. van Breugel and
	B. Sharma and
	J. Worrell},
	title     = {Approximating a Behavioural Pseudometric Without Discount for Probabilistic
	Systems},
	booktitle = {{FOSSACS}},
	pages     = {123--137},
	year      = {2007}
}
@proceedings{DBLP:conf/fossacs/2007,
	editor    = {Helmut Seidl},
	title     = {{FOSSACS}},
	series    = {Lecture Notes in Computer Science},
	volume    = {4423},
	publisher = {Springer},
	year      = {2007}
}

@inproceedings{DBLP:conf/qest/JaegerMLM14,
	author    = {Manfred Jaeger and
	Hua Mao and
	Kim G. Larsen and
	Radu Mardare},
	title     = {Continuity Properties of Distances for {M}arkov Processes},
	booktitle = {{QEST}},
	pages     = {297--312},
	year      = {2014}
}
@proceedings{DBLP:conf/qest/2014,
	editor    = {Gethin Norman and
	William H. Sanders},
	title     = {{QEST}},
	series    = {Lecture Notes in Computer Science},
	volume    = {8657},
	publisher = {Springer},
	year      = {2014}
}

@inproceedings{DBLP:conf/aaai/FernsPP04,
	author    = {Norm Ferns and
	Prakash Panangaden and
	Doina Precup},
	title     = {Metrics for Finite {M}arkov Decision Processes},
	booktitle = {IAAI},
	pages     = {950--951},
	year      = {2004}
}
@proceedings{DBLP:conf/aaai/2004,
	editor    = {Deborah L. McGuinness and
	George Ferguson},
	title     = {Sixteenth Conference on Innovative Applications of Artificial Intelligence,
	2004},
	publisher = {{AAAI} Press / The {MIT} Press},
	year      = {2004}
}

@inproceedings{DBLP:conf/hybrid/TkachevA14,
	author    = {Ilya Tkachev and
	Alessandro Abate},
	title     = {On approximation metrics for linear temporal model-checking of stochastic
	systems},
	booktitle = {HSCC},
	pages     = {193--202},
	year      = {2014},
	timestamp = {Tue, 22 Apr 2014 20:59:57 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/hybrid/TkachevA14},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}	crossref  = {DBLP:conf/hybrid/2014},
@proceedings{DBLP:conf/hybrid/2014,
	editor    = {Martin Fr{\"{a}}nzle and
	John Lygeros},
	title     = {17th International Conference on Hybrid Systems: Computation and Control
	(part of {CPS} Week), HSCC'14, Berlin, Germany, April 15-17, 2014},
	publisher = {{ACM}},
	year      = {2014},
	url       = {http://dl.acm.org/citation.cfm?id=2562059},
	isbn      = {978-1-4503-2732-9},
	timestamp = {Tue, 22 Apr 2014 20:53:28 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/hybrid/2014},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/entcs/Abate13,
	author    = {Alessandro Abate},
	title     = {Approximation Metrics Based on Probabilistic Bisimulations for General
	State-Space {M}arkov Processes: {A} Survey},
	journal   = {Electr. Notes Theor. Comput. Sci.},
	volume    = {297},
	pages     = {3--25},
	year      = {2013},
	timestamp = {Fri, 03 Jan 2014 15:08:07 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/entcs/Abate13},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{DBLP:journals/ejcon/GirardP11,
	author    = {Antoine Girard and
	George J. Pappas},
	title     = {Approximate Bisimulation: {A} Bridge Between Computer Science and
	Control Theory},
	journal   = {Eur. J. Control},
	volume    = {17},
	number    = {5-6},
	pages     = {568--578},
	year      = {2011},
	timestamp = {Tue, 06 Nov 2012 14:08:48 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/ejcon/GirardP11},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DBLP:conf/emsoft/CaspiB02,
	author    = {Paul Caspi and
	Albert Benveniste},
	title     = {Toward an Approximation Theory for Computerised Control},
	booktitle = { {EMSOFT}},
	pages     = {294--304},
	year      = {2002},
	timestamp = {Mon, 04 Jul 2011 09:36:36 +0200},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/emsoft/CaspiB02},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}	crossref  = {DBLP:conf/emsoft/2002},
url       = {http://dx.doi.org/10.1007/3-540-45828-X_22},
doi       = {10.1007/3-540-45828-X_22},
@proceedings{DBLP:conf/emsoft/2002,
	editor    = {Alberto L. Sangiovanni{-}Vincentelli and
	Joseph Sifakis},
	title     = {Embedded Software, Second International Conference, {EMSOFT} 2002,
	Grenoble, France, October 7-9, 2002, Proceedings},
	series    = {Lecture Notes in Computer Science},
	volume    = {2491},
	publisher = {Springer},
	year      = {2002},
	isbn      = {3-540-44307-X},
	timestamp = {Tue, 29 Oct 2002 11:33:53 +0100},
	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/emsoft/2002},
	bibsource = {dblp computer science bibliography, http://dblp.org}
}

license: MIT

license_type: permissive

branch_name: refs/heads/main

extension: bib


text:
/*=========== 兼容IE8/9下checkbox/raido文字样式;如项目使用的icheck请注释 ===========*/
.radio-inline,
.checkbox-inline {
	line-height: 26px;
}
.radio-inline .mgr,
.checkbox-inline .mgc {
	margin-top: 5px !important;
}
.avatar-wrapper img{
	max-width: none;
}
.avatar-wrapper .jcrop-holder.jcrop-light{
	margin: 0 auto;
}
.checkbox-table{
	padding-left: 25px;
}

branch_name: refs/heads/master


text:
@define-color tone1 #1d212e;
@define-color tone2 #1c2541;
@define-color tone3 #3a506b;
@define-color tone4 #5bc0be;
@define-color tone5 #6fffe9;

window {
    /*background-color: @tone1;*/
    background-color: #2a2a2a;
    border-color: #10615c;
}

window decoration{
    box-shadow: none;
}

.grid{
	background-image: none;
	background-color: @tone1;
	border:none;
	border-bottom:1px solid ;

}

label{
	color: #dddddd;
}

#lbl_fields{
	color: #FFFFFF;
	font-weight: bold;
}

#title{
 	color: #FFFFFF;
 	font-size: 20px;
}

entry{
	margin:5px;
	padding: 5px;
	border-radius: 0px;
	border:1px solid #535353;

}

entry:focus{
	background-image: none;
	background-color: #DDDD88;
}

headerbar {
    background-color: @tone3;
    border-color: #10615c;
    border-radius: 0px;
    border:0px;
}

headerbar box.horizontal button{
	margin: 0px;
}

headerbar box.horizontal.right button.titlebutton{
	/*background-color:#ff00ff;*/
	border-radius:100%;
	padding: 2px;
}

/*******************************************************************************
                            button
*******************************************************************************/

button {
	background-image: none;
	background-color: @tone3;
	color: #FFFFFF;
	border-radius:0px;
	border:none;
	border-bottom:1px solid @tone3;
	box-shadow: none;
	padding: 5px;
	font-size:12px;
}

button:hover{
    background-image: none;
    background-color: @tone4;
}

button:active{
    background-color: @tone2;
}
/*
button.titlebutton.close {
  background-color: #ec7063 ;
  color: white;
}

button.titlebutton.close:hover {
  background-color: #cd6155 ;
}

button.titlebutton.close:active{
    background-color:  #cb4335 ;
}
*/

/******************************************************************************/

switch slider{
	background-color:@tone3;
	color: #FFFFFF;
}

switch {
	background-color: @tone2;
	background-image: none;
	margin: 5px;
}

switch:checked{
	background-color: @tone5;
}

combobox window menu{
	background-color: @tone3;
	color: #FFFFFF;
}

combobox window menu menuitem:hover{
	background-color: @tone4;
}

treeview{
	background-color:#333333;
}

repository: GustavoAle/misc

repo_name: GustavoAle/misc

extension: css


text:
require ${BPN}.inc

DEPENDS += " \
    ${BPN}-native \
    glib-2.0-native \
    glib-2.0 \
    dbus \
    iso-codes \
"

inherit gtk-icon-cache bash-completion features_check

# for unicode-ucd
EXTRA_OECONF += "--with-ucd-dir=${STAGING_DATADIR}/unicode/ucd"

PACKAGECONFIG ??= " \
    dconf vala \
    ${@bb.utils.contains_any('DISTRO_FEATURES', [ 'wayland', 'x11' ], 'gtk3 gtk4', '', d)} \
    ${@bb.utils.filter('DISTRO_FEATURES', 'systemd wayland x11', d)} \
"

REQUIRED_DISTRO_FEATURES = "${@bb.utils.contains('PACKAGECONFIG', 'gtk4', 'opengl', '', d)}"

do_configure:prepend() {
    # run native unicode-parser
    sed -i 's:$(builddir)/unicode-parser:unicode-parser:g' ${S}/src/Makefile.am
}

FILES:${PN} += " \
    ${datadir}/dbus-1 \
    ${datadir}/GConf \
    ${datadir}/glib-2.0 \
    ${libdir}/gtk-3.0 \
    ${libdir}/gtk-4.0 \
    ${systemd_user_unitdir} \
"

FILES:${PN}-dev += " \
    ${datadir}/gettext \
"
RDEPENDS:${PN} += "python3-core"

repository: openembedded/meta-openembedded

repo_name: openembedded/meta-openembedded

gha_license_id: MIT

gha_language: BitBake

extension: bb