{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T14:03:32Z","timestamp":1776261812242,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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-22749-2_18","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:09:45Z","timestamp":1776258585000},"page":"353-372","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-5883-5082","authenticated-orcid":false,"given":"Raz","family":"Lotan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5503-5791","authenticated-orcid":false,"given":"Neta","family":"Elad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4209-1635","authenticated-orcid":false,"given":"Oded","family":"Padon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M.: The power of temporal proofs. Theor. Comput. Sci. 65(1), 35\u201383 (1989), https:\/\/doi.org\/10.1016\/0304-3975(89)90138-2","DOI":"10.1016\/0304-3975(89)90138-2"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Lee, C.S.: Ranking functions for size-change termination II. Log. Methods Comput. Sci. 5(2) (2009), http:\/\/arxiv.org\/abs\/0903.4382","DOI":"10.2168\/LMCS-5(2:8)2009"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Berkovits, I., Lazic, M., Losa, G., Padon, O., Shoham, S.: Verification of threshold-based distributed algorithms by decomposition to decidable logics. In: Computer Aided Verification - 31st International Conference, CAV 2019 (2019), https:\/\/doi.org\/10.1007\/978-3-030-25543-5_15","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Brunel, J., Chemouil, D., Tawa, J.: Analyzing the fundamental liveness property of the chord protocol. In: Formal Methods in Computer Aided Design, FMCAD 2018 (2018), https:\/\/doi.org\/10.23919\/FMCAD.2018.8603001","DOI":"10.23919\/FMCAD.2018.8603001"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Chen, Y., Heizmann, M., Leng\u00e1l, O., Li, Y., Tsai, M., Turrini, A., Zhang, L.: Advanced automata-based algorithms for program termination checking. In: Programming Language Design and Implementation, PLDI 2018 (2018), https:\/\/doi.org\/10.1145\/3192366.3192405","DOI":"10.1145\/3192366.3192405"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Magnago, E.: LTL falsification in infinite-state systems. Information and Computation (2022), https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540122001328","DOI":"10.1016\/j.ic.2022.104977"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Daniel, J., Cimatti, A., Griggio, A., Tonetta, S., Mover, S.: Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In: Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016 (2016), https:\/\/doi.org\/10.1007\/978-3-319-41528-4_15","DOI":"10.1007\/978-3-319-41528-4_15"},{"key":"18_CR8","unstructured":"Elad, N., Lotan, R.: implicit-rankings-timers, https:\/\/github.com\/neta-elad\/implicit-rankings-timers"},{"key":"18_CR9","unstructured":"Elad, N., Lotan, R.: Verifying first-order temporal properties of infinite states systems via timers and rankings (artifact) (Jan 2026), https:\/\/doi.org\/10.5281\/zenodo.18157346"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with invisible ranking. Int. J. Softw. Tools Technol. Transf. 8(3), 261\u2013279 (2006). https:\/\/doi.org\/10.1007\/S10009-005-0193-X","DOI":"10.1007\/S10009-005-0193-X"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proving liveness of parameterized programs. In: Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916 (2016). https:\/\/doi.org\/10.1145\/2933575.2935310","DOI":"10.1145\/2933575.2935310"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Geatti, L., Gianola, A., Gigante, N.: First-order automata. In: Proceedings of the Thirty-Ninth AAAI Conference on Artificial Intelligence (2025), https:\/\/doi.org\/10.1609\/aaai.v39i14.33638","DOI":"10.1609\/aaai.v39i14.33638"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83\u201392 (2017), https:\/\/doi.org\/10.1145\/3068608","DOI":"10.1145\/3068608"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Herrmann, R., R\u00fcmmer, P.: A new approach for showing termination of parameterized transition systems. In: Implementation and Application of Automata (2026), https:\/\/doi.org\/10.1007\/978-3-032-02602-6_14","DOI":"10.1007\/978-3-032-02602-6_14"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Hoenicke, J., Padon, O., Shoham, S.: On the Power of Temporal Prophecy, pp. 40\u201353. Springer Nature Switzerland, Cham (2026), https:\/\/doi.org\/10.1007\/978-3-032-13711-1_3","DOI":"10.1007\/978-3-032-13711-1_3"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Hong, C., Lin, A.W.: Regular abstractions for array systems. Proc. ACM Program. Lang. 8(POPL), 638\u2013666 (2024), https:\/\/doi.org\/10.1145\/3632864","DOI":"10.1145\/3632864"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Ioannidis, E., Zakowski, Y., Zdancewic, S., Angel, S.: Structural temporal logic for mechanized program verification (2025), https:\/\/arxiv.org\/abs\/2410.14906","DOI":"10.1145\/3763091"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Lamport, L.: A new solution of dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974), https:\/\/doi.org\/10.1145\/361082.361093","DOI":"10.1145\/361082.361093"},{"key":"18_CR19","unstructured":"Leung, D., Zeldovich, N., Kaashoek, F.: Shipwright: Proving liveness of distributed systems with byzantine participants (2025), https:\/\/arxiv.org\/abs\/2507.14080"},{"key":"18_CR20","unstructured":"Lotan, R., Elad, N., Padon, O., Shoham, S.: Verifying first-order temporal properties of infinite-state systems via timers and rankings (2026), https:\/\/arxiv.org\/abs\/2601.13325"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Lotan, R., Shoham, S.: Implicit rankings for verifying liveness properties in first-order logic. In: Tools and Algorithms for the Construction and Analysis of Systems TACAS 2025 (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_20","DOI":"10.1007\/978-3-031-90643-5_20"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Toward liveness proofs at scale. In: Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 255\u2013276. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_13","DOI":"10.1007\/978-3-031-65627-9_13"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Ouyang, L., Sun, X., Tang, R., Huang, Y., Jivrajani, M., Ma, X., Xu, T.: Multi-grained specifications for distributed system model checking and verification. In: Proceedings of the Twentieth European Conference on Computer Systems. EuroSys \u201925 (2025). https:\/\/doi.org\/10.1145\/3689031.3696069","DOI":"10.1145\/3689031.3696069"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. 2(POPL), 26:1\u201326:33 (2018). https:\/\/doi.org\/10.1145\/3158114","DOI":"10.1145\/3158114"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Padon, O., Hoenicke, J., McMillan, K.L., Podelski, A., Sagiv, M., Shoham, S.: Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods Syst. Des. 57(2), 246\u2013269 (2021). https:\/\/doi.org\/10.1007\/S10703-021-00377-1","DOI":"10.1007\/S10703-021-00377-1"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: Safety verification by interactive generalization. In: PLDI \u201916: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 614\u2013630 (Jun 2016). https:\/\/doi.org\/10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"18_CR28","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. pp. 32\u201341. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319598","DOI":"10.1109\/LICS.2004.1319598"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Qiu, L., Kim, Y., Shin, J., Kim, J., Honor\u00e9, W., Shao, Z.: Lido: Linearizable byzantine distributed objects with refinement-based liveness proofs. Proc. ACM Program. Lang. 8(PLDI), 1140\u20131164 (2024), https:\/\/doi.org\/10.1145\/3656423","DOI":"10.1145\/3656423"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Qiu, L., Xiao, J., Shin, J.Y., Shao, Z.: Lido-dag: A framework for verifying safety and liveness of dag-based consensus protocols. Proc. ACM Program. Lang. 9(PLDI) (Jun 2025), https:\/\/doi.org\/10.1145\/3729306","DOI":"10.1145\/3729306"},{"key":"18_CR31","unstructured":"Sun, X., Ma, W., Gu, J.T., Ma, Z., Chajed, T., Howell, J., Lattuada, A., Padon, O., Suresh, L., Szekeres, A., Xu, T.: Anvil: Verifying liveness of cluster management controllers. In: 18th USENIX Symposium on Operating Systems Design and Implementation (2024), https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/sun-xudong"},{"key":"18_CR32","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for Concurrency - Structure versus Automata (1995). https:\/\/doi.org\/10.1007\/3-540-60915-6_6","DOI":"10.1007\/3-540-60915-6_6"},{"key":"18_CR33","doi-asserted-by":"publisher","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J.: Mostly automated verification of liveness properties for distributed protocols with ranking functions. Proc. ACM Program. Lang. 8(POPL), 1028\u20131059 (2024). https:\/\/doi.org\/10.1145\/3632877","DOI":"10.1145\/3632877"},{"key":"18_CR34","doi-asserted-by":"publisher","unstructured":"Zhang, W.: First order b\u00fcchi automata and their application to verification of LTL specifications. J. Log. Algebraic Methods Program. 142, 101021 (2025). https:\/\/doi.org\/10.1016\/J.JLAMP.2024.101021","DOI":"10.1016\/J.JLAMP.2024.101021"},{"key":"18_CR35","doi-asserted-by":"publisher","unstructured":"Zhao, Q., P\u00eerlea, G., Grzeszkiewicz, K., Gilbert, S., Sergey, I.: Compositional verification of composite byzantine protocols. In: Conference on Computer and Communications Security. CCS \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3658644.3690355","DOI":"10.1145\/3658644.3690355"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22749-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:09:52Z","timestamp":1776258592000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}