{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T07:46:02Z","timestamp":1766043962454,"version":"3.48.0"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032054340"},{"type":"electronic","value":"9783032054357"}],"license":[{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-05435-7_26","type":"book-chapter","created":{"date-parts":[[2025,9,13]],"date-time":"2025-09-13T01:30:55Z","timestamp":1757727055000},"page":"477-496","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["ISL: Monitoring Image Segmentation Logic in\u00a0Medical Imaging Analysis"],"prefix":"10.1007","author":[{"given":"Ziyan","family":"An","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Moyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ipek","family":"Oguz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meiyi","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,12]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"An, Z., Johnson, T.T., Ma, M.: Formal logic enabled personalized federated learning through property inference. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol.\u00a038, pp. 10882\u201310890 (2024)","DOI":"10.1609\/aaai.v38i10.28962"},{"key":"26_CR2","unstructured":"An, Z., et al.: Combining LLMs with a logic-based framework to explain MCTS. In: Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems, pp. 2405\u20132407. AAMAS \u201925, International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC (2025)"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"An, Z., Wang, X., T.\u00a0Johnson, T., Sprinkle, J., Ma, M.: Runtime monitoring of accidents in driving recordings with multi-type logic in empirical models. In: International Conference on Runtime Verification, pp. 376\u2013388. Springer (2023)","DOI":"10.1007\/978-3-031-44267-4_21"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Bennett, B.: Spatial reasoning with propositional logics. In: Principles of Knowledge Representation and Reasoning, pp. 51\u201362. Elsevier (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50102-0"},{"key":"26_CR5","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1020083231504","volume":"17","author":"B Bennett","year":"2002","unstructured":"Bennett, B., Cohn, A.G., Wolter, F., Zakharyaschev, M.: Multi-dimensional modal logic as a framework for Spatio-temporal reasoning. Appl. Intell. 17, 239\u2013251 (2002)","journal-title":"Appl. Intell."},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Berger, A.H., et al.: Topologically faithful multi-class segmentation in medical images. In: International Conference on Medical Image Computing and Computer-Assisted Intervention, pp. 721\u2013731. Springer (2024)","DOI":"10.1007\/978-3-031-72111-3_68"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Bresolin, D., Sala, P., Della\u00a0Monica, D., Montanari, A., Sciavicco, G.: A decidable spatial generalization of metric interval temporal logic. In: 2010 17th International Symposium on Temporal Representation and Reasoning, pp. 95\u2013102. IEEE (2010)","DOI":"10.1109\/TIME.2010.22"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Chang, K.K.C., Xu, K., Kim, E., Sangiovanni-Vincentelli, A., Seshia, S.A.: Dynamic, multi-objective specification and falsification of autonomous CPS. In: International Conference on Runtime Verification, pp. 40\u201358. Springer (2024)","DOI":"10.1007\/978-3-031-74234-7_3"},{"key":"26_CR9","unstructured":"Chaudhry, R., Omole, A.E., Bordoni, B.: Anatomy, thorax, lungs. In: StatPearls [Internet]. StatPearls Publishing (2024)"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Chen, Z., An, Z., Reynolds, J., Mullen, K., Martini, S., Ma, M.: LogiDebrief: a signal-temporal logic based automated debriefing approach with large language models integration. arXiv preprint arXiv:2505.03985 (2025)","DOI":"10.24963\/ijcai.2025\/1065"},{"issue":"3","key":"26_CR11","doi-asserted-by":"publisher","first-page":"297","DOI":"10.2307\/1932409","volume":"26","author":"LR Dice","year":"1945","unstructured":"Dice, L.R.: Measures of the amount of ecologic association between species. Ecology 26(3), 297\u2013302 (1945). https:\/\/doi.org\/10.2307\/1932409","journal-title":"Ecology"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Dokhanchi, A., Amor, H.B., Deshmukh, J.V., Fainekos, G.: Evaluating perception systems for autonomous vehicles using quality temporal logic. In: Runtime Verification: 18th International Conference, RV 2018, Limassol, Cyprus, November 10\u201313, 2018, Proceedings 18, pp. 409\u2013416. Springer (2018)","DOI":"10.1007\/978-3-030-03769-7_23"},{"key":"26_CR13","unstructured":"European Union: Artificial intelligence act \u2013 article 15: Accuracy, robustness and cybersecurity. https:\/\/artificialintelligenceact.eu\/article\/15\/ (2024). Accessed 05 May 2025"},{"issue":"1","key":"26_CR14","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1038\/s41597-024-03358-1","volume":"11","author":"N Gaggion","year":"2024","unstructured":"Gaggion, N., et al.: CheXmask: a large-scale dataset of anatomical segmentation masks for multi-center chest X-ray images. Sci. Data 11(1), 511 (2024)","journal-title":"Sci. Data"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Gaggion, N., Mansilla, L., Mosquera, C., Milone, D.H., Ferrante, E.: Improving anatomical plausibility in medical image segmentation via hybrid graph neural networks: Applications to chest x-ray analysis. IEEE Transactions on Medical Imaging (2022)","DOI":"10.1109\/TMI.2022.3224660"},{"key":"26_CR16","unstructured":"Gal, Y., Ghahramani, Z.: Dropout as a Bayesian approximation: Representing model uncertainty in deep learning. International Conference on Machine Learning (ICML) (2016)"},{"issue":"10","key":"26_CR17","doi-asserted-by":"publisher","DOI":"10.1118\/1.4894817","volume":"41","author":"G Gill","year":"2014","unstructured":"Gill, G., Bauer, C., Beichel, R.R.: A method for avoiding overlap of left and right lungs in shape model guided segmentation of lungs in CT volumes. Med. Phys. 41(10), 101908 (2014)","journal-title":"Med. Phys."},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: 53rd IEEE Conference on Decision and Control, pp. 108\u2013113. IEEE (2014)","DOI":"10.1109\/CDC.2014.7039367"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Gros, R., Belta, C.: Spatel: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 189\u2013198 (2015)","DOI":"10.1145\/2728606.2728633"},{"issue":"12","key":"26_CR20","doi-asserted-by":"publisher","first-page":"3969","DOI":"10.1109\/TMI.2022.3202183","volume":"41","author":"J Hao","year":"2022","unstructured":"Hao, J., et al.: Retinal structure detection in octa image via voting-based multitask learning. IEEE Trans. Med. Imaging 41(12), 3969\u20133980 (2022)","journal-title":"IEEE Trans. Med. Imaging"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"He, W., Wu, C., Bensalem, S.: Box-based monitor approach for out-of-distribution detection in YOLO: an exploratory study. In: International Conference on Runtime Verification, pp. 229\u2013239. Springer (2024)","DOI":"10.1007\/978-3-031-74234-7_15"},{"issue":"2","key":"26_CR22","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1177\/02783649231223546","volume":"43","author":"M Hekmatnejad","year":"2024","unstructured":"Hekmatnejad, M., Hoxha, B., Deshmukh, J.V., Yang, Y., Fainekos, G.: Formalizing and evaluating requirements of perception systems for automated vehicles using spatio-temporal perception logic. Int. J. Robot. Res. 43(2), 203\u2013238 (2024)","journal-title":"Int. J. Robot. Res."},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Irvin, J., et\u00a0al.: CheXpert: a large chest radiograph dataset with uncertainty labels and expert comparison. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol.\u00a033, pp. 590\u2013597 (2019)","DOI":"10.1609\/aaai.v33i01.3301590"},{"key":"26_CR24","first-page":"547","volume":"37","author":"P Jaccard","year":"1901","unstructured":"Jaccard, P.: \u00c9tude comparative de la distribution florale dans une portion des alpes et des jura. Bull Soc Vaudoise Sci Nat 37, 547\u2013579 (1901)","journal-title":"Bull Soc Vaudoise Sci Nat"},{"key":"26_CR25","unstructured":"Kendall, A., Gal, Y.: What uncertainties do we need in Bayesian deep learning for computer vision? Adv. Neural Inf. Process. Syst. (NeurIPS) 30 (2017)"},{"key":"26_CR26","unstructured":"Kingma, D.P.: Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014)"},{"key":"26_CR27","doi-asserted-by":"publisher","DOI":"10.1016\/j.media.2024.103092","volume":"93","author":"M Li","year":"2024","unstructured":"Li, M., et al.: OCTA-500: a retinal dataset for optical coherence tomography angiography study. Med. Image Anal. 93, 103092 (2024)","journal-title":"Med. Image Anal."},{"key":"26_CR28","doi-asserted-by":"publisher","unstructured":"Li, M., Huang, K., Xu, Q., Yang, J., Zhang, Y., Yang, J.: OCTA-500: a novel dataset for retinal optical coherence tomography angiography analysis. Med. Image Anal. 91, 103092 (2024). https:\/\/doi.org\/10.1016\/j.media.2024.103092, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1361841524000173","DOI":"10.1016\/j.media.2024.103092"},{"key":"26_CR29","doi-asserted-by":"crossref","unstructured":"Li, T., et al.: STSL: a novel spatio-temporal specification language for cyber-physical systems. In: 2020 IEEE 20th International Conference on Software Quality, Reliability and Security (QRS), pp. 309\u2013319. IEEE (2020)","DOI":"10.1109\/QRS51102.2020.00048"},{"issue":"1","key":"26_CR30","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1186\/s41747-024-00508-3","volume":"8","author":"J Lim","year":"2024","unstructured":"Lim, J., Abily, A., Ben Salem, D., Gaillandre, L., Attye, A., Ognard, J.: Training and validation of a deep learning u-net architecture general model for automated segmentation of inner ear from ct. Eur. Radiol. Exp. 8(1), 104 (2024)","journal-title":"Eur. Radiol. Exp."},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"Ma, M., Bartocci, E., Lifland, E., Stankovic, J., Feng, L.: SaSTL: spatial aggregation signal temporal logic for runtime monitoring in smart cities. In: 2020 ACM\/IEEE 11th International Conference on Cyber-Physical Systems (ICCPS), pp. 51\u201362. IEEE (2020)","DOI":"10.1109\/ICCPS48487.2020.00013"},{"key":"26_CR32","first-page":"14604","volume":"33","author":"M Ma","year":"2020","unstructured":"Ma, M., Gao, J., Feng, L., Stankovic, J.: STLnet: signal temporal logic enforced multivariate recurrent neural networks. Adv. Neural. Inf. Process. Syst. 33, 14604\u201314614 (2020)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"26_CR33","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 152\u2013166. Springer (2004)","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"26_CR34","doi-asserted-by":"crossref","unstructured":"Moon, N., Bullitt, E., Van\u00a0Leemput, K., Gerig, G.: Automatic brain and tumor segmentation. In: Medical Image Computing and Computer-Assisted Intervention\u2014MICCAI 2002: 5th International Conference Tokyo, Japan, September 25\u201328, 2002 Proceedings, Part I 5, pp. 372\u2013379. Springer (2002)","DOI":"10.1007\/3-540-45786-0_46"},{"key":"26_CR35","doi-asserted-by":"publisher","DOI":"10.1016\/j.media.2019.101557","volume":"59","author":"T Nair","year":"2020","unstructured":"Nair, T., Precup, D., Arbel, T.: Exploring uncertainty measures in deep networks for multiple sclerosis lesion detection and segmentation. Med. Image Anal. 59, 101557 (2020)","journal-title":"Med. Image Anal."},{"key":"26_CR36","unstructured":"Panara, K., Hoffer, M.: Anatomy, head and neck, ear internal auditory canal (internal auditory meatus, internal acoustic canal) (2019)"},{"key":"26_CR37","unstructured":"Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. KR 92, 165\u2013176 (1992)"},{"key":"26_CR38","doi-asserted-by":"crossref","unstructured":"Ronneberger, O., Fischer, P., Brox, T.: U-Net: convolutional networks for biomedical image segmentation. In: MICCAI 2015: 18th International Conference, Munich, Germany, October 5-9, 2015, proceedings, part III 18, pp. 234\u2013241. Springer (2015)","DOI":"10.1007\/978-3-319-24574-4_28"},{"key":"26_CR39","doi-asserted-by":"publisher","first-page":"82031","DOI":"10.1109\/ACCESS.2021.3086020","volume":"9","author":"N Siddique","year":"2021","unstructured":"Siddique, N., Paheding, S., Elkin, C.P., Devabhaktuni, V.: U-net and its variants for medical image segmentation: a review of theory and applications. IEEE Access 9, 82031\u201382057 (2021)","journal-title":"IEEE Access"},{"issue":"11","key":"26_CR40","doi-asserted-by":"publisher","first-page":"4970","DOI":"10.1002\/mp.13773","volume":"46","author":"AM Sousa","year":"2019","unstructured":"Sousa, A.M., et al.: ALTIS: a fast and automatic lung and trachea CT-image segmentation method. Med. Phys. 46(11), 4970\u20134982 (2019)","journal-title":"Med. Phys."},{"key":"26_CR41","unstructured":"Stucki, N., Paetzold, J.C., Shit, S., Menze, B., Bauer, U.: Topologically faithful image segmentation via induced matching of persistence barcodes. In: International Conference on Machine Learning, pp. 32698\u201332727. PMLR (2023)"},{"key":"26_CR42","doi-asserted-by":"crossref","unstructured":"Toledo, F., Woodlief, T., Elbaum, S., Dwyer, M.B.: Specifying and monitoring safe driving properties with scene graphs. In: 2024 IEEE International Conference on Robotics and Automation (ICRA), pp. 15577\u201315584. IEEE (2024)","DOI":"10.1109\/ICRA57147.2024.10610973"},{"key":"26_CR43","doi-asserted-by":"crossref","unstructured":"Tran, H.D., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: International Conference on Computer Aided Verification, pp. 3\u201317. Springer (2020)","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"26_CR44","doi-asserted-by":"crossref","unstructured":"Vuppala, S.R.H., Allen, N., Pinisetty, S., Roop, P.: A formal approach for safe reinforcement learning: a rate-adaptive pacemaker case study. In: International Conference on Runtime Verification, pp. 3\u201321. Springer (2024)","DOI":"10.1007\/978-3-031-74234-7_1"},{"issue":"5","key":"26_CR45","doi-asserted-by":"publisher","first-page":"1243","DOI":"10.1049\/ipr2.12419","volume":"16","author":"R Wang","year":"2022","unstructured":"Wang, R., et al.: Medical image segmentation using deep learning: a survey. IET Image Proc. 16(5), 1243\u20131267 (2022)","journal-title":"IET Image Proc."},{"key":"26_CR46","unstructured":"Wolter, F., Zakharyaschev, M.: Spatial representation and reasoning in RCC-8 with Boolean region terms. In: Proceedings of the 14th European Conference on Artificial Intelligence, pp. 244\u2013248. Citeseer (2000)"},{"key":"26_CR47","doi-asserted-by":"crossref","unstructured":"Woodlief, T., Toledo, F., Elbaum, S., Dwyer, M.B.: S3c: spatial semantic scene coverage for autonomous vehicles. In: Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering, pp. 1\u201313 (2024)","DOI":"10.1145\/3597503.3639178"},{"key":"26_CR48","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2024.103252","volume":"242","author":"T Woodlief","year":"2025","unstructured":"Woodlief, T., Toledo, F., Elbaum, S., Dwyer, M.B.: The SGSM framework: enabling the specification and monitor synthesis of safe driving properties through scene graphs. Sci. Comput. Program. 242, 103252 (2025)","journal-title":"Sci. Comput. Program."},{"key":"26_CR49","doi-asserted-by":"crossref","unstructured":"Zhao, L., Tohka, J., Ruotsalainen, U.: Accurate 3D left-right brain hemisphere segmentation in MR images based on shape bottlenecks and partial volume estimation. In: Image Analysis: 15th Scandinavian Conference, SCIA 2007, Aalborg, Denmark, June 10-14, 2007 15, pp. 581\u2013590. Springer (2007)","DOI":"10.1007\/978-3-540-73040-8_59"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05435-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T07:43:16Z","timestamp":1766043796000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05435-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,12]]},"ISBN":["9783032054340","9783032054357"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05435-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,9,12]]},"assertion":[{"value":"12 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Graz","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv25.isec.tugraz.at\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}