{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T07:33:03Z","timestamp":1767771183378,"version":"build-2238731810"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:00:00Z","timestamp":1635724800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T00:00:00Z","timestamp":1647302400000},"content-version":"vor","delay-in-days":134,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/N007565\/1"],"award-info":[{"award-number":["EP\/N007565\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Future AI and Robotics for Space Hub","award":["EP\/R026092\/1"],"award-info":[{"award-number":["EP\/R026092\/1"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We introduce a framework for the verification of protocols involving a distinguished machine (referred to as a leader) orchestrating the operation of an arbitrary number of identical machines (referred to as followers) in a network. At the core of our framework is a high-level formalism capturing the operation of these types of machines together with their network interactions. We show that this formalism automatically translates to a tractable form of first-order temporal logic. Checking whether a protocol specified in our formalism satisfies a desired property (expressible in temporal logic) then amounts to checking whether the protocol\u2019s translation in first-order temporal logic entails that property. Many different types of protocols used in practice, such as cache coherence, atomic commitment, consensus, and synchronization protocols, fit within our framework. First-order temporal logic also facilitates parameterized verification by enabling us to model such protocols abstractly without referring to individual machines.<\/jats:p>","DOI":"10.1007\/s10703-022-00390-y","type":"journal-article","created":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T13:03:00Z","timestamp":1647349380000},"page":"440-468","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Parameterized verification of leader\/follower systems via first-order temporal logic"],"prefix":"10.1007","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9635-0643","authenticated-orcid":false,"given":"G.","family":"Kourtis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4610-9533","authenticated-orcid":false,"given":"C.","family":"Dixon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0875-3862","authenticated-orcid":false,"given":"M.","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3820-643X","authenticated-orcid":false,"given":"A.","family":"Lisitsa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,15]]},"reference":[{"key":"390_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Jonsson B, Nilsson M, d\u2019Orso J, Saksena M (2004) Regular Model Checking for LTL(MSO). In: International Conference on Computer Aided Verification, LNCS, vol. 3114, pp. 348\u2013360. Springer","DOI":"10.1007\/978-3-540-27813-9_27"},{"key":"390_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Jonsson B, Rezine A, Saksena M (2006) Proving liveness by backwards reachability. In: International Conference on Concurrency Theory, LNCS, vol. 4137, pp. 95\u2013109. Springer","DOI":"10.1007\/11817949_7"},{"issue":"4","key":"390_CR3","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1108\/17563780911005818","volume":"2","author":"A Behdenna","year":"2009","unstructured":"Behdenna A, Dixon C, Fisher M (2009) Deductive verification of simple foraging robotic behaviours. Int J Intell Comput Cybern 2(4):604\u2013643","journal-title":"Int J Intell Comput Cybern"},{"key":"390_CR4","doi-asserted-by":"crossref","unstructured":"Benghabrit W, Grall H, Royer JC, Sellami M (2015) Abstract accountability language: translation, compliance and application. In: Asia-Pacific Software Engineering Conference, pp. 214\u2013221. IEEE","DOI":"10.1109\/APSEC.2015.14"},{"key":"390_CR5","doi-asserted-by":"crossref","unstructured":"Benghabrit W, Grall H, Royer JC, Sellami M (2015) Checking accountability with a prover. In: Computer Software and Applications Conference, vol.\u00a02, pp. 83\u201388. IEEE","DOI":"10.1109\/COMPSAC.2015.8"},{"key":"390_CR6","volume-title":"Concurrency control and recovery in database systems","author":"PA Bernstein","year":"1987","unstructured":"Bernstein PA, Hadzilacos V, Goodman N (1987) Concurrency control and recovery in database systems. Addison-Wesley, Boston"},{"key":"390_CR7","doi-asserted-by":"publisher","unstructured":"Bhatia L, Tomic I, Fu A, Breza M, McCann JA, Control communication co-design for wide area cyber-physical systems. ACM Trans Cyber-Phys Syst https:\/\/doi.org\/10.1145\/3418528","DOI":"10.1145\/3418528"},{"issue":"1","key":"390_CR8","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/1119439.1119443","volume":"7","author":"A Degtyarev","year":"2006","unstructured":"Degtyarev A, Fisher M, Konev B (2006) Monodic temporal resolution. ACM Trans Comput Logic 7(1):108\u2013150","journal-title":"ACM Trans Comput Logic"},{"issue":"2","key":"390_CR9","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1023\/A:1021352309671","volume":"72","author":"A Degtyarev","year":"2002","unstructured":"Degtyarev A, Fisher M, Lisitsa A (2002) Equality and monodic first-order temporal logic. Studia Logica 72(2):147\u2013156","journal-title":"Studia Logica"},{"issue":"3","key":"390_CR10","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G Delzanno","year":"2003","unstructured":"Delzanno G (2003) Constraint-based verification of parameterized cache coherence protocols. Formal Methods Syst Design 23(3):257\u2013301","journal-title":"Formal Methods Syst Design"},{"key":"390_CR11","first-page":"353","volume-title":"International Conference on Computer Aided Verification","author":"G Delzanno","year":"2020","unstructured":"Delzanno G (2020) Automatic verification of parameterized cache coherence protocols. International Conference on Computer Aided Verification. Springer International Publishing, Cham, pp 353\u2013360"},{"issue":"1","key":"390_CR12","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1016\/j.jal.2005.08.003","volume":"4","author":"C Dixon","year":"2006","unstructured":"Dixon C (2006) Using temporal logics of knowledge for specification and verification-a case study. J Appl Logic 4(1):50\u201378","journal-title":"J Appl Logic"},{"key":"390_CR13","doi-asserted-by":"crossref","unstructured":"Dixon C, Fisher M, Konev B, Lisitsa A (2008) Practical first-order temporal reasoning. In: International Symposium on Temporal Representation and Reasoning, pp. 156\u2013163. IEEE","DOI":"10.1109\/TIME.2008.15"},{"key":"390_CR14","doi-asserted-by":"crossref","unstructured":"Esparza J, Finkel A, Mayr R (1999) On the verification of broadcast protocols. In: Symposium on Logic in Computer Science, pp. 352\u2013359. IEEE Computer Society Press","DOI":"10.1109\/LICS.1999.782630"},{"issue":"3","key":"390_CR15","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10817-005-7354-1","volume":"34","author":"M Fern\u00e1ndez-Gago","year":"2005","unstructured":"Fern\u00e1ndez-Gago M, Hustadt U, Dixon C, Fisher M, Konev B (2005) First-order temporal verification in practice. J Autom Reason 34(3):295\u2013321","journal-title":"J Autom Reason"},{"key":"390_CR16","unstructured":"Fisher M, Konev B, Lisitsa A (2006) Practical Infinite-State Verification with Temporal Reasoning. In: Verification of Infinite State Systems and Security, NATO Security through Science Series: Information and Communication, vol.\u00a01, pp. 91\u2013100. IOS Press"},{"key":"390_CR17","doi-asserted-by":"crossref","unstructured":"Fisher M, Konev B, Lisitsa A (2009) Temporal verification of fault-tolerant protocols. In: Methods, Models and Tools for Fault Tolerance, pp. 44\u201356. Springer","DOI":"10.1007\/978-3-642-00867-2_3"},{"key":"390_CR18","unstructured":"Fisher M, Lisitsa A (2003) Deductive verification of cache coherence protocols. In: Proceedings of the 3rd Workshop on Automated Verification of Critical Systems AVoCS, 3: 177\u2013186"},{"issue":"1","key":"390_CR19","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1132863.1132867","volume":"31","author":"J Gray","year":"2006","unstructured":"Gray J, Lamport L (2006) Consensus on transaction commit. ACM Trans Database Syst (TODS) 31(1):133\u2013160","journal-title":"ACM Trans Database Syst (TODS)"},{"key":"390_CR20","doi-asserted-by":"crossref","unstructured":"Halle S (2011) Causality in message-based contract violations: a temporal logic \u201cwhodunit\u201d. In: International Enterprise Distributed Object Computing Conference, pp. 171\u2013180. IEEE","DOI":"10.1109\/EDOC.2011.21"},{"key":"390_CR21","doi-asserted-by":"crossref","unstructured":"Hodkinson I, Kontchakov R, Kurucz A, Wolter F, Zakharyaschev M (2003) On the computational complexity of decidable fragments of first-order linear temporal logics. In: 10th International Symposium on Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings., pp. 91\u201398. IEEE","DOI":"10.1109\/TIME.2003.1214884"},{"issue":"1\u20133","key":"390_CR22","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I Hodkinson","year":"2000","unstructured":"Hodkinson I, Wolter F, Zakharyaschev M (2000) Decidable fragments of first-order temporal logics. Annals Pure Appl Logic 106(1\u20133):85\u2013134","journal-title":"Annals Pure Appl Logic"},{"key":"390_CR23","doi-asserted-by":"crossref","unstructured":"Hustadt U, Konev B, Riazanov A, Voronkov A (2004) Temp: A temporal monodic prover. In: International Joint Conference on Automated Reasoning, LNCS, vol. 3097, pp. 326\u2013330. Springer","DOI":"10.1007\/978-3-540-25984-8_23"},{"issue":"1\u20132","key":"390_CR24","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.ic.2004.10.005","volume":"199","author":"B Konev","year":"2005","unstructured":"Konev B, Degtyarev A, Dixon C, Fisher M, Hustadt U (2005) Mechanising first-order temporal resolution. Inf Comput 199(1\u20132):55\u201386","journal-title":"Inf Comput"},{"key":"390_CR25","unstructured":"Konev B, Degtyarev A, Fisher M, Lisitsa A, Characterising finite domains in monodic first-order temporal logic. Tech. rep., ULCS-09-009, Department of Computer Science, University of Liverpool"},{"key":"390_CR26","doi-asserted-by":"crossref","unstructured":"Ludwig M, Hustadt U (2009) Fair derivations in monodic temporal reasoning. In: International Conference on Automated Deduction, pp. 261\u2013276. Springer","DOI":"10.1007\/978-3-642-02959-2_21"},{"issue":"2\u20133","key":"390_CR27","doi-asserted-by":"publisher","first-page":"69","DOI":"10.3233\/AIC-2010-0457","volume":"23","author":"M Ludwig","year":"2010","unstructured":"Ludwig M, Hustadt U (2010) Implementing a fair monodic temporal logic prover. AI Commun 23(2\u20133):69\u201396","journal-title":"AI Commun"},{"key":"390_CR28","volume-title":"Distributed Algorithms","author":"NA Lynch","year":"1996","unstructured":"Lynch NA (1996) Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA"},{"issue":"2\u20133","key":"390_CR29","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(88)90045-X","volume":"57","author":"A Szalas","year":"1988","unstructured":"Szalas A, Holenderski L (1988) Incompleteness of first-order temporal logic with until. Theoretical Comput Sci 57(2\u20133):317\u2013325","journal-title":"Theoretical Comput Sci"},{"issue":"3","key":"390_CR30","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.2307\/2695115","volume":"66","author":"F Wolter","year":"2001","unstructured":"Wolter F, Zakharyaschev M (2001) Decidable fragments of first-order modal logics. J Symb Logic 66(3):1415\u20131438","journal-title":"J Symb Logic"},{"issue":"1\u20132","key":"390_CR31","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0168-0072(01)00124-5","volume":"118","author":"F Wolter","year":"2002","unstructured":"Wolter F, Zakharyaschev M (2002) Axiomatizing the monodic fragment of first-order temporal logic. Annals Pure Appl logic 118(1\u20132):133\u2013145","journal-title":"Annals Pure Appl logic"}],"updated-by":[{"DOI":"10.1007\/s10703-023-00408-z","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T00:00:00Z","timestamp":1675728000000}}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00390-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-022-00390-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00390-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,20]],"date-time":"2024-09-20T05:35:06Z","timestamp":1726810506000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-022-00390-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,11]]}},"alternative-id":["390"],"URL":"https:\/\/doi.org\/10.1007\/s10703-022-00390-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,11]]},"assertion":[{"value":"29 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 February 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}