M. Aiello, I. Pratt-Hartmann & J. (editors) van Benthem (2007):
Handbook of Spatial Logics.
Springer,
doi:10.1007/978-1-4020-5587-4.
A. Aziz, K. Sanwal, V. Singhal & R. Brayton (2000):
Model checking Continuous Time Markov Chains.
ACM Transactions on Computational Logic 1(1),
pp. 162–170,
doi:10.1145/343369.343402.
C. Baier, B. Haverkort, H. Hermanns & J.-P. Katoen (2003):
Model-Checking Algorithms for Continuous-Time Markov Chains.
IEEE Transactions on Software Engineering. IEEE CS 29(6),
pp. 524–541,
doi:10.1109/TSE.2003.1205180.
M. Bernardo, R. De Nicola & J. Hillston (2016):
Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems.
LNCS 9700.
Springer.
L. Bortolussi & J. Hillston (2015):
Model checking single agent behaviours by fluid approximation.
Inf. Comput. 242,
pp. 183–226,
doi:10.1016/j.ic.2015.03.002.
L. Bortolussi & J. Hillston (2012):
Fluid Model Checking.
In: M. Koutny & I. Ulidowski: CONCUR,
LNCS 7454.
Springer,
pp. 333–347,
doi:10.1007/978-3-642-32940-1_24.
V. Ciancia, S. Gilmore, D. Latella, M. Loreti & M. Massink (2014):
Data verification for collective adaptive systems: spatial model-checking of vehicle location data.
In: FoCAS Workshp @ SASO - 2014 IEEE Eighth International Conference on Self-Adaptive and Self-Organizing Systems Workshops.
IEEE.
Computer Society Press,
pp. 32–37,
doi:10.1109/SASOW.2014.16.
V. Ciancia, D. Latella & M. Massink (2015):
On Space in CARMA.
Technical Report TR-QC-01-2015.
QUANTICOL.
V. Ciancia, G. Grilletti, D. Latella, M. Loreti & M. Massink (2015):
An Experimental Spatio-Temporal Model Checker.
In: D. Bianculli, R. Clinescu & B. Rumpe: Software Engineering and Formal Methods (SEFM 2015). Co-located Workshops, York, UK, September 7-8, 2015. Revised Selected Papers,
LNCS 9509.
Springer,
pp. 297–311,
doi:10.1007/978-3-662-49224-6_24.
V. Ciancia, D. Latella, M. Loreti & M. Massink (2014):
Specifying and Verifying Properties of Space.
In: J. Diaz, I. Lanese & D. Sangiorgi: Theoretical Computer Science (TCS 2014),
LNCS 8705.
Springer,
pp. 222–235,
doi:10.1007/978-3-662-44602-7_18.
V. Ciancia, S. Gilmore, G. Grilletti, D. Latella, M. Loreti & M. Massink (2016):
On Spatio-temporal model-checking of vehicular movement in public transport systems - Preliminary Version..
Technical Report TR-QC-02-2016.
QUANTICOL.
V. Ciancia, D. Latella, M. Loreti & M. Massink (2016):
Model Checking Spatial Logics for Closure Spaces - Extended Version..
Technical Report TR-QC-03-2016.
QUANTICOL.
V. Ciancia, D. Latella, M. Loreti & M. Massink (2016):
Spatial Logic and Spatial Model Checking for Closure Spaces.
In: Bernardo, chapter 6,
pp. 156–201,
doi:10.1007/978-3-319-34096-8_6.
V. Ciancia, D. Latella & M. Massink (2016):
On-the-Fly Mean-field Model-checking for Attribute-based Coordination.
In: A. Lluch Lafuente & J. Proença: Coordination Models and Languages,
LNCS 9686.
Springer,
pp. 67–83,
doi:10.1007/978-3-319-39519-7_5.
V. Ciancia, M. Latella, D. Massink, R. Paskauskas & A. Vandin (2016):
A Tool-chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems.
In: T. Margaria & B. Steffen: ISoLA 2016, Imperial, Corfu, Greece, October 5-14, 2016, Proceedings,
LNCS.
Springer.
(To appear).
R. De Nicola, D. Latella, A. Lluch Lafuente, M. Loreti, A. Margheri, M. Massink, A. Morichetta, R. Pugliese, F. Tiezzi & A. Vandin (2015):
The SCEL Language: Design, Implementation, Verification.
In: M. Wirsing, M. Hölzl, N. Koch & P. Mayer: Software Engineering for Collective Autonomic Systems, chapter I.1,
LNCS 8998.
Springer,
pp. 3–71,
doi:10.1007/978-3-319-16310-9_1.
A. Galton (2003):
A generalized topological view of motion in discrete space.
Theoretical Computer Science. 305((1-3)),
pp. 111–134,
doi:10.1016/S0304-3975(02)00701-6.
R. Grosu, E. Bartocci, F. Corradini, E. Entcheva, S. Smolka & A. Wasilewska (2008):
Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes.
In: M. Egerstedt & B. Mishra: Hybrid Systems: Computation and Control, 11th International Workshop, (HSCC'08) 2008, St. Louis, MO, USA, April 22-24, 2008. Proceedings,
LNCS 4981.
Springer,
pp. 229–243,
doi:10.1007/978-3-540-78929-1_17.
R. Grosu, S. Smolka, F. Corradini, A. Wasilewska, E. Entcheva & E. Bartocci (2009):
Learning and detecting emergent behavior in networks of cardiac myocytes.
Commun. ACM 52(3),
pp. 97–105,
doi:10.1145/1467247.1467271.
I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Grosu & C. Belta (2015):
SpaTeL: a novel spatial-temporal logic and its applications to networked systems.
In: A. Girard & S. Sankaranarayanan: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC'15) Seattle, WA, USA, April 14-16, 2015.
ACM,
pp. 189–198,
doi:10.1145/2728606.2728633.
H. Hansson & B. Jonsson (1994):
A Logic for Reasoning about Time and Reliability.
Formal Aspects of Computing 6,
pp. 512–535,
doi:10.1007/BF01211866.
C. Jones (2001):
Thinking Tools for the Future of Computing Science.
In: R. Wilhelm: Informatics 10 Years Back 10 Years Ahead,
LNCS 2000.
Springer,
pp. 112–130,
doi:10.1007/3-540-44577-3_8.
A. Kolesnichenko, P.-T. de Boer, A. Remke & B. Haverkort (2013):
A logic for model-checking mean-field models.
In: 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), Budapest, Hungary, June 24-27, 2013.
IEEE Computer Society,
pp. 1–12,
doi:10.1109/DSN.2013.6575345.
A. Kolesnichenko, A. Remke, P.-T. de Boer & B. Haverkort (2012):
A logic for model-checking of mean-field models.
Technical Report TR-CTIT-12-11, http://doc.utwente.nl/80267/.
K. Larsen & A. Legay (2014):
Statistical Model Checking Past, Present, and Future - (Track Introduction).
In: T. Margaria & B. Steffen: 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,
LNCS 8803.
Springer,
pp. 135–142,
doi:10.1007/978-3-662-45231-8_10.
D. Latella, M. Loreti & M. Massink (2013):
On-the-fly PCTL Fast Mean-Field Model-Checking for Self-organising Coordination - Preliminary Version.
Technical Report TR-QC-01-2013.
QUANTICOL.
D. Latella, M. Loreti & M. Massink (2014):
On-the-fly Fast Mean-Field Model-Checking.
In: M. Abadi & A. Lluch Lafuente: Trustworthy Global Computing, 4th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers,
LNCS 8358.
Springer,
pp. 297–314,
doi:10.1007/978-3-319-05119-2_17.
D. Latella, M. Loreti & M. Massink (2015):
On-the-fly Fluid Model Checking via Discrete Time Population Models.
In: M. Beltrán, W. Knottenbelt & J. Bradley: Computer Performance Engineering,
LNCS 9272.
Springer,
pp. 193–207,
doi:10.1007/978-3-319-23267-6_13.
D. Latella, M. Loreti & M. Massink (2015):
On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination.
Science of Computer Programming. 110,
pp. 23–50,
doi:10.1016/j.scico.2015.06.009.
J.-Y. Le Boudec, D. McDonald & J. Mundinger (2007):
A Generic Mean Field Convergence Result for Systems of Interacting Objects.
In: QEST07.
IEEE Computer Society Press,
pp. 3–18,
doi:10.1109/QEST.2007.8.
M. Loreti & J. Hillston (2016):
Modelling and Analysis of Collective Adaptive Systems with CARMA and its Tools.
In: Bernardo, chapter 4,
pp. 83–119,
doi:10.1007/978-3-319-34096-8_4.
L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti & M. Massink (2015):
Qualitative and Quantitative Monitoring of Spatio-Temporal Properties.
In: E. Bertocci & R. Majumdar: Runtime Verification,
LNCS 9333.
Springer,
pp. 21–37,
doi:10.1007/978-3-319-23820-3_2.
S. Sebastio & A. Vandin (2013):
MultiVeStA: statistical model checking for discrete event simulators.
In: A. Horváth, P. Buchholz, V. Cortellessa, L. Muscariello & M. Squillante: 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools '13, Torino, Italy, December 10-12, 2013.
ICST/ACM,
pp. 310–315,
doi:10.4108/icst.valuetools.2013.254377.