{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:42:06Z","timestamp":1777596126615,"version":"3.51.4"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Since distributed systems are inherently concurrent and asynchronous, it is a challenge for us to verify distributed systems. MSVL is a useful temporal logic programming language and its axiomatic system has been established. However, the axiomatic system of MSVL lacks mechanisms to manage asynchronous communication, which makes it cannot deal with distributed systems. Thus, to verify distributed systems with MSVL in a deductive way, this paper is motivated to extend the axiomatic system of MSVL with new axioms for asynchronous communication. To this end, firstly we formalize state axioms regarding asynchronous communication commands and then prove the soundness and completeness. Further, to demonstrate how the extended axiomatic system of MSVL works for distributed systems, we apply it to the well-known Ricart\u2013Agrawala (RA) algorithm, which is a distributed mutual exclusion algorithm and has an infinite state space. To do this, we model the RA algorithm with MSVL, specify the desired properties and then verify an instance of the RA algorithm with respect to the first-come-first-served property.<\/jats:p>","DOI":"10.1007\/s00165-014-0303-1","type":"journal-article","created":{"date-parts":[[2014,7,28]],"date-time":"2014-07-28T06:10:48Z","timestamp":1406527848000},"page":"103-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Verification of distributed systems with the axiomatic system of MSVL"],"prefix":"10.1145","volume":"27","author":[{"given":"Qian","family":"Ma","sequence":"first","affiliation":[{"name":"Institute of Computing Theory and Technology, Xidian University, P.O. Box 177, No. 2 South Tai Bai Road, 710071, Xi\u2019an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[{"name":"Institute of Computing Theory and Technology, Xidian University, P.O. Box 177, No. 2 South Tai Bai Road, 710071, Xi\u2019an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nan","family":"Zhang","sequence":"additional","affiliation":[{"name":"Institute of Computing Theory and Technology, Xidian University, P.O. Box 177, No. 2 South Tai Bai Road, 710071, Xi\u2019an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaobing","family":"Wang","sequence":"additional","affiliation":[{"name":"Institute of Computing Theory and Technology, Xidian University, P.O. Box 177, No. 2 South Tai Bai Road, 710071, Xi\u2019an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/1721654.1721672"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Barringer H Fisher M Gabbay D Gough G Owens R (1990) METATEM: a framework for programming in temporal logic. In: Proceedings on Stepwise refinement of distributed systems: models formalisms correctness REX workshop. Springer-Verlag New York Inc. New York pp 94\u2013129","DOI":"10.1007\/3-540-52559-9_62"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","DOI":"10.1090\/conm\/029","volume-title":"Automating theorem proving: after 25\u00a0years","author":"Bledsoe W","year":"1984"},{"key":"e_1_2_1_2_4_2","volume-title":"Distributed systems analysis with CCS","author":"Bruns G","year":"1996"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Clarke EM Emerson EA (1981) Design and synthesis of synchronization skeletons using branching timed temporal logic. In: LNCS vol 131. Springer Bertin pp 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Cranen S Groote J Keiren JJA Stappers FPM Vink EP Wesselink W Willemse TA (2013) An overview of the mCRL2 toolset and its recent advances. In: Piterman N Smolka SA (eds) Tools and algorithms for the construction and analysis of systems vol 7795. Lecture notes in computer science Springer Berlin pp 199\u2013213","DOI":"10.1007\/978-3-642-36742-7_15"},{"key":"e_1_2_1_2_7_2","unstructured":"Clarke EM Grumberg O Peled D (2008) Model checking. The MIT Press Cambridge"},{"issue":"6","key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","first-page":"710","DOI":"10.1109\/TSE.1983.235434","article-title":"Formal specification and verification of distributed systems","volume":"9","author":"Chen B-S","year":"1983","journal-title":"Trans Soft Eng SE-"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.03.007"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Duan Z Koutny M Holt C (1994) Projection in temporal logic programming. In: Proceedings of logic programming and automated reasoning. LNAI vol 822 pp 333\u2013344","DOI":"10.1007\/3-540-58216-9_48"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Dong J Sun J Liu Y (2013) Build your own model checker in one month. In: Poceedings of ICSE13 pp 1481\u20131483","DOI":"10.1109\/ICSE.2013.6606751"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Duan Z Tian C (2008) A unified model checking approach with projection temporal logic. In: Proceedings of ICFEM08 pp 167\u2013186","DOI":"10.1007\/978-3-540-88194-0_12"},{"key":"e_1_2_1_2_13_2","unstructured":"Duan Z (1996) An extended interval temporal logic and a framing technique for temporal logic programming. PhD thesis University of Newcastle Upon Tyne May 1996"},{"key":"e_1_2_1_2_14_2","volume-title":"Temporal logic and temporal logic programming language","author":"Duan Z","year":"2006"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Fisher M (1994) A survey of concurrent metatem: the language and its applications. In: Temporal logic. Lecture notes in computer science vol 827. Springer Berlin pp 480\u2013505","DOI":"10.1007\/BFb0014005"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/1199324"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"#cr-split#-e_1_2_1_2_18_2.1","doi-asserted-by":"crossref","unstructured":"Jensen K (1991) Coloured petri nets: a high level language for system design and analysis. In: Rozenberg G","DOI":"10.1007\/978-3-642-84524-6_2"},{"key":"#cr-split#-e_1_2_1_2_18_2.2","unstructured":"(ed) Advances in petri nets 1990 vol 483. Lecture notes in computer science Springer Berlin pp 342-416"},{"key":"e_1_2_1_2_19_2","unstructured":"Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis Oxford University"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Lynch NA Tuttle MR (1987) Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the sixth annual ACM symposium on principles of distributed computing. PODC \u201987 pp 137\u2013151","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_1_2_22_2","unstructured":"Milner R (1982) A calculus of communicating systems. Springer-Verlag New York Inc. Secaucus"},{"key":"e_1_2_1_2_23_2","unstructured":"Milner R (1999) Communicating and mobile systems: the \u03c0-calculus. Cambridge University Press Cambridge"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Moszkowski BC (1986) Executing temporal logic programs. PhD thesis Cambridge Uniersity Cambridge","DOI":"10.1007\/3-540-15670-4_6"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Mo D Wang X Duan Z (2011) Asynchronous communication in MSVL. In: Proceeding of ICFEM2011. LNCS vol 6991 pp 82\u201397","DOI":"10.1007\/978-3-642-24559-6_8"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/356698.356702"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th annal IEEE symposium on foudations of computer science. IEEE Computer Society pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/358527.358537"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2012.73"},{"key":"e_1_2_1_2_31_2","unstructured":"Tang CS (1983) Toward a unified logic basis for programming languages. In: Proceedings of IFIP congress. Elsevier Science North Holland pp 425\u2013429"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Tian C Duan Z (2011) Expressiveness of propositional projection temporal logic with star. Theor Comput Sci 412:1729\u20131744","DOI":"10.1016\/j.tcs.2010.12.047"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Woodcock J Larsen PG Bicarregui J Fitzgerald J (2009) Formal methods: practice and experience. Comput Surv 41(4):19: 1\u201319:36","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129510000241"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0303-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0303-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0303-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:55:19Z","timestamp":1641484519000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0303-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1]]}},"alternative-id":["10.1007\/s00165-014-0303-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0303-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1]]}}}