×

A logic for monitoring dynamic networks of spatially-distributed cyber-physical systems. (English) Zbl 07471693

Summary: Cyber-Physical Systems (CPS) consist of inter-wined computational (cyber) and physical components interacting through sensors and/or actuators. Computational elements are networked at every scale and can communicate with each other and with humans. Nodes can join and leave the network at any time or they can move to different spatial locations. In this scenario, monitoring spatial and temporal properties plays a key role in the understanding of how complex behaviors can emerge from local and dynamic interactions. We revisit here the Spatio-Temporal Reach and Escape Logic (STREL), a logic-based formal language designed to express and monitor spatio-temporal requirements over the execution of mobile and spatially distributed CPS. STREL considers the physical space in which CPS entities (nodes of the graph) are arranged as a weighted graph representing their dynamic topological configuration. Both nodes and edges include attributes modeling physical and logical quantities that can evolve over time. STREL combines the Signal Temporal Logic with two spatial modalities reach and escape that operate over the weighted graph. From these basic operators, we can derive other important spatial modalities such as everywhere, somewhere and surround. We propose both qualitative and quantitative semantics based on constraint semiring algebraic structure. We provide an offline monitoring algorithm for STREL and we show the feasibility of our approach with the application to two case studies: monitoring spatio-temporal requirements over a simulated mobile ad-hoc sensor network and a simulated epidemic spreading model for COVID19.

MSC:

03B70 Logic in computer science
68-XX Computer science

Software:

NetworkX

References:

[1] Eugene Asarin, Paul Caspi, and Oded Maler. Timed regular expressions.J. ACM, 49(2):172- 206, 2002.doi:10.1145/506147.506151. · Zbl 1323.68335
[2] Ebru Aydin-Gol, Ezio Bartocci, and Calin Belta. A formal methods approach to pattern synthesis in reaction diffusion systems. InProc. of CDC 2014: the 53rd IEEE Conference on · Zbl 1507.92031
[3] Suhail Alsalehi, Noushin Mehdipour, Ezio Bartocci, and Calin Belta. Neural network-based control for multi-agent systems from spatio-temporal specifications. InProc. of CDC 2021:
[4] Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors.Handbook of Spatial Logics. Springer, Dordrecht, Niederlande, 2007.doi:10.1007/978-1-4020-5587-4. · Zbl 1172.03001
[5] Franz Aurenhammer. Voronoi diagrams—a survey of a fundamental geometric data structure.ACM Comput. Surv., 23(3):345-405, 1991.doi:10.1145/116873.116880.
[6] Ezio Bartocci, Ebru Aydin-Gol, Iman Haghighi, and Calin Belta. A formal methods approach to pattern recognition and synthesis in reaction diffusion networks.IEEE Transactions on · Zbl 1507.92031
[7] Ezio Bartocci, Luca Bortolussi, Michele Loreti, and Laura Nenzi. Monitoring mobile and spatially distributed cyber-physical systems. InProc. of MEMOCODE 2017: the 15th ACM
[8] Fred Brauer, Carlos Castillo-Chavez, and Zhilan Feng.Mathematical Models in Epidemiology, volume 69 ofTexts in Applied Mathematics. Springer New York, New York, · Zbl 1433.92001
[9] Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. Voxlogica: A spatial model checker for declarative image analysis. InProc. of TACAS 2019: the 25th International · Zbl 1461.68113
[10] Stefano Bistarelli, Ugo Montanari, and Francesca Rossi. Semiring-based constraint satisfaction and optimization.J. ACM, 44(2):201-236, 1997. URL:http://doi.acm.org/10.1145/256303. 256306,doi:10.1145/256303.256306. · Zbl 0890.68032
[11] Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Specifying and verifying properties of space. InProc. of TCS 2014: the 8th IFIP TC 1/WG 2.2 International Conference · Zbl 1417.68101
[12] Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Spatial logic and spatial model checking for closure spaces. InProc. of SFM 2016, volume 9700 ofLNCS, pages 156-201, Bertinoro, Italy, 2016. Springer.doi:10.1007/978-3-319-34096-8_6. · Zbl 1346.68122
[13] Boris Delaunay. Sur la sph‘ere vide. a la m´emoire de georges vorono¨ı.Bulletin de l’Acad´emie des Sciences de l’URSS, 6:793-800, 1934. · Zbl 0010.41101
[14] Alexandre Donz´e, Thomas Ferr‘ere, and Oded Maler. Efficient robust monitoring for STL. InProc. of CAV 2013: the 25th International Conference on Computer Aided Verification, volume 8044 ofLNCS, pages 264-279, Saint Petersburg, Russia, 2013. Springer.doi:10.1007/ 978-3-642-39799-8_19.
[15] E. Allen Emerson and Joseph Y. Halpern. “sometimes” and “not never” revisited: On branching versus linear time. In John R. Wright, Larry Landweber, Alan J. Demers, and Tim Teitelbaum, editors,Proc. of POPL 83: the Tenth Annual ACM Symposium on Principles of Programming · Zbl 0629.68020
[16] Raphael A. Finkel and Jon Louis Bentley. Quad trees: A data structure for retrieval on composite keys.Acta Informatica, 4:1-9, 1974.doi:10.1007/BF00288933. · Zbl 0278.68030
[17] Antony Galton. The mereotopology of discrete space. In Christian Freksa and DavidM. Mark, editors,Proc. of COSIT ’99: the International Conference on Spatial Information Theory: · Zbl 1436.03166
[18] Aric A. Hagberg, Daniel A. Schult, and Pieter J. Swart. Exploring network structure, dynamics, and function using networkx. In Ga¨el Varoquaux, Travis Vaught, and Jarrod Millman, editors,
[19] Stefan Jaksic, Ezio Bartocci, Radu Grosu, and Dejan Nickovic. An algebraic framework for runtime verification.IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 37(11):2233-2243, 2018.doi:10.1109/TCAD.2018.2858460.
[20] Alberto Lluch-Lafuente and Ugo Montanari. Quantitative mu-calculus and CTL defined over constraint semirings.Theor. Comput. Sci., 346(1):135-160, 2005. URL:http://dx.doi.org/ 10.1016/j.tcs.2005.08.006,doi:10.1016/j.tcs.2005.08.006. · Zbl 1080.68065
[21] J. O. Lloyd-Smith, S. J. Schreiber, P. E. Kopp, and W. M. Getz. Superspreading and the effect of individual variation on disease emergence.Nature, 438(7066):355-359, November 2005. Number: 7066 Publisher: Nature Publishing Group. URL:https://www.nature.com/ articles/nature04153,doi:10.1038/nature04153.
[22] Oded Maler. Some thoughts on runtime verification. InProc. of RV 2016: the 16th International Conference on Runtime Verification, volume 10012 ofLNCS, pages 3-14. Springer, 2016.
[23] Sara Mohammadinejad, Jyotirmoy V. Deshmukh, and Laura Nenzi. Mining interpretable spatio-temporal logic properties for spatially distributed systems. InProc. of ATVA 2021: · Zbl 1497.68433
[24] Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In Proc. of FORMATS/FTRTFT 2004: the Joint International Conferences on Formal Modelling and Analysis of Timed Systems and on Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 3253 ofLNCS, pages 152-166, Grenoble, France, 2004. Springer.doi: · Zbl 1109.68518
[25] Oded Maler and Dejan Nickovic. Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Transf., 15(3):247-268, 2013.doi:10.1007/s10009-012-0247-9. · Zbl 1109.68518
[26] Romualdo Pastor-Satorras, Claudio Castellano, Piet Van Mieghem, and Alessandro Vespignani. Epidemic processes in complex networks.Reviews of Modern Physics, 87(3):925-979, August 2015. arXiv: 1408.2701. URL:http://arxiv.org/abs/1408.2701,doi:10.1103/RevModPhys. 87.925.
[27] Ennio Visconti, Ezio Bartocci, Michele Loreti, and Laura Nenzi. Online monitoring of spatiotemporal properties for imprecise signals. InProc. of MEMOCODE 2021: the 19th ACM-IEEE
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.