@article(BDG06,
 author       = "Christel Baier and Pedro R. D'Argenio and Marcus Grober",
 year         = "2006",
 title        = "Partial Order Reduction for Probabilistic Branching Time",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "153",
 number       = "2",
 pages        = "97--116",
 doi          = "10.1016/j.entcs.2005.10.034",
)
@article(Ba+03,
 author       = "Christel Baier and Boudewijn R. Haverkort and Holger Hermanns and Joost-Pieter Katoen",
 year         = "2003",
 title        = "{Model-Checking Algorithms for Continuous-Time Markov Chains}",
 journal      = "{IEEE} Transactions on Software Engineering. IEEE CS",
 volume       = "29",
 number       = "6",
 pages        = "524--541",
 doi          = "10.1109/TSE.2003.1205180",
)
@inproceedings(BCG95,
 author       = "Girish Bhat and Rance Cleaveland and Orna Grumberg",
 year         = "1995",
 title        = "Efficient On-the-Fly Model Checking for {CTL*}",
 booktitle    = "LICS",
 publisher    = "IEEE Computer Society",
 pages        = "388--397",
 doi          = "10.1109/LICS.1995.523273",
)
@article(Clarke1986,
 author       = "Edmund M. Clarke and E. A. Emerson and A. P. Sistla",
 year         = "1986",
 title        = "Automatic verification of finite-state concurrent systems using temporal logic specifications",
 journal      = "ACM Trans. Program. Lang. Syst.",
 volume       = "8",
 number       = "2",
 pages        = "244--263",
 doi          = "10.1145/5397.5399",
)
@article(Courcoubetis1992,
 author       = "Costas Courcoubetis and Moshe Y. Vardi and Pierre Wolper and Mihalis Yannakakis",
 year         = "1992",
 title        = "Memory-efficient algorithms for the verification of temporal properties",
 journal      = "Form. Methods Syst. Des.",
 volume       = "1",
 number       = "2-3",
 pages        = "275--288",
 doi          = "10.1007/BF00121128",
)
@article(FBBF12,
 author       = "Alvaro Fernandez-Diaz and Christel Baier and Clara Benac-Earle and Lars-Ake Fredlund",
 year         = "2012",
 title        = "Static Partial Order Reduction for Probabilistic Concurrent Systems",
 journal      = "QEST 2012",
 volume       = "0",
 pages        = "104--113",
 doi          = "10.1109/QEST.2012.22",
)
@incollection(GnM11,
 author       = "Stefania Gnesi and Franco Mazzanti",
 year         = "2011",
 title        = "An Abstract, on the Fly Framework for the Verification of Service-Oriented Systems",
 editor       = "Martin Wirsing and Matthias M. H{\"o}lzl",
 booktitle    = "Results of the SENSORIA Project",
 series       = "LNCS",
 volume       = "6582",
 publisher    = "Springer",
 pages        = "390--407",
 doi          = "10.1007/978-3-642-20401-2\_18",
)
@article(HHWZ09,
 author       = "Ernst Moritz Hahn and Holger Hermanns and Bj{\"o}rn Wachter and Lijun Zhang",
 year         = "2009",
 title        = "Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains",
 journal      = "Fundam. Inform.",
 volume       = "95",
 number       = "1",
 pages        = "129--155",
 doi          = "10.3233/FI-2009-145",
)
@article(Hansson1994,
 author       = "Hans Hansson and Bengt Jonsson",
 year         = "1994",
 title        = "A Logic for Reasoning about Time and Reliability",
 journal      = "Formal Aspects of Computing",
 volume       = "6",
 pages        = "512--535",
 doi          = "10.1007/BF01211866",
)
@article(Her90,
 author       = "Ted Herman",
 year         = "1990",
 title        = "Probabilistic Self-Stabilization",
 journal      = "Inf. Process. Lett.",
 volume       = "35",
 number       = "2",
 pages        = "63--67",
 doi          = "10.1016/0020-0190(90)90107-9",
)
@book(Hol04,
 author       = "Gerard J. Holzmann",
 year         = "2004",
 title        = "The SPIN Model Checker - primer and reference manual",
 publisher    = "Addison-Wesley",
)
@book(Kemeny1976,
 author       = "J. G. Kemeny and J. L. Snell and A. W. Knapp",
 year         = "1976",
 title        = "Denumerable Markov Chains",
 publisher    = "Springer-Verlag",
 address      = "New York, USA",
 doi          = "10.1007/978-1-4684-9455-6",
)
@article(KNP04,
 author       = "Marta Z. Kwiatkowska and Gethin Norman and David Parker",
 year         = "2004",
 title        = "Probabilistic symbolic model checking with PRISM: a hybrid approach",
 journal      = "STTT",
 volume       = "6",
 number       = "2",
 pages        = "128--142",
 doi          = "10.1007/s10009-004-0140-2",
)
@inproceedings(La+13a,
 author       = "Diego Latella and Michele Loreti and Mieke Massink",
 year         = "2013",
 title        = "On-the-fly Fast Mean-Field Model-Checking",
 editor       = "Mart\'{\i }n Abadi and Alberto Lluch-Lafuente",
 booktitle    = "Trustworthy Global Computing - 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers",
 series       = "Lecture Notes in Computer Science",
 volume       = "8358",
 publisher    = "Springer",
 pages        = "297--314",
 doi          = "10.1007/978-3-319-05119-2\_17",
)
@techreport(LLM13b,
 author       = "Diego Latella and Michele Loreti and Mieke Massink",
 year         = "2013",
 title        = "On-the-fly PCTL Fast Mean-Field Model-Checking for Self-organising Coordination - Preliminary Version",
 type         = "Technical Report",
 number       = "TR-QC-01-2013",
 institution  = "Quanticol Technical Report",
 note         = "Available on-line at \url {http://www.quanticol.eu}",
)
@inproceedings(BMM07,
 author       = "Jean-Yves {Le Boudec} and David McDonald and Jochen Mundinger",
 year         = "2007",
 title        = "A Generic Mean Field Convergence Result for Systems of Interacting Objects",
 booktitle    = "QEST07",
 publisher    = "{IEEE} Computer Society Press",
 pages        = "3--18",
 doi          = "10.1109/QEST.2007.3",
 note         = "ISBN 978-0-7695-2883-0",
)
@article(DIMTV04,
 author       = "Giuseppe Della Penna and Benedetto Intrigila and Igor Melatti and Enrico Tronci and Marisa Venturini Zilli",
 year         = "2006",
 title        = "Finite horizon analysis of Markov Chains with the Murphi verifier",
 journal      = "STTT",
 volume       = "8",
 number       = "4-5",
 pages        = "397--409",
 doi          = "10.1007/s10009-005-0216-7",
)
@inproceedings(Pnueli1977,
 author       = "Amir Pnueli",
 year         = "1977",
 title        = "The temporal logic of programs",
 booktitle    = "SFCS '77: Proceedings of the 18th Annual Symposium on Foundations of Computer Science ({SFCS} 1977)",
 publisher    = "IEEE Computer Society",
 address      = "Washington, DC, USA",
 pages        = "46--57",
 doi          = "10.1109/SFCS.1977.32",
)
@article(RoV10,
 author       = "Kristin Y. Rozier and Moshe Y. Vardi",
 year         = "2010",
 title        = "{LTL} satisfiability checking",
 journal      = "STTT",
 volume       = "12",
 number       = "2",
 pages        = "123--137",
 doi          = "10.1007/s10009-010-0140-3",
)
@inproceedings(Younes2004,
 author       = "H{\r a}kan L. S. Younes and Marta Z. Kwiatkowska and Gethin Norman and David Parker",
 year         = "2004",
 title        = "Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study",
 editor       = "K. Jensen and A. Podelski",
 booktitle    = "Proc. 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04)",
 series       = "LNCS",
 volume       = "2988",
 publisher    = "Springer",
 pages        = "46--60",
 doi          = "10.1007/978-3-540-24730-2\_4",
)