@book(Ai+07,
 author       = {M. Aiello and Pratt-Hartmann, I. and {van Benthem}, J. (editors)},
 year         = {2007},
 title        = {Handbook of Spatial Logics},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4020-5587-4},
)
@article(Az+00,
 author       = {A. Aziz and K. Sanwal and V. Singhal and R. Brayton},
 year         = {2000},
 title        = {{Model checking Continuous Time Markov Chains}},
 journal      = {{ACM Transactions on Computational Logic}},
 volume       = {1},
 number       = {1},
 pages        = {162--170},
 doi          = {10.1145/343369.343402},
)
@article(Ba+03,
 author       = {C. Baier and B. Haverkort and H. Hermanns and J.-P. 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},
)
@book(FMQECAS16,
 editor       = {M. Bernardo and {De Nicola}, R. and J. Hillston},
 year         = {2016},
 title        = {{Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems}},
 series       = {LNCS},
 volume       = {9700},
 publisher    = {Springer},
)
@article(BoH15,
 author       = {L. Bortolussi and J. 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(BoH12b,
 author       = {L. Bortolussi and J. Hillston},
 year         = {2012},
 title        = {Fluid Model Checking},
 editor       = {M. Koutny and I. Ulidowski},
 booktitle    = {CONCUR},
 series       = {LNCS},
 volume       = {7454},
 publisher    = {Springer},
 pages        = {333--347},
 doi          = {10.1007/978-3-642-32940-1\_24},
)
@conference(Ci+14c,
 author       = {V. Ciancia and S. Gilmore and D. Latella and M. Loreti and M. Massink},
 year         = {2014},
 title        = {{Data verification for collective adaptive systems: spatial model-checking of vehicle location data}},
 booktitle    = {{FoCAS Workshp @ SASO - 2014 IEEE Eighth International Conference on Self-Adaptive and Self-Organizing Systems Workshops}},
 organization = {IEEE},
 publisher    = {Computer Society Press},
 pages        = {32--37},
 doi          = {10.1109/SASOW.2014.16},
)
@techreport(CLM15,
 author       = {V. Ciancia and D. Latella and M. Massink},
 year         = {2015},
 title        = {{On Space in CARMA}},
 type         = {Technical Report},
 number       = {TR-QC-01-2015},
 institution  = {QUANTICOL},
)
@conference(Ci+15b,
 author       = {V. Ciancia and G. Grilletti and D. Latella and M. Loreti and M. Massink},
 year         = {2015},
 title        = {{An Experimental Spatio-Temporal Model Checker}},
 editor       = {D. Bianculli and R. Clinescu and B. Rumpe},
 booktitle    = {{Software Engineering and Formal Methods (SEFM 2015). Co-located Workshops, York, UK, September 7-8, 2015. Revised Selected Papers}},
 series       = {LNCS},
 volume       = {9509},
 publisher    = {Springer},
 pages        = {297--311},
 doi          = {10.1007/978-3-662-49224-6\_24},
)
@conference(Ci+14a,
 author       = {V. Ciancia and D. Latella and M. Loreti and M. Massink},
 year         = {2014},
 title        = {{Specifying and Verifying Properties of Space}},
 editor       = {J. Diaz and I. Lanese and D. Sangiorgi},
 booktitle    = {{Theoretical Computer Science (TCS 2014)}},
 series       = {LNCS},
 volume       = {8705},
 publisher    = {Springer},
 pages        = {222--235},
 doi          = {10.1007/978-3-662-44602-7\_18},
)
@techreport(Ci+16,
 author       = {V. Ciancia and S. Gilmore and G. Grilletti and D. Latella and M. Loreti and M. Massink},
 year         = {2016},
 title        = {{On Spatio-temporal model-checking of vehicular movement in public transport systems - Preliminary Version.}},
 type         = {Technical Report},
 number       = {TR-QC-02-2016},
 institution  = {QUANTICOL},
)
@techreport(Ci+16a,
 author       = {V. Ciancia and D. Latella and M. Loreti and M. Massink},
 year         = {2016},
 title        = {{Model Checking Spatial Logics for Closure Spaces - Extended Version.}},
 type         = {Technical Report},
 number       = {TR-QC-03-2016},
 institution  = {QUANTICOL},
)
@incollection(Ci+16b,
 author       = {V. Ciancia and D. Latella and M. Loreti and M. Massink},
 year         = {2016},
 title        = {{Spatial Logic and Spatial Model Checking for Closure Spaces}},
 editor       = {Bernardo},
 chapter      = {6},
 pages        = {156--201},
 doi          = {10.1007/978-3-319-34096-8\_6},
)
@conference(CLM16a,
 author       = {V. Ciancia and D. Latella and M. Massink},
 year         = {2016},
 title        = {{On-the-Fly Mean-field Model-checking for Attribute-based Coordination}},
 editor       = {{Lluch Lafuente}, A. and Proen\c{c}a, J.},
 booktitle    = {Coordination Models and Languages},
 series       = {LNCS},
 volume       = {9686},
 publisher    = {Springer},
 pages        = {67--83},
 doi          = {10.1007/978-3-319-39519-7\_5},
)
@inproceedings(Ci+16x,
 author       = {V. Ciancia and M. Latella, D. Massink and R. Paskauskas and A. Vandin},
 year         = {2016},
 title        = {A Tool-chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems},
 editor       = {T. Margaria and B. Steffen},
 booktitle    = {ISoLA 2016, Imperial, Corfu, Greece, October 5-14, 2016, Proceedings},
 series       = {LNCS},
 publisher    = {Springer},
 note         = {(To appear)},
)
@incollection(De+15,
 author       = {{De Nicola}, R. and D. Latella and {Lluch Lafuente}, A. and M. Loreti and A. Margheri and M. Massink and A. Morichetta and R. Pugliese and F. Tiezzi and A. Vandin},
 year         = {2015},
 title        = {{The SCEL Language: Design, Implementation, Verification}},
 editor       = {M. Wirsing and M. {H\"olzl} and N. Koch and P. Mayer},
 booktitle    = {{Software Engineering for Collective Autonomic Systems}},
 chapter      = {I.1},
 series       = {LNCS},
 volume       = {8998},
 publisher    = {Springer},
 pages        = {3--71},
 doi          = {10.1007/978-3-319-16310-9\_1},
)
@article(Gal03,
 author       = {A. Galton},
 year         = {2003},
 title        = {{A generalized topological view of motion in discrete space}},
 journal      = {Theoretical Computer Science.},
 volume       = {305},
 number       = {(1-3)},
 pages        = {111--134},
 doi          = {10.1016/S0304-3975(02)00701-6},
)
@inproceedings(Gr+08,
 author       = {R. Grosu and E. Bartocci and F. Corradini and E. Entcheva and S. Smolka and A. Wasilewska},
 year         = {2008},
 title        = {Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes},
 editor       = {M. Egerstedt and B. Mishra},
 booktitle    = {Hybrid Systems: Computation and Control, 11th International Workshop, (HSCC'08) 2008, St. Louis, MO, USA, April 22-24, 2008. Proceedings},
 series       = {LNCS},
 volume       = {4981},
 publisher    = {Springer},
 pages        = {229--243},
 doi          = {10.1007/978-3-540-78929-1\_17},
)
@article(Gr+09,
 author       = {R. Grosu and S. Smolka and F. Corradini and A. Wasilewska and E. Entcheva and E. Bartocci},
 year         = {2009},
 title        = {Learning and detecting emergent behavior in networks of cardiac myocytes},
 journal      = {Commun. {ACM}},
 volume       = {52},
 number       = {3},
 pages        = {97--105},
 doi          = {10.1145/1467247.1467271},
)
@inproceedings(Ha+15,
 author       = {I. Haghighi and A. Jones and Z. Kong and E. Bartocci and R. Grosu and C. Belta},
 year         = {2015},
 title        = {SpaTeL: a novel spatial-temporal logic and its applications to networked systems},
 editor       = {A. Girard and S. Sankaranarayanan},
 booktitle    = {Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC'15) Seattle, WA, USA, April 14-16, 2015},
 publisher    = {{ACM}},
 pages        = {189--198},
 doi          = {10.1145/2728606.2728633},
)
@article(Hansson1994,
 author       = {H. Hansson and B. 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},
)
@conference(Jon00,
 author       = {C. Jones},
 year         = {2001},
 title        = {{Thinking Tools for the Future of Computing Science}},
 editor       = {R. Wilhelm},
 booktitle    = {{Informatics 10 Years Back 10 Years Ahead}},
 series       = {LNCS},
 volume       = {2000},
 publisher    = {Springer},
 pages        = {112--130},
 doi          = {10.1007/3-540-44577-3\_8},
)
@inproceedings(Ko+13,
 author       = {A. Kolesnichenko and {de Boer}, P.-T. and A. Remke and B. 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},
)
@misc(Ko+12,
 author       = {A. Kolesnichenko and A. Remke and {de Boer}, P.-T. and B. Haverkort},
 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(LaL14,
 author       = {K. Larsen and A. Legay},
 year         = {2014},
 title        = {Statistical Model Checking Past, Present, and Future - (Track Introduction)},
 editor       = {T. Margaria and B. Steffen},
 booktitle    = {Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part {II}},
 series       = {LNCS},
 volume       = {8803},
 publisher    = {Springer},
 pages        = {135--142},
 doi          = {10.1007/978-3-662-45231-8\_10},
)
@techreport(LLM13b,
 author       = {D. Latella and M. Loreti and M. 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}},
)
@conference(LLM14,
 author       = {D. Latella and M. Loreti and M. Massink},
 year         = {2014},
 title        = {{On-the-fly Fast Mean-Field Model-Checking}},
 editor       = {M. Abadi and {Lluch Lafuente}, A.},
 booktitle    = {{Trustworthy Global Computing, 4th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers}},
 series       = {LNCS},
 volume       = {8358},
 publisher    = {Springer},
 pages        = {297--314},
 doi          = {10.1007/978-3-319-05119-2\_17},
)
@conference(LLM15b,
 author       = {D. Latella and M. Loreti and M. Massink},
 year         = {2015},
 title        = {{On-the-fly Fluid Model Checking via Discrete Time Population Models}},
 editor       = {M. Beltr\'an and W. Knottenbelt and J. Bradley},
 booktitle    = {Computer Performance Engineering},
 series       = {LNCS},
 volume       = {9272},
 publisher    = {Springer},
 pages        = {193--207},
 doi          = {10.1007/978-3-319-23267-6\_13},
)
@article(LLM15a,
 author       = {D. Latella and M. Loreti and M. Massink},
 year         = {2015},
 title        = {{On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination}},
 journal      = {Science of Computer Programming.},
 volume       = {110},
 pages        = {23--50},
 doi          = {10.1016/j.scico.2015.06.009},
)
@inproceedings(BMM07,
 author       = {{Le Boudec}, J.-Y. and D. McDonald and J. 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.8},
)
@incollection(LoH16,
 author       = {M. Loreti and J. Hillston},
 year         = {2016},
 title        = {{Modelling and Analysis of Collective Adaptive Systems with CARMA and its Tools}},
 editor       = {Bernardo},
 chapter      = {4},
 pages        = {83--119},
 doi          = {10.1007/978-3-319-34096-8\_4},
)
@conference(Ne+15,
 author       = {L. Nenzi and L. Bortolussi and V. Ciancia and M. Loreti and M. Massink},
 year         = {2015},
 title        = {{Qualitative and Quantitative Monitoring of Spatio-Temporal Properties}},
 editor       = {E. Bertocci and R. Majumdar},
 booktitle    = {Runtime Verification},
 series       = {LNCS},
 volume       = {9333},
 publisher    = {Springer},
 pages        = {21--37},
 doi          = {10.1007/978-3-319-23820-3\_2},
)
@inproceedings(SeV13,
 author       = {S. Sebastio and A. Vandin},
 year         = {2013},
 title        = {MultiVeStA: statistical model checking for discrete event simulators},
 editor       = {A. Horv{\'{a}}th and P. Buchholz and V. Cortellessa and L. Muscariello and M. Squillante},
 booktitle    = {7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools '13, Torino, Italy, December 10-12, 2013},
 publisher    = {{ICST/ACM}},
 pages        = {310--315},
 doi          = {10.4108/icst.valuetools.2013.254377},
)