{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:16:24Z","timestamp":1742937384131,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031331695"},{"type":"electronic","value":"9783031331701"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-33170-1_11","type":"book-chapter","created":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T12:55:27Z","timestamp":1685710527000},"page":"174-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning with\u00a0Metric Temporal Logic and\u00a0Resettable Skewed Clocks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3385-3205","authenticated-orcid":false,"given":"Alberto","family":"Bombardelli","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9091-7899","authenticated-orcid":false,"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,6,3]]},"reference":[{"issue":"1","key":"11_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181\u2013204 (1994)","journal-title":"J. ACM"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Barsotti, D., Nieto, L.P., Tiu, A.: Verification of clock synchronization algorithms: experiments on a combination of deductive tools. Electron. Notes Theor. Comput. Sci. 145, 63\u201378 (2006). Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005)","DOI":"10.1016\/j.entcs.2005.10.005"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-031-06773-0_27","volume-title":"NFM 2022","author":"A Bombardelli","year":"2022","unstructured":"Bombardelli, A., Tonetta, S.: Asynchronous composition of local interface LTL properties. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, pp. 508\u2013526. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_27"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Bombardelli, A., Tonetta, S.: Metric temporal logic with resettable skewed clocks - version with proofs. In: DATE (2023, to appear). https:\/\/es-static.fbk.eu\/people\/bombardelli\/papers\/date23\/extended_abstract.pdf","DOI":"10.23919\/DATE56975.2023.10137043"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/11691372_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"GM Brown","year":"2006","unstructured":"Brown, G.M., Pike, L.: Easy parameterized verification of Biphase mark and 8N1 protocols. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 58\u201372. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_4"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-13464-7_13","volume-title":"Formal Techniques for Distributed Systems","author":"L Bu","year":"2010","unstructured":"Bu, L., Cimatti, A., Li, X., Mover, S., Tonetta, S.: Model checking of hybrid systems using shallow synchronization. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE -2010. LNCS, vol. 6117, pp. 155\u2013169. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13464-7_13"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-319-04921-2_20","volume-title":"Language and Automata Theory and Applications","author":"C Carapelle","year":"2014","unstructured":"Carapelle, C., Feng, S., Fern\u00e1ndez Gil, O., Quaas, K.: Satisfiability for MTL and TPTL over non-monotonic data words. In: Dediu, A.-H., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 248\u2013259. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-04921-2_20"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-030-25540-4_21","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2019","unstructured":"Cimatti, A., Griggio, A., Magnago, E., Roveri, M., Tonetta, S.: Extending nuXmv with timed transition systems and timed temporal properties. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 376\u2013386. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_21"},{"key":"11_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.104502","volume":"272","author":"A Cimatti","year":"2019","unstructured":"Cimatti, A., Griggio, A., Magnago, E., Roveri, M., Tonetta, S.: SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. Inf. Comput. 272, 104502 (2019)","journal-title":"Inf. Comput."},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-54862-8_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46\u201361. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_4"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-319-08867-9_28","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Verifying LTL properties of hybrid systems with K-Liveness. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 424\u2013440. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_28"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Damm, W., Hungar, H., Josko, B., Peikenkamp, T., Stierand, I.: Using contract-based component specifications for virtual integration testing and architecture design, pp. 1\u20136 (2011)","DOI":"10.1109\/DATE.2011.5763167"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2004","unstructured":"de Moura, L., et al.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496\u2013500. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_45"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Ganguly, R., et al.: Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols. CoRR, abs\/2204.09796 (2022)","DOI":"10.1109\/ICDCS54860.2022.00012"},{"issue":"4","key":"11_CR16","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-030-20652-9_2","volume-title":"NASA Formal Methods","author":"J Ortiz","year":"2019","unstructured":"Ortiz, J., Amrani, M., Schobbens, P.-Y.: $$ML_{\\nu }$$: a distributed real-time modal logic. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 19\u201335. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_2"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-22256-6_23","volume-title":"Implementation and Application of Automata","author":"J Ortiz","year":"2011","unstructured":"Ortiz, J., Legay, A., Schobbens, P.-Y.: Distributed event clock automata. In: Bouchou-Markhoff, B., Caron, P., Champarnaud, J.-M., Maurel, D. (eds.) CIAA 2011. LNCS, vol. 6807, pp. 250\u2013263. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22256-6_23"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"3","key":"11_CR20","first-page":"247","volume":"4","author":"J-F Raskin","year":"1999","unstructured":"Raskin, J.-F., Schobbens, P.-Y.: The logic of event clocks - decidability, complexity and expressiveness. J. Autom. Lang. Comb. 4(3), 247\u2013286 (1999)","journal-title":"J. Autom. Lang. Comb."},{"issue":"6","key":"11_CR21","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1109\/TSE.2012.73","volume":"39","author":"G Rodr\u00edguez-Navas","year":"2013","unstructured":"Rodr\u00edguez-Navas, G., Proenza, J.: Using timed automata for modeling distributed systems with clocks: challenges and solutions. IEEE Trans. Software Eng. 39(6), 857\u2013868 (2013)","journal-title":"IEEE Trans. Software Eng."},{"key":"11_CR22","unstructured":"Rushby, J.M., von Henke, F.W.: Formal verification of the interactive convergence clock synchronization algorithm using EHDM (1989)"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"09","DOI":"10.4204\/EPTCS.256.14","volume":"256","author":"S Tonetta","year":"2017","unstructured":"Tonetta, S.: Linear-time temporal logic with event freezing functions. Electron. Proc. Theor. Comput. Sci. 256, 09 (2017)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"issue":"4","key":"11_CR24","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1145\/158431.158434","volume":"2","author":"F Wang","year":"1993","unstructured":"Wang, F., Mok, A.K., Emerson, E.A.: Distributed real-time system specification and verification in APTL. TOSEM 2(4), 346\u2013378 (1993)","journal-title":"TOSEM"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-33170-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,14]],"date-time":"2023-12-14T15:59:31Z","timestamp":1702569571000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-33170-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031331695","9783031331701"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-33170-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"3 June 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 May 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/nfm-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}