2016
Journal article
Open Access
Model checking spatial logics for closure spaces
Ciancia V., Latella D., Loreti M., Massink M.
Closure spaces Closure Spaces Spatial logics Computer Science (all) Topological Spaces General Computer Science Logic in Computer Science (cs.LO) Spatial Logics Modal Logics FOS: Computer and information sciences Collective Adaptive Systems Spatial model checking Theoretical Computer Science Spatial Logics Model-checking Computer Science - Logic in Computer Science Collective logics D.2.4 F.3.1 F.3.2
Spatial aspects of computation are becoming increasingly relevant in Computer Science, especially in the field of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explicitly. We present a topology-based approach to formal verification of spatial properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We extend the framework with a spatial surrounded operator, a propagation operator and with some collective operators. The latter are interpreted over arbitrary sets of points instead of individual points in space. We define efficient model checking procedures, both for the individual and the collective spatial fragments of the logic and provide a proof-of-concept tool.
Source: Logical Methods in Computer Science 12 (2016): 1–51. doi:10.2168/LMCS-12(4:2)2016
Publisher: Technische Universität Braunschweig, Institute of Theoretical Computer Science, Braunschweig, Germany, Germania
[Aie02] Marco Aiello. Spatial Reasoning: Theory and Practice. PhD thesis, Institute of Logic, Language and Computation, University of Amsterdam, 2002.
[APHvB07] Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors. Handbook of Spatial Logics. Springer, 2007.
[AS15] Francesco Luca De Angelis and Giovanna Di Marzo Serugendo. A logic language for run time assessment of spatial properties in self-organizing systems. In 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops 2015, Cambridge, MA, USA, September 21-25, 2015, pages 86{91. IEEE Computer Society, 2015.
[BB07] Johan van Benthem and Guram Bezhanishvili. Modal logics of space. In Aiello et al. [APHvB07], pages 217{298.
[BCLM16] Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. From collective adaptive systems to human centric computation and back: Spatial model checking for medical imaging. In Maurice H. ter Beek and Michele Loreti, editors, Proceedings of the Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, FORECAST@STAF 2016, Vienna, Austria, 8 July 2016., volume 217 of EPTCS, pages 81{92, 2016.
[BHLM13] Luca Bortolussi, Jane Hillston, Diego Latella, and Mieke Massink. Continuous approximation of collective system behaviour: A tutorial. Performance Evaluation, 70(5):317 { 349, 2013.
[BHMU11] Arne T. Bittig, Fiete Haack, Carsten Maus, and Adelinde M. Uhrmacher. Adapting rule-based model descriptions for simulating in continuous and hybrid space. In Francois Fages, editor, Computational Methods in Systems Biology, 9th International Conference, CMSB 2011, Paris, France, September 21-23, 2011. Proceedings, pages 161{170. ACM, 2011.
[BK08] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
[BKL11] Mikolaj Bojanczyk, Bartek Klin, and Slawomir Lasota. Automata with group actions. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 355{364. IEEE Computer Society, 2011.
[CC03] L. Caires and L. Cardelli. A spatial logic for concurrency (part I). Information and Computation, 186(2):194{235, 2003.
[CE82] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Dexter Kozen, editor, Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52{71. Springer Berlin Heidelberg, 1982.
[CG00] Luca Cardelli and Andrew D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), pages 365{377, 2000.
[CG12] Luca Cardelli and Philippa Gardner. Processes in space. Theor. Comput. Sci., 431:40{55, 2012.
[CGG02] Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. A spatial logic for querying graphs. In Peter Widmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew Hennessy, Stephan Eidenbenz, and Ricardo Conejo, editors, Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings, volume 2380 of Lecture Notes in Computer Science, pages 597{610. Springer, 2002.
[CGL+14] Vincenzo Ciancia, Stephen Gilmore, Diego Latella, Michele Loreti, and Mieke Massink. Data veri cation for collective adaptive systems: Spatial model-checking of vehicle location data. In Eighth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW 2014, London, United Kingdom, September 8-12, 2014, pages 32{37. IEEE Computer Society, 2014.
[CGL+15] Vincenzo Ciancia, Gianluca Grilletti, Diego Latella, Michele Loreti, and Mieke Massink. 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, volume 9509 of Lecture Notes in Computer Science, pages 297{311. Springer, 2015.
[CLBR09] Augustin Chaintreau, Jean-Yves Le Boudec, and Nikodin Ristanovic. The age of gossip: Spatial mean eld regime. In Proceedings of the Eleventh International Joint Conference on Measurement and Modeling of Computer Systems, SIGMETRICS '09, pages 109{120, New York, NY, USA, 2009. ACM.
[CLLM14a] V. Ciancia, D. Latella, M. Loreti, and M. Massink. Specifying and Verifying Properties of Space. In Springer, editor, The 8th IFIP International Conference on Theoretical Computer Science, TCS 2014, Track B, volume 8705 of Lecture Notes in Computer Science, pages 222{235, 2014.
[CLLM14b] Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Specifying and verifying properties of space. Technical Report TR-QC-06-2014, QUANTICOL, 2014.
[CLLM16] Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Spatial logic and spatial model checking for closure spaces. In Marco Bernardo, Rocco De Nicola, and Jane Hillston, editors, 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, volume 9700 of Lecture Notes in Computer Science, pages 156{201. Springer, 2016.
[CLM+16] Vincenzo Ciancia, Diego Latella, Mieke Massink, Rytis Paskauskas, and Andrea Vandin. A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In Tiziana Margaria and Bernhard Ste en, editors, 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 5-14, 2016, Proceedings, volume 9952 of Lecture Notes in Computer Science. Springer, 2016.
[CLMP15] Vincenzo Ciancia, Diego Latella, Mieke Massink, and Rytis Pakauskas. 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, pages 74{79. IEEE Computer Society, 2015.
[CM10] Vincenzo Ciancia and Ugo Montanari. Symmetries, local names and dynamic (de)-allocation of names. Inf. Comput., 208(12):1349 { 1367, 2010.
[DBVZ95] Alberto Del Bimbo, Enrico Vicario, and Daniele Zingoni. Symbolic description and visual querying of image sequences using spatio-temporal logic. IEEE Trans. Knowl. Data Eng., 7(4):609{622, 1995.
[DFP98] Rocco De Nicola, Gian Luigi Ferrari, and Rosario Pugliese. Klaim: A kernel language for agents interaction and mobility. IEEE Trans. Software Eng., 24(5):315{330, 1998.
[FS06] Marcelo P. Fiore and Sam Staton. Comparing operational models of name-passing process calculi. Inf. Comput., 204(4):524{560, 2006.
[Gal99] Antony Galton. The mereotopology of discrete space. In Christian Freksa and DavidM. Mark, editors, Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science, volume 1661 of Lecture Notes in Computer Science, pages 251{266. Springer Berlin Heidelberg, 1999.
[Gal03] Antony Galton. A generalized topological view of motion in discrete space. Theoretical Computer Science, 305(1{3):111 { 134, 2003.
[Gal14] Antony Galton. Discrete mereotopology. In Claudio Calosi and Pierluigi Graziani, editors, Mereology and the Sciences, pages 293{321. Springer International Publishing, 2014.
[GBB14] Ebru Aydin Gol, Ezio Bartocci, and Calin Belta. A formal methods approach to pattern synthesis in reaction di usion systems. In 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014, pages 108{113. IEEE, 2014.
[GBC+08] R. Grosu, E. Bartocci, F. Corradini, E. Entcheva, S. A. Smolka, and A. Wasilewska. Learning and detecting emergent behavior in networks of cardiac myocytes. In Proc. of HSCC 2008, the 11th ACM international conference on Hybrid Systems: Computation and Control, 2008.
[GC11] Murdoch James Gabbay and Vincenzo Ciancia. Freshness and name-restriction in sets of traces with names. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrucken, Germany, March 26-April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 365{380. Springer, 2011.
[GL07] Fabio Gadducci and Alberto Lluch-Lafuente. Graphical encoding of a spatial logic for the pi -calculus. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 of Lecture Notes in Computer Science, pages 209{225. Springer, 2007.
[Gra09] Marco Grandis. Directed algebraic topology : models of non-reversible worlds. Cambridge University Press, Cambridge, 2009.
[GSC+09] Radu Grosu, Scott A. Smolka, Flavio Corradini, Anita Wasilewska, Emilia Entcheva, and Ezio Bartocci. Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM, 52(3):97{105, March 2009.
[HJK+15] I. Haghighi, A. Jones, J. Z. Kong, E. Bartocci, Grosu R., and C. Belta. SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems. In Proc. of HSCC, 2015.
[JEU08] Mathias John, Roland Ewald, and Adelinde M. Uhrmacher. A spatial extension to the pi calculus. Electr. Notes Theor. Comput. Sci., 194(3):133{148, 2008.
[KKWZ07] Roman Kontchakov, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. Spatial logic + temporal logic = ? In Aiello et al. [APHvB07], pages 497{564.
[KM07] Philip Kremer and Grigori Mints. Dynamic topological logic. In Aiello et al. [APHvB07], pages 565{606.
[Kov08] V. A. Kovalevsky. Geometry of Locally Finite Spaces: Computer Agreeable Topology and Algorithms for Computer Imagery. Editing House Dr. Baerbel Kovalevski, 2008.
[KPWZ10] Roman Kontchakov, Ian Pratt-Hartmann, Frank Wolter, and Michael Zakharyaschev. Spatial logics with connectedness predicates. Logical Methods in Computer Science, 6(3), 2010.
[KR89] T. Yung Kong and Azriel Rosenfeld. Digital topology: Introduction and survey. Computer Vision, Graphics, and Image Processing, 48(3):357{393, 1989.
[KST12] Alexander Kurz, Tomoyuki Suzuki, and Emilio Tuosto. On nominal regular languages with binders. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7213 of Lecture Notes in Computer Science, pages 255{269. Springer, 2012.
[Mil09] Robin Milner. The Space and Motion of Communicating Agents. Cambridge University Press, 2009.
[NB14] Laura Nenzi and Luca Bortolussi. Specifying and monitoring properties of stochastic spatiotemporal systems in signal temporal logic. In Moshe Haviv, William J. Knottenbelt, Lorenzo Maggi, and Daniele Miorandi, editors, 8th International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2014, Bratislava, Slovakia, December 9-11, 2014. ICST, 2014.
[NBC+15] Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, and Mieke Massink. Qualitative and quantitative monitoring of spatio-temporal properties. In Ezio Bartocci and Rupak Majumdar, editors, Runtime Veri cation - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings, volume 9333 of Lecture Notes in Computer Science, pages 21{37. Springer, 2015.
[Ros79] Azriel Rosenfeld. Digital topology. The American Mathematical Monthly, 86(8):621{630, 1979.
[RS85] John Reif and A.P. Sistla. A multiprocess network logic with temporal and spatial modalities. Journal of Computer and System Sciences, 30(1):41 { 53, 1985.
[Sla09] Josef Slapal. Another approach to connectedness with respect to a closure operator. Applied Categorical Structures, 17(6):603{612, 2009.
[SW07] Michael B. Smyth and Julian Webster. Discrete spatial models. In Springer [APHvB07], pages 713{798.
[Tar72] Robert Tarjan. Depth rst search and linear graph algorithms. SIAM Journal on Computing, 1972.
[TPGN15] Christos Tsigkanos, Liliana Pasquale, Carlo Ghezzi, and Bashar Nuseibeh. Ariadne: Topology aware adaptive security for cyber-physical systems. In 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Volume 2, pages 729{732. IEEE, 2015.
[APHvB07] Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors. Handbook of Spatial Logics. Springer, 2007.
[AS15] Francesco Luca De Angelis and Giovanna Di Marzo Serugendo. A logic language for run time assessment of spatial properties in self-organizing systems. In 2015 IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASO Workshops 2015, Cambridge, MA, USA, September 21-25, 2015, pages 86{91. IEEE Computer Society, 2015.
[BB07] Johan van Benthem and Guram Bezhanishvili. Modal logics of space. In Aiello et al. [APHvB07], pages 217{298.
[BCLM16] Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. From collective adaptive systems to human centric computation and back: Spatial model checking for medical imaging. In Maurice H. ter Beek and Michele Loreti, editors, Proceedings of the Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, FORECAST@STAF 2016, Vienna, Austria, 8 July 2016., volume 217 of EPTCS, pages 81{92, 2016.
[BHLM13] Luca Bortolussi, Jane Hillston, Diego Latella, and Mieke Massink. Continuous approximation of collective system behaviour: A tutorial. Performance Evaluation, 70(5):317 { 349, 2013.
[BHMU11] Arne T. Bittig, Fiete Haack, Carsten Maus, and Adelinde M. Uhrmacher. Adapting rule-based model descriptions for simulating in continuous and hybrid space. In Francois Fages, editor, Computational Methods in Systems Biology, 9th International Conference, CMSB 2011, Paris, France, September 21-23, 2011. Proceedings, pages 161{170. ACM, 2011.
[BK08] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
[BKL11] Mikolaj Bojanczyk, Bartek Klin, and Slawomir Lasota. Automata with group actions. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 355{364. IEEE Computer Society, 2011.
[CC03] L. Caires and L. Cardelli. A spatial logic for concurrency (part I). Information and Computation, 186(2):194{235, 2003.
[CE82] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Dexter Kozen, editor, Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52{71. Springer Berlin Heidelberg, 1982.
[CG00] Luca Cardelli and Andrew D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), pages 365{377, 2000.
[CG12] Luca Cardelli and Philippa Gardner. Processes in space. Theor. Comput. Sci., 431:40{55, 2012.
[CGG02] Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. A spatial logic for querying graphs. In Peter Widmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew Hennessy, Stephan Eidenbenz, and Ricardo Conejo, editors, Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings, volume 2380 of Lecture Notes in Computer Science, pages 597{610. Springer, 2002.
[CGL+14] Vincenzo Ciancia, Stephen Gilmore, Diego Latella, Michele Loreti, and Mieke Massink. Data veri cation for collective adaptive systems: Spatial model-checking of vehicle location data. In Eighth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW 2014, London, United Kingdom, September 8-12, 2014, pages 32{37. IEEE Computer Society, 2014.
[CGL+15] Vincenzo Ciancia, Gianluca Grilletti, Diego Latella, Michele Loreti, and Mieke Massink. 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, volume 9509 of Lecture Notes in Computer Science, pages 297{311. Springer, 2015.
[CLBR09] Augustin Chaintreau, Jean-Yves Le Boudec, and Nikodin Ristanovic. The age of gossip: Spatial mean eld regime. In Proceedings of the Eleventh International Joint Conference on Measurement and Modeling of Computer Systems, SIGMETRICS '09, pages 109{120, New York, NY, USA, 2009. ACM.
[CLLM14a] V. Ciancia, D. Latella, M. Loreti, and M. Massink. Specifying and Verifying Properties of Space. In Springer, editor, The 8th IFIP International Conference on Theoretical Computer Science, TCS 2014, Track B, volume 8705 of Lecture Notes in Computer Science, pages 222{235, 2014.
[CLLM14b] Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Specifying and verifying properties of space. Technical Report TR-QC-06-2014, QUANTICOL, 2014.
[CLLM16] Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Spatial logic and spatial model checking for closure spaces. In Marco Bernardo, Rocco De Nicola, and Jane Hillston, editors, 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, volume 9700 of Lecture Notes in Computer Science, pages 156{201. Springer, 2016.
[CLM+16] Vincenzo Ciancia, Diego Latella, Mieke Massink, Rytis Paskauskas, and Andrea Vandin. A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In Tiziana Margaria and Bernhard Ste en, editors, 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 5-14, 2016, Proceedings, volume 9952 of Lecture Notes in Computer Science. Springer, 2016.
[CLMP15] Vincenzo Ciancia, Diego Latella, Mieke Massink, and Rytis Pakauskas. 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, pages 74{79. IEEE Computer Society, 2015.
[CM10] Vincenzo Ciancia and Ugo Montanari. Symmetries, local names and dynamic (de)-allocation of names. Inf. Comput., 208(12):1349 { 1367, 2010.
[DBVZ95] Alberto Del Bimbo, Enrico Vicario, and Daniele Zingoni. Symbolic description and visual querying of image sequences using spatio-temporal logic. IEEE Trans. Knowl. Data Eng., 7(4):609{622, 1995.
[DFP98] Rocco De Nicola, Gian Luigi Ferrari, and Rosario Pugliese. Klaim: A kernel language for agents interaction and mobility. IEEE Trans. Software Eng., 24(5):315{330, 1998.
[FS06] Marcelo P. Fiore and Sam Staton. Comparing operational models of name-passing process calculi. Inf. Comput., 204(4):524{560, 2006.
[Gal99] Antony Galton. The mereotopology of discrete space. In Christian Freksa and DavidM. Mark, editors, Spatial Information Theory. Cognitive and Computational Foundations of Geographic Information Science, volume 1661 of Lecture Notes in Computer Science, pages 251{266. Springer Berlin Heidelberg, 1999.
[Gal03] Antony Galton. A generalized topological view of motion in discrete space. Theoretical Computer Science, 305(1{3):111 { 134, 2003.
[Gal14] Antony Galton. Discrete mereotopology. In Claudio Calosi and Pierluigi Graziani, editors, Mereology and the Sciences, pages 293{321. Springer International Publishing, 2014.
[GBB14] Ebru Aydin Gol, Ezio Bartocci, and Calin Belta. A formal methods approach to pattern synthesis in reaction di usion systems. In 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014, pages 108{113. IEEE, 2014.
[GBC+08] R. Grosu, E. Bartocci, F. Corradini, E. Entcheva, S. A. Smolka, and A. Wasilewska. Learning and detecting emergent behavior in networks of cardiac myocytes. In Proc. of HSCC 2008, the 11th ACM international conference on Hybrid Systems: Computation and Control, 2008.
[GC11] Murdoch James Gabbay and Vincenzo Ciancia. Freshness and name-restriction in sets of traces with names. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrucken, Germany, March 26-April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 365{380. Springer, 2011.
[GL07] Fabio Gadducci and Alberto Lluch-Lafuente. Graphical encoding of a spatial logic for the pi -calculus. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 of Lecture Notes in Computer Science, pages 209{225. Springer, 2007.
[Gra09] Marco Grandis. Directed algebraic topology : models of non-reversible worlds. Cambridge University Press, Cambridge, 2009.
[GSC+09] Radu Grosu, Scott A. Smolka, Flavio Corradini, Anita Wasilewska, Emilia Entcheva, and Ezio Bartocci. Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM, 52(3):97{105, March 2009.
[HJK+15] I. Haghighi, A. Jones, J. Z. Kong, E. Bartocci, Grosu R., and C. Belta. SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems. In Proc. of HSCC, 2015.
[JEU08] Mathias John, Roland Ewald, and Adelinde M. Uhrmacher. A spatial extension to the pi calculus. Electr. Notes Theor. Comput. Sci., 194(3):133{148, 2008.
[KKWZ07] Roman Kontchakov, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. Spatial logic + temporal logic = ? In Aiello et al. [APHvB07], pages 497{564.
[KM07] Philip Kremer and Grigori Mints. Dynamic topological logic. In Aiello et al. [APHvB07], pages 565{606.
[Kov08] V. A. Kovalevsky. Geometry of Locally Finite Spaces: Computer Agreeable Topology and Algorithms for Computer Imagery. Editing House Dr. Baerbel Kovalevski, 2008.
[KPWZ10] Roman Kontchakov, Ian Pratt-Hartmann, Frank Wolter, and Michael Zakharyaschev. Spatial logics with connectedness predicates. Logical Methods in Computer Science, 6(3), 2010.
[KR89] T. Yung Kong and Azriel Rosenfeld. Digital topology: Introduction and survey. Computer Vision, Graphics, and Image Processing, 48(3):357{393, 1989.
[KST12] Alexander Kurz, Tomoyuki Suzuki, and Emilio Tuosto. On nominal regular languages with binders. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7213 of Lecture Notes in Computer Science, pages 255{269. Springer, 2012.
[Mil09] Robin Milner. The Space and Motion of Communicating Agents. Cambridge University Press, 2009.
[NB14] Laura Nenzi and Luca Bortolussi. Specifying and monitoring properties of stochastic spatiotemporal systems in signal temporal logic. In Moshe Haviv, William J. Knottenbelt, Lorenzo Maggi, and Daniele Miorandi, editors, 8th International Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS 2014, Bratislava, Slovakia, December 9-11, 2014. ICST, 2014.
[NBC+15] Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, and Mieke Massink. Qualitative and quantitative monitoring of spatio-temporal properties. In Ezio Bartocci and Rupak Majumdar, editors, Runtime Veri cation - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings, volume 9333 of Lecture Notes in Computer Science, pages 21{37. Springer, 2015.
[Ros79] Azriel Rosenfeld. Digital topology. The American Mathematical Monthly, 86(8):621{630, 1979.
[RS85] John Reif and A.P. Sistla. A multiprocess network logic with temporal and spatial modalities. Journal of Computer and System Sciences, 30(1):41 { 53, 1985.
[Sla09] Josef Slapal. Another approach to connectedness with respect to a closure operator. Applied Categorical Structures, 17(6):603{612, 2009.
[SW07] Michael B. Smyth and Julian Webster. Discrete spatial models. In Springer [APHvB07], pages 713{798.
[Tar72] Robert Tarjan. Depth rst search and linear graph algorithms. SIAM Journal on Computing, 1972.
[TPGN15] Christos Tsigkanos, Liliana Pasquale, Carlo Ghezzi, and Bashar Nuseibeh. Ariadne: Topology aware adaptive security for cyber-physical systems. In 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Volume 2, pages 729{732. IEEE, 2015.
Metrics
Back to previous page
BibTeX entry
@article{oai:it.cnr:prodotti:359518,
title = {Model checking spatial logics for closure spaces},
author = {Ciancia V. and Latella D. and Loreti M. and Massink M.},
publisher = {Technische Universität Braunschweig, Institute of Theoretical Computer Science, Braunschweig, Germany, Germania},
doi = {10.2168/lmcs-12(4:2)2016 and 10.48550/arxiv.1609.06513},
journal = {Logical Methods in Computer Science},
volume = {12},
pages = {1–51},
year = {2016}
}
0000-0003-1314-0574
