2018
Journal article
Open Access
Qualitative and quantitative monitoring of spatio-temporal properties with SSTL
Nenzi L., Bortolussi L., Ciancia V., Loreti M., Massink M.
Spatio-Temporal Logic Turing Reaction-Diffusion system Statistical Model Checking Bike Sharing Quantitative Semantics Real-Time Verification bike-sharing system Signal Temporal Logic Logic in Computer Science (cs.LO) Monitoring Algorithms FOS: Computer and information sciences Computer Science - Logic in Computer Science Turing Pattern Monitoring F.4.1
In spatially located, large scale systems, time and space dynamics interact and drives the behaviour. Examples of such systems can be found in many smart city applications and Cyber-Physical Systems. In this paper we present the Signal Spatio-Temporal Logic (SSTL), a modal logic that can be used to specify spatio-temporal properties of linear time and discrete space models. The logic is equipped with a Boolean and a quantitative semantics for which ecient monitoring algorithms have been developed. As such, it is suitable for real-time verication of both white box and black box complex systems. These algorithms can also be combined with stochastic model checking routines. SSTL combines the until temporal modality with two spatial modalities, one expressing that something is true somewhere nearby and the other capturing the notion of being surrounded by a region that satises a given spatio-temporal property. The monitoring algorithms are implemented in an open source Java tool. We illustrate the use of SSTL analysing the formation of patterns in a Turing Reaction-Diusion system and spatio-temporal aspects of a large bike-sharing system.
Source: Logical Methods in Computer Science 14 (2018): 1–38. doi:10.23638/LMCS-14(4:2)2018
Publisher: Technische Universität Braunschweig, Institute of Theoretical Computer Science, Braunschweig, Germany, Germania
[1] Aiello, M., Pratt-Hartmann, I., van Benthem, J. (eds.): Handbook of Spatial Logics. Springer (2007)
[2] Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. J. ACM (1996)
[3] Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theoretical Computer Science (2015)
[4] Bortolussi, L., Nenzi, L.: Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In: Proc. of VALUETOOLS (2014)
[5] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Proc. of IFIPTCS (2014)
[6] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: M. Bernardo et al. (ed.) 16th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Quantitative Evaluation of Collective Adaptive System, LNCS, vol. 9700, pp. 156-201. Springer (2016)
[7] Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model-checking of vehicular movement in public transport systems. International Journal on Software Tools for Technology Transfer STTT, Accepted for publication (2017)
[8] Ciancia, V., Gilmore, S., Latella, D., Loreti, M., Massink, M.: Data verification for collective adaptive systems: Spatial model-checking of vehicle location data. In: Proc. of SASOW (2014)
[9] Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART, York, UK, September 7-8, 2015, Revised Selected Papers. LNCS, vol. 9509, pp. 297-311. Springer (2015)
[10] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science Volume 12, Issue 4 (Oct 2016), http://lmcs.episciences.org/2067
[11] Ciancia, V., Latella, D., Massink, M., Pasˇkauskas, R.: Exploring spatio-temporal properties of bike-sharing systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops 2015, Cambridge, MA, USA, September 21-25, 2015. pp. 74-79. IEEE Computer Society (2015), http://dx.doi.org/10.1109/SASOW.2015.17
[12] Ciancia, V., Latella, D., Massink, M., Pasˇkauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) 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. LNCS, vol. 9952, pp. 657-673. Springer (2016)
[13] Donze´, A., Ferrer, T., Maler, O.: Efficient robust monitoring for stl. In: Proc. of CAV (2013) Proposition A.1. Let dG be the diameter of the graph G and X (`) the fixed point of X (i; `), then X (`) = X (dG + 1; `) for all ` ∈ L.
[2] Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsi cation. In: Proc. of CAV 2015. LNCS, vol. 9207, pp. 356{374. Springer (2015)
[3] Alur, R., Feder, T., Henzinger, T.: The bene ts of relaxing punctuality. J. ACM (1996)
[4] Bae, K., Meseguer, J.: A rewriting-based model checker for the linear temporal logic of rewriting. Electron. Notes Theor. Comput. Sci. 290, 19{36 (Dec 2012), http://dx.doi.org/10.1016/j.entcs.2012.11.009
[5] Barbot, B., Chen, T., Han, T., Katoen, J.P., Mereacre, A.: E cient CTMC model checking of linear real-time objectives. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 128{142. Springer (2011)
[6] Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theoretical Computer Science (2015)
[7] Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective systems behaviour: a tutorial. Performance Evaluation 70(5), 317{349 (May 2013)
[8] Bortolussi, L., Nenzi, L.: Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In: Proc. of VALUETOOLS (2014)
[9] Bortolussi, L., Policriti, A., Silvetti, S.: Logic-based multi-objective design of chemical reaction networks. In: Proc. of Hybrid Systems Biology. pp. 164{178 (2016)
[10] Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: Proc. of TACAS (2018)
[11] Bortolussi, L., Galpin, V., Hillston, J.: Hybrid performance modelling of opportunistic networks. In: Proceedings 10th Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2012, Tallinn, Estonia, 31 March and 1 April 2012. pp. 106{121 (2012), http://dx.doi.org/10.4204/ EPTCS.85.8
[12] Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106{137 (2012), http://dblp.uni-trier.de/db/journals/iandc/iandc211.html#BrocheninDL12
[13] Cardelli, L., Gardner, P., Ghelli, G.: A spatial logic for querying graphs. In: Widmayer, P., Ruiz, F.T., Bueno, R.M., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP. Lecture Notes in Computer Science, vol. 2380, pp. 597{610. Springer (2002), http://dblp.uni-trier.de/db/conf/icalp/icalp2002.html# CardelliGG02
[14] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Proc. of IFIP-TCS (2014)
[15] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: M. Bernardo et al. (ed.) 16th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Quantitative Evaluation of Collective Adaptive System, LNCS, vol. 9700, pp. 156{201. Springer (2016)
[16] Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal modelchecking of vehicular movement in public transport systems. International Journal on Software Tools for Technology Transfer STTT, Online rst publication. (2018), https://doi.org/10.1007/ s10009-018-0483-8
[17] Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART, York, UK, September 7-8, 2015, Revised Selected Papers. LNCS, vol. 9509, pp. 297{311. Springer (2015)
[18] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science Volume 12, Issue 4 (Oct 2016), http://lmcs.episciences.org/ 2067
[19] Ciancia, V., Latella, D., Massink, M., Paskauskas, R.: Exploring spatio-temporal properties of bikesharing systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops 2015, Cambridge, MA, USA, September 21-25, 2015. pp. 74{79. IEEE Computer Society (2015), http://dx.doi.org/10.1109/SASOW.2015.17
[20] Ciancia, V., Latella, D., Massink, M., Paskauskas, R., Vandin, A.: A tool-chain for statistical spatiotemporal model checking of bike sharing systems. In: Margaria, T., Ste en, B. (eds.) Leveraging Applications of Formal Methods, Veri cation and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I. LNCS, vol. 9952, pp. 657{673. Springer (2016)
[21] Conforti, G., Macedonio, D., Sassone, V.: Static bilog: a unifying language for spatial structures. Fundam. Inform. 80(1-3), 91{110 (2007), http://dblp.uni-trier.de/db/journals/fuin/fuin80.html# ConfortiMS07
[22] Donze, A., Ferrer, T., Maler, O.: E cient robust monitoring for stl. In: Proc. of CAV (2013)
[23] Donze, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Proc. of FORMATS (2010)
[24] Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic speci cations for continuous-time signals. Theor. Comput. Sci. (2009)
[25] Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic speci cations for continuous-time signals. Theoretical Computer Science (2009)
[26] Feng, C., Hillston, J., Reijsbergen, D.: Moment-Based Probabilistic Prediction of Bike Availability for Bike-Sharing Systems. In: Quantitative Evaluation of Systems. pp. 139{155. Lecture Notes in Computer Science, Springer, Cham (Aug 2016), https://link.springer.com/chapter/10.1007/ 978-3-319-43425-4_9
[27] Galton, A.: A generalized topological view of motion in discrete space. Theoretical Computer Science 305(1{3), 111 { 134 (2003), http://www.sciencedirect.com/science/article/pii/ S0304397502007016
[28] Galton, A.: The mereotopology of discrete space. In: Freksa, C., Mark, D. (eds.) Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science. Lecture Notes in Computer Science, Springer Berlin Heidelberg (1999)
[29] Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction di usion systems. In: Proc. of CDC (2014)
[30] Haghighi, I., Jones, A., Kong, J.Z., Bartocci, E., R., G., Belta, C.: SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems. In: Proc. of HSCC (2015)
[31] Leppanen, T., Karttunen, M., Barrio, R.A., Kaski, K.: The E ect of Noise on Turing Patterns. ResearchGate 150, 367 (Jan 2003), https://www.researchgate.net/publication/230720532_The_ Effect_of_Noise_on_Turing_Patterns
[32] Lesmes, F., Hochberg, D., Moran, F., Perez-Mercader, J.: Noise-Controlled Self-Replicating Patterns. Physical Review Letters 91(23) (Dec 2003), http://link.aps.org/doi/10.1103/PhysRevLett. 91.238301
[33] Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Proc. FORMATS (2004)
[34] Mari, L., Bertuzzo, E., Righetto, L., Casagrandi, R., Gatto, M., Rodriguez-Iturbe, I., Rinaldo, A.: Modelling cholera epidemics: the role of waterways, human mobility and sanitation. Journal of The Royal Society Interface (2012)
[35] Meseguer, J.: The temporal logic of rewriting: A gentle introduction. In: Concurrency, Graphs and Models. Lecture Notes in Computer Science, vol. 5065, pp. 354{382. Springer (2008), http://dblp. uni-trier.de/db/conf/birthday/montanari2008.html#Meseguer08
[36] Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Runtime Veri cation (RV). LNCS, vol. 9333, p. 21{37. Springer (2015)
[37] Nenzi, L., Bortolussi, L., Loreti, M.: jSSTL - a tool to monitor spatio-temporal properties. In: VALUETOOLS (2016)
[38] Reif, J.H., Sistla, A.: A multiprocess network logic with temporal and spatial modalities. Journal of Computer and System Sciences 30(1), 41{53 (February 1985)
[39] Turing, A.M.: The Chemical Basis of Morphogenesis. Philosophical Transactions of the Royal Society of London B: Biological Sciences (1952)
[40] Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: An empirical study. In: Proc. of 2004, the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain, March 29 - April 2 (2004)
[2] Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. J. ACM (1996)
[3] Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theoretical Computer Science (2015)
[4] Bortolussi, L., Nenzi, L.: Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In: Proc. of VALUETOOLS (2014)
[5] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Proc. of IFIPTCS (2014)
[6] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: M. Bernardo et al. (ed.) 16th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Quantitative Evaluation of Collective Adaptive System, LNCS, vol. 9700, pp. 156-201. Springer (2016)
[7] Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model-checking of vehicular movement in public transport systems. International Journal on Software Tools for Technology Transfer STTT, Accepted for publication (2017)
[8] Ciancia, V., Gilmore, S., Latella, D., Loreti, M., Massink, M.: Data verification for collective adaptive systems: Spatial model-checking of vehicle location data. In: Proc. of SASOW (2014)
[9] Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART, York, UK, September 7-8, 2015, Revised Selected Papers. LNCS, vol. 9509, pp. 297-311. Springer (2015)
[10] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science Volume 12, Issue 4 (Oct 2016), http://lmcs.episciences.org/2067
[11] Ciancia, V., Latella, D., Massink, M., Pasˇkauskas, R.: Exploring spatio-temporal properties of bike-sharing systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops 2015, Cambridge, MA, USA, September 21-25, 2015. pp. 74-79. IEEE Computer Society (2015), http://dx.doi.org/10.1109/SASOW.2015.17
[12] Ciancia, V., Latella, D., Massink, M., Pasˇkauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) 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. LNCS, vol. 9952, pp. 657-673. Springer (2016)
[13] Donze´, A., Ferrer, T., Maler, O.: Efficient robust monitoring for stl. In: Proc. of CAV (2013) Proposition A.1. Let dG be the diameter of the graph G and X (`) the fixed point of X (i; `), then X (`) = X (dG + 1; `) for all ` ∈ L.
[2] Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsi cation. In: Proc. of CAV 2015. LNCS, vol. 9207, pp. 356{374. Springer (2015)
[3] Alur, R., Feder, T., Henzinger, T.: The bene ts of relaxing punctuality. J. ACM (1996)
[4] Bae, K., Meseguer, J.: A rewriting-based model checker for the linear temporal logic of rewriting. Electron. Notes Theor. Comput. Sci. 290, 19{36 (Dec 2012), http://dx.doi.org/10.1016/j.entcs.2012.11.009
[5] Barbot, B., Chen, T., Han, T., Katoen, J.P., Mereacre, A.: E cient CTMC model checking of linear real-time objectives. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 128{142. Springer (2011)
[6] Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theoretical Computer Science (2015)
[7] Bortolussi, L., Hillston, J., Latella, D., Massink, M.: Continuous approximation of collective systems behaviour: a tutorial. Performance Evaluation 70(5), 317{349 (May 2013)
[8] Bortolussi, L., Nenzi, L.: Specifying and monitoring properties of stochastic spatio-temporal systems in signal temporal logic. In: Proc. of VALUETOOLS (2014)
[9] Bortolussi, L., Policriti, A., Silvetti, S.: Logic-based multi-objective design of chemical reaction networks. In: Proc. of Hybrid Systems Biology. pp. 164{178 (2016)
[10] Bortolussi, L., Silvetti, S.: Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: Proc. of TACAS (2018)
[11] Bortolussi, L., Galpin, V., Hillston, J.: Hybrid performance modelling of opportunistic networks. In: Proceedings 10th Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2012, Tallinn, Estonia, 31 March and 1 April 2012. pp. 106{121 (2012), http://dx.doi.org/10.4204/ EPTCS.85.8
[12] Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106{137 (2012), http://dblp.uni-trier.de/db/journals/iandc/iandc211.html#BrocheninDL12
[13] Cardelli, L., Gardner, P., Ghelli, G.: A spatial logic for querying graphs. In: Widmayer, P., Ruiz, F.T., Bueno, R.M., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP. Lecture Notes in Computer Science, vol. 2380, pp. 597{610. Springer (2002), http://dblp.uni-trier.de/db/conf/icalp/icalp2002.html# CardelliGG02
[14] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Proc. of IFIP-TCS (2014)
[15] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Spatial logic and spatial model checking for closure spaces. In: M. Bernardo et al. (ed.) 16th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Quantitative Evaluation of Collective Adaptive System, LNCS, vol. 9700, pp. 156{201. Springer (2016)
[16] Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal modelchecking of vehicular movement in public transport systems. International Journal on Software Tools for Technology Transfer STTT, Online rst publication. (2018), https://doi.org/10.1007/ s10009-018-0483-8
[17] Ciancia, V., Grilletti, G., Latella, D., Loreti, M., Massink, M.: An experimental spatio-temporal model checker. In: Software Engineering and Formal Methods - SEFM 2015 Collocated Workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART, York, UK, September 7-8, 2015, Revised Selected Papers. LNCS, vol. 9509, pp. 297{311. Springer (2015)
[18] Ciancia, V., Latella, D., Loreti, M., Massink, M.: Model Checking Spatial Logics for Closure Spaces. Logical Methods in Computer Science Volume 12, Issue 4 (Oct 2016), http://lmcs.episciences.org/ 2067
[19] Ciancia, V., Latella, D., Massink, M., Paskauskas, R.: Exploring spatio-temporal properties of bikesharing systems. In: 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops 2015, Cambridge, MA, USA, September 21-25, 2015. pp. 74{79. IEEE Computer Society (2015), http://dx.doi.org/10.1109/SASOW.2015.17
[20] Ciancia, V., Latella, D., Massink, M., Paskauskas, R., Vandin, A.: A tool-chain for statistical spatiotemporal model checking of bike sharing systems. In: Margaria, T., Ste en, B. (eds.) Leveraging Applications of Formal Methods, Veri cation and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I. LNCS, vol. 9952, pp. 657{673. Springer (2016)
[21] Conforti, G., Macedonio, D., Sassone, V.: Static bilog: a unifying language for spatial structures. Fundam. Inform. 80(1-3), 91{110 (2007), http://dblp.uni-trier.de/db/journals/fuin/fuin80.html# ConfortiMS07
[22] Donze, A., Ferrer, T., Maler, O.: E cient robust monitoring for stl. In: Proc. of CAV (2013)
[23] Donze, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Proc. of FORMATS (2010)
[24] Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic speci cations for continuous-time signals. Theor. Comput. Sci. (2009)
[25] Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic speci cations for continuous-time signals. Theoretical Computer Science (2009)
[26] Feng, C., Hillston, J., Reijsbergen, D.: Moment-Based Probabilistic Prediction of Bike Availability for Bike-Sharing Systems. In: Quantitative Evaluation of Systems. pp. 139{155. Lecture Notes in Computer Science, Springer, Cham (Aug 2016), https://link.springer.com/chapter/10.1007/ 978-3-319-43425-4_9
[27] Galton, A.: A generalized topological view of motion in discrete space. Theoretical Computer Science 305(1{3), 111 { 134 (2003), http://www.sciencedirect.com/science/article/pii/ S0304397502007016
[28] Galton, A.: The mereotopology of discrete space. In: Freksa, C., Mark, D. (eds.) Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science. Lecture Notes in Computer Science, Springer Berlin Heidelberg (1999)
[29] Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction di usion systems. In: Proc. of CDC (2014)
[30] Haghighi, I., Jones, A., Kong, J.Z., Bartocci, E., R., G., Belta, C.: SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems. In: Proc. of HSCC (2015)
[31] Leppanen, T., Karttunen, M., Barrio, R.A., Kaski, K.: The E ect of Noise on Turing Patterns. ResearchGate 150, 367 (Jan 2003), https://www.researchgate.net/publication/230720532_The_ Effect_of_Noise_on_Turing_Patterns
[32] Lesmes, F., Hochberg, D., Moran, F., Perez-Mercader, J.: Noise-Controlled Self-Replicating Patterns. Physical Review Letters 91(23) (Dec 2003), http://link.aps.org/doi/10.1103/PhysRevLett. 91.238301
[33] Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Proc. FORMATS (2004)
[34] Mari, L., Bertuzzo, E., Righetto, L., Casagrandi, R., Gatto, M., Rodriguez-Iturbe, I., Rinaldo, A.: Modelling cholera epidemics: the role of waterways, human mobility and sanitation. Journal of The Royal Society Interface (2012)
[35] Meseguer, J.: The temporal logic of rewriting: A gentle introduction. In: Concurrency, Graphs and Models. Lecture Notes in Computer Science, vol. 5065, pp. 354{382. Springer (2008), http://dblp. uni-trier.de/db/conf/birthday/montanari2008.html#Meseguer08
[36] Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Runtime Veri cation (RV). LNCS, vol. 9333, p. 21{37. Springer (2015)
[37] Nenzi, L., Bortolussi, L., Loreti, M.: jSSTL - a tool to monitor spatio-temporal properties. In: VALUETOOLS (2016)
[38] Reif, J.H., Sistla, A.: A multiprocess network logic with temporal and spatial modalities. Journal of Computer and System Sciences 30(1), 41{53 (February 1985)
[39] Turing, A.M.: The Chemical Basis of Morphogenesis. Philosophical Transactions of the Royal Society of London B: Biological Sciences (1952)
[40] Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: An empirical study. In: Proc. of 2004, the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain, March 29 - April 2 (2004)
Metrics
Back to previous page
BibTeX entry
@article{oai:it.cnr:prodotti:393208,
title = {Qualitative and quantitative monitoring of spatio-temporal properties with SSTL},
author = {Nenzi L. and Bortolussi L. and Ciancia V. and Loreti M. and Massink M.},
publisher = {Technische Universität Braunschweig, Institute of Theoretical Computer Science, Braunschweig, Germany, Germania},
doi = {10.23638/lmcs-14(4:2)2018 and 10.48550/arxiv.1706.09334},
journal = {Logical Methods in Computer Science},
volume = {14},
pages = {1–38},
year = {2018}
}
0000-0003-1314-0574
