@article(Az+00,
 author       = {Adnan Aziz and Kumud Sanwal and Vigyan Singhal and Robert K. Brayton},
 year         = {2000},
 title        = {Model-checking continous-time Markov chains},
 journal      = {{ACM} Trans. Comput. Log.},
 volume       = {1},
 number       = {1},
 pages        = {162--170},
 doi          = {10.1145/343369.343402},
)
@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} Trans. Software Eng.},
 volume       = {29},
 number       = {6},
 pages        = {524--541},
 doi          = {10.1109/TSE.2003.1205180},
)
@book(BaK08,
 author       = {Christel Baier and Joost{-}Pieter Katoen},
 year         = {2008},
 title        = {Principles of model checking},
 publisher    = {{MIT} Press},
)
@inproceedings(BCG95,
 author       = {Girish Bhat and Rance Cleaveland and Orna Grumberg},
 year         = {1995},
 title        = {Efficient On-the-Fly Model Checking for CTL*},
 booktitle    = {Proceedings, 10th Annual {IEEE} Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995},
 publisher    = {{IEEE} Computer Society},
 pages        = {388--397},
 doi          = {10.1109/LICS.1995.523273},
)
@incollection(Bo+15,
 author       = {L. Bortolussi and G. Cabri and {Di Marzo Serugendo}, G. and V. Galpin and J. Hillston and R. Lanciani and M. Massink and D. Tribastone, M. Weyns},
 year         = {2015},
 title        = {{Verification of CAS}},
 editor       = {J. Hillston and J. Pitt and M. Wirsing and F. Zambonelli},
 booktitle    = {Collective Adaptive Systems: Qualitative and Quantitative Modelling and Analysis},
 publisher    = {{Schloss Dagstuhl - Leibniz-Zentrum f\"ur Informatik, Dagstuhl Publishing, Germany}},
 pages        = {91--102},
 note         = {{Dagstuhl Reports. Vol. 4, Issue 12. Report from Dagstuhl Seminar 14512. ISSN 2192-5283}},
)
@inproceedings(BoH12b,
 author       = {Luca Bortolussi and Jane Hillston},
 year         = {2012},
 title        = {Fluid Model Checking},
 editor       = {Maciej Koutny and Irek Ulidowski},
 booktitle    = {{CONCUR} 2012 - Concurrency Theory - 23rd International Conference, {CONCUR} 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7454},
 publisher    = {Springer},
 pages        = {333--347},
 doi          = {10.1007/978-3-642-32940-1_24},
)
@article(BoH15,
 author       = {Luca Bortolussi and Jane Hillston},
 year         = {2015},
 title        = {Model checking single agent behaviours by fluid approximation},
 journal      = {Inf. Comput.},
 volume       = {242},
 pages        = {183--226},
 doi          = {10.1016/j.ic.2015.03.002},
)
@inproceedings(BMM07,
 author       = {Jean{-}Yves Le Boudec and David D. McDonald and Jochen Mundinger},
 year         = {2007},
 title        = {A Generic Mean Field Convergence Result for Systems of Interacting Objects},
 booktitle    = {Fourth International Conference on the Quantitative Evaluaiton of Systems {(QEST} 2007), 17-19 September 2007, Edinburgh, Scotland, {UK}},
 publisher    = {{IEEE} Computer Society},
 pages        = {3--18},
 doi          = {10.1109/QEST.2007.8},
)
@inproceedings(CLM16a,
 author       = {Vincenzo Ciancia and Diego Latella and Mieke Massink},
 year         = {2016},
 title        = {On-the-Fly Mean-Field Model-Checking for Attribute-Based Coordination},
 editor       = {Lluch{-}Lafuente, Alberto and Proen{\c{c}}a, Jos{\'{e}}},
 booktitle    = {Coordination Models and Languages - 18th {IFIP} {WG} 6.1 International Conference, {COORDINATION} 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9686},
 publisher    = {Springer},
 pages        = {67--83},
 doi          = {10.1007/978-3-319-39519-7_5},
)
@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      = {Formal Methods in System Design},
 volume       = {1},
 number       = {2/3},
 pages        = {275--288},
 doi          = {10.1007/BF00121128},
)
@article(DaN08,
 author       = {R.W.R. Darling and J.R. Norris},
 year         = {2008},
 title        = {Differential equation approximations for {Markov} chains},
 journal      = {Probability Surveys},
 volume       = {5},
 pages        = {37--79},
 doi          = {10.1214/07-PS121},
)
@incollection(De+15,
 author       = {{De Nicola}, Rocco and Diego Latella and Lluch{-}Lafuente, Alberto and Michele Loreti and Andrea Margheri and Mieke Massink and Andrea Morichetta and Rosario Pugliese and Francesco Tiezzi and Andrea Vandin},
 year         = {2015},
 title        = {The {SCEL} Language: Design, Implementation, Verification},
 editor       = {Martin Wirsing and Matthias M. H{\"{o}}lzl and Nora Koch and Philip Mayer},
 booktitle    = {Software Engineering for Collective Autonomic Systems - The {ASCENS} Approach},
 series       = {Lecture Notes in Computer Science},
 volume       = {8998},
 publisher    = {Springer},
 pages        = {3--71},
 doi          = {10.1007/978-3-319-16310-9_1},
)
@inproceedings(DIMTV04,
 author       = {{Della Penna}, Giuseppe and Benedetto Intrigila and Igor Melatti and Enrico Tronci and Marisa Venturini Zilli},
 year         = {2004},
 title        = {Bounded Probabilistic Model Checking with the Mur\emph{alpha} Verifier},
 editor       = {Alan J. Hu and Andrew K. Martin},
 booktitle    = {Formal Methods in Computer-Aided Design, 5th International Conference, {FMCAD} 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {3312},
 publisher    = {Springer},
 pages        = {214--229},
 doi          = {10.1007/978-3-540-30494-4_16},
)
@inproceedings(FeH14,
 author       = {Cheng Feng and Jane Hillston},
 year         = {2014},
 title        = {{PALOMA:} {A} Process Algebra for Located Markovian Agents},
 editor       = {Gethin Norman and William H. Sanders},
 booktitle    = {Quantitative Evaluation of Systems - 11th International Conference, {QEST} 2014, Florence, Italy, September 8-10, 2014. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8657},
 publisher    = {Springer},
 pages        = {265--280},
 doi          = {10.1007/978-3-319-10696-0_22},
)
@inproceedings(GaG10,
 author       = {Nicolas Gast and Bruno Gaujal},
 year         = {2010},
 title        = {A mean field model of work stealing in large-scale systems},
 editor       = {Vishal Misra and Paul Barford and Mark S. Squillante},
 booktitle    = {{SIGMETRICS} 2010, Proceedings of the 2010 {ACM} {SIGMETRICS} International Conference on Measurement and Modeling of Computer Systems, New York, New York, USA, 14-18 June 2010},
 publisher    = {{ACM}},
 pages        = {13--24},
 doi          = {10.1145/1811039.1811042},
)
@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    = {Rigorous Software Engineering for Service-Oriented Systems - Results of the {SENSORIA} Project on Software Engineering for Service-Oriented Computing},
 series       = {Lecture Notes in Computer Science},
 volume       = {6582},
 publisher    = {Springer},
 pages        = {390--407},
 doi          = {10.1007/978-3-642-20401-2_18},
)
@article(Gu+06,
 author       = {Guillaume Guirado and Thomas H{\'{e}}rault and Richard Lassaigne and Sylvain Peyronnet},
 year         = {2006},
 title        = {Distribution, Approximation and Probabilistic Model Checking},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {135},
 number       = {2},
 pages        = {19--30},
 doi          = {10.1016/j.entcs.2005.10.016},
)
@inproceedings(Ha+09,
 author       = {Ernst Moritz Hahn and Holger Hermanns and Bj{\"{o}}rn Wachter and Lijun Zhang},
 year         = {2009},
 title        = {{INFAMY:} An Infinite-State Markov Model Checker},
 editor       = {Ahmed Bouajjani and Oded Maler},
 booktitle    = {Computer Aided Verification, 21st International Conference, {CAV} 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5643},
 publisher    = {Springer},
 pages        = {641--647},
 doi          = {10.1007/978-3-642-02658-4_49},
)
@article(HaJ94,
 author       = {Hans Hansson and Bengt Jonsson},
 year         = {1994},
 title        = {A Logic for Reasoning about Time and Reliability},
 journal      = {Formal Asp. Comput.},
 volume       = {6},
 number       = {5},
 pages        = {512--535},
 doi          = {10.1007/BF01211866},
)
@inproceedings(He+04,
 author       = {Thomas H{\'{e}}rault and Richard Lassaigne and Fr{\'{e}}d{\'{e}}ric Magniette and Sylvain Peyronnet},
 year         = {2004},
 title        = {Approximate Probabilistic Model Checking},
 editor       = {Bernhard Steffen and Giorgio Levi},
 booktitle    = {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},
 pages        = {73--84},
 doi          = {10.1007/978-3-540-24622-0_8},
)
@book(Hol04,
 author       = {Gerard J. Holzmann},
 year         = {2004},
 title        = {The {SPIN} Model Checker - primer and reference manual},
 publisher    = {Addison-Wesley},
)
@article(HuT92,
 author       = {D. Huynh and L. Tian},
 year         = {1992},
 title        = {On some equivalence relations for probabilistic processes},
 journal      = {Fundamenta Informaticae},
 volume       = {17},
 pages        = {211--234},
)
@misc(Ko+12,
 author       = {A. Kolesnichenko and A. Remke and {de Boer}, P.-T.},
 year         = {2012},
 title        = {A logic for model-checking of mean-field models},
 howpublished = {Technical Report TR-CTIT-12-11, http://doc.utwente.nl/80267/},
)
@inproceedings(Ko+13,
 author       = {Anna Kolesnichenko and Pieter{-}Tjerk de Boer and Anne Remke and Boudewijn R. Haverkort},
 year         = {2013},
 title        = {A logic for model-checking mean-field models},
 booktitle    = {2013 43rd Annual {IEEE/IFIP} International Conference on Dependable Systems and Networks (DSN), Budapest, Hungary, June 24-27, 2013},
 publisher    = {{IEEE} Computer Society},
 pages        = {1--12},
 doi          = {10.1109/DSN.2013.6575345},
)
@inproceedings(LaL16,
 author       = {Kim G. Larsen and Axel Legay},
 year         = {2016},
 title        = {Statistical Model Checking: Past, Present, and Future},
 editor       = {Tiziana Margaria and Bernhard Steffen},
 booktitle    = {Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part {I}},
 series       = {Lecture Notes in Computer Science},
 volume       = {9952},
 pages        = {3--15},
 doi          = {10.1007/978-3-319-47166-2_1},
)
@misc(Lat83,
 author       = {D. Latella},
 year         = {1983},
 title        = {Comunicazione basata su propriet\`a nei sistemi decentralizzati},
 note         = {[Property-based inter-process communication in decentralized systems] Graduation Thesis. Istituto di Scienze dell'Informazione. Univ. of Pisa, Italy (in italian)},
)
@inproceedings(LLM14,
 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 Lluch{-}Lafuente, Alberto},
 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},
)
@inproceedings(LLM14a,
 author       = {Diego Latella and Michele Loreti and Mieke Massink},
 year         = {2014},
 title        = {On-the-fly Probabilistic Model Checking},
 editor       = {Ivan Lanese and Lluch{-}Lafuente, Alberto and Ana Sokolova and Hugo Torres Vieira},
 booktitle    = {Proceedings 7th Interaction and Concurrency Experience, {ICE} 2014, Berlin, Germany, 6th June 2014.},
 series       = {{EPTCS}},
 volume       = {166},
 pages        = {45--59},
 doi          = {10.4204/EPTCS.166.6},
)
@article(LLM15a,
 author       = {Diego Latella and Michele Loreti and Mieke Massink},
 year         = {2015},
 title        = {On-the-fly {PCTL} fast mean-field approximated model-checking for self-organising coordination},
 journal      = {Sci. Comput. Program.},
 volume       = {110},
 pages        = {23--50},
 doi          = {10.1016/j.scico.2015.06.009},
)
@inproceedings(LoH16,
 author       = {Michele Loreti and Jane Hillston},
 year         = {2016},
 title        = {Modelling and Analysis of Collective Adaptive Systems with {CARMA} and its Tools},
 editor       = {Marco Bernardo and Rocco De Nicola and Jane Hillston},
 booktitle    = {Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems - 16th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, {SFM} 2016, Bertinoro, Italy, June 20-24, 2016, Advanced Lectures},
 series       = {Lecture Notes in Computer Science},
 volume       = {9700},
 publisher    = {Springer},
 pages        = {83--119},
 doi          = {10.1007/978-3-319-34096-8_4},
)