{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T01:13:43Z","timestamp":1648862023284},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,5,4]],"date-time":"2011-05-04T00:00:00Z","timestamp":1304467200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2011,8]]},"DOI":"10.1007\/s10703-011-0117-1","type":"journal-article","created":{"date-parts":[[2011,5,3]],"date-time":"2011-05-03T13:48:57Z","timestamp":1304430537000},"page":"1-46","source":"Crossref","is-referenced-by-count":2,"title":["On the refinement of liveness properties of distributed systems"],"prefix":"10.1007","volume":"39","author":[{"given":"Paul C.","family":"Attie","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,5,4]]},"reference":[{"issue":"2","key":"117_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi M, Lamport L (1991) The existence of refinement mappings. Theor Comput Sci 82(2):253\u2013284","journal-title":"Theor Comput Sci"},{"issue":"3","key":"117_CR2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern B, Schneider F (1987) Recognizing safety and liveness. Distrib Comput 2(3):117\u2013126","journal-title":"Distrib Comput"},{"issue":"1","key":"117_CR3","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1145\/59287.62028","volume":"11","author":"B Alpern","year":"1989","unstructured":"Alpern B, Schneider F (1989) Verifying temporal properties without temporal logic. ACM Trans Program Lang Syst 11(1):147\u2013167","journal-title":"ACM Trans Program Lang Syst"},{"key":"117_CR4","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-60045-0_49","volume-title":"CAV 95: Computer-aided verification","author":"R Alur","year":"1995","unstructured":"Alur R, Henzinger TA (1995) Local liveness for compositional modeling of fair reactive systems. In: Wolper P (ed) CAV 95: Computer-aided verification. Lecture notes in computer science, vol\u00a0939. Springer, Berlin, pp 166\u2013179"},{"key":"117_CR5","unstructured":"Attie PC (2008) On the refinement of liveness properties of distributed systems. Technical report, Department of Computer Science, American University of Beirut, Feb 2008. Available at http:\/\/arxiv.org\/PS_cache\/arxiv\/pdf\/0801\/0801.0949v1.pdf"},{"key":"117_CR6","series-title":"LNCS","volume-title":"CONCUR\u201901: 12th international conference on concurrency theory","author":"PC Attie","year":"2001","unstructured":"Attie PC, Lynch NA (2001) Dynamic input\/output automata: a formal model for dynamic systems (extended abstract). In: CONCUR\u201901: 12th international conference on concurrency theory. LNCS. Springer, Berlin"},{"issue":"1","key":"117_CR7","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1145\/963778.963782","volume":"26","author":"PC Attie","year":"2004","unstructured":"Attie PC, Arora A, Emerson EA (2004) Synthesis of fault-tolerant concurrent programs. ACM Trans Program Lang Syst 26(1):125\u2013185","journal-title":"ACM Trans Program Lang Syst"},{"key":"117_CR8","series-title":"Cambridge tracts in theoretical computer science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624193","volume-title":"Process algebra","author":"JCM Baeten","year":"1990","unstructured":"Baeten JCM, Weijland WP (1990) Process algebra. Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge"},{"key":"117_CR9","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/3-540-60692-0_69","volume-title":"15th conference on the foundations of software technology and theoretical computer science","author":"A Browne","year":"1995","unstructured":"Browne A, Manna Z, Sipma H (1995) Generalized temporal verification diagrams. In: 15th conference on the foundations of software technology and theoretical computer science. LNCS, vol\u00a01026. Springer, Berlin, pp 484\u2013498"},{"key":"117_CR10","volume-title":"Parallel program design","author":"KM Chandy","year":"1988","unstructured":"Chandy KM, Misra J (1988) Parallel program design. Addison-Wesley, Reading"},{"key":"117_CR11","volume-title":"Proceedings 4th annual symposium on principles of programming languages","author":"P Cousot","year":"1977","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a\u00a0unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings 4th annual symposium on principles of programming languages. ACM, New York"},{"key":"117_CR12","volume-title":"Proceedings of the workshop on verification and computational logic (VCL\u20192000)","author":"D Dams","year":"2000","unstructured":"Dams D, Gerth R, Grumberg O (2000) Fair model checking of abstractions. In: Proceedings of the workshop on verification and computational logic (VCL\u20192000), University of Southampton, July 2000. Springer, Berlin"},{"key":"117_CR13","volume-title":"International conference on distributed computing systems","author":"M Demirbas","year":"2002","unstructured":"Demirbas M, Arora A (2002) Convergence refinement. In: International conference on distributed computing systems. Vienna, Austria, July 2002"},{"key":"117_CR14","first-page":"84","volume-title":"12th ann ACM symp on principles of programming languages","author":"EA Emerson","year":"1985","unstructured":"Emerson EA, Lei C (1985) Modalities for model checking: branching time logic strikes back. In: 12th ann ACM symp on principles of programming languages, New Orleans, Louisiana, Jan 1985. ACM, New York, pp 84\u201396"},{"key":"117_CR15","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/S0304-3975(98)00239-4","volume":"220","author":"A Fekete","year":"1999","unstructured":"Fekete A, Gupta D, Luchango V, Lynch N, Shvartsman A (1999) Eventually-serializable data services. Theor Comput Sci 220:113\u2013156. Conference version appears in ACM symposium on principles of distributed computing (1996)","journal-title":"Theor Comput Sci"},{"key":"117_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4886-6","volume-title":"Fairness","author":"N Francez","year":"1986","unstructured":"Francez N (1986) Fairness. Springer, New York"},{"key":"117_CR17","first-page":"285","volume-title":"Foundations of component-based systems","author":"SJ Garland","year":"2000","unstructured":"Garland SJ, Lynch NA (2000) Using I\/O automata for developing distributed systems. In: Leavens GT, Sitaraman M (eds) Foundations of component-based systems. Cambridge University Press, Cambridge, pp 285\u2013312"},{"key":"117_CR18","unstructured":"Gawlick R, Segala R, Sogaard-Andersen JF, Lynch NA (1993) Liveness in timed and untimed systems. Technical Report MIT\/LCS\/TR-587, MIT Laboratory for Computer Science, Boston, Mass, Nov 1993"},{"issue":"2","key":"117_CR19","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1006\/inco.1997.2671","volume":"141","author":"R Gawlick","year":"1998","unstructured":"Gawlick R, Segala R, Sogaard-Andersen JF, Lynch NA (1998) Liveness in timed and untimed systems. Inf Comput 141(2):119\u2013171","journal-title":"Inf Comput"},{"issue":"4","key":"117_CR20","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1145\/1024922.1024923","volume":"5","author":"D Griffioen","year":"2004","unstructured":"Griffioen D, Vaandrager F (2004) A theory of normed simulations. ACM Trans Comput Log 5(4):577\u2013610","journal-title":"ACM Trans Comput Log"},{"issue":"3","key":"117_CR21","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg O, Long DE (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843\u2013871","journal-title":"ACM Trans Program Lang Syst"},{"key":"117_CR22","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-63141-0_19","volume-title":"CONCUR\u201997: eighth international conference on concurrency theory","author":"TA Henzinger","year":"1997","unstructured":"Henzinger TA, Kupferman O, Rajamani SK (1997) Fair simulation. In: Mazurkiewicz A, Wonkowski J (eds) CONCUR\u201997: eighth international conference on concurrency theory. Lecture notes in computer science, vol\u00a0939. Warsaw, Poland, July 1997. Springer, Berlin, pp 273\u2013287"},{"key":"117_CR23","series-title":"Prentice Hall international series in computer science","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall international series in computer science. Prentice Hall, Englewood Cliffs"},{"key":"117_CR24","unstructured":"Jensen HE (1999) Abstraction-based verification of distributed systems. PhD thesis, Institute for Computer Science, Aalborg University, June 1999"},{"key":"117_CR25","series-title":"Synthesis lectures on computer science","volume-title":"The theory of timed I\/O automata","author":"DK Kaynar","year":"2010","unstructured":"Kaynar DK, Lynch NA, Segala R, Vaandrager F (2010) The theory of timed I\/O automata, 2nd edn. Synthesis lectures on computer science. Morgan Claypool Publishers, San Rafael","edition":"2"},{"issue":"1","key":"117_CR26","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y Kesten","year":"2000","unstructured":"Kesten Y, Pnueli A (2000) Verification by augmented finitary abstraction. Inf Comput 163(1):203\u2013243","journal-title":"Inf Comput"},{"issue":"4","key":"117_CR27","doi-asserted-by":"crossref","first-page":"668","DOI":"10.1006\/jcss.2000.1744","volume":"62","author":"Y Kesten","year":"2001","unstructured":"Kesten Y, Pnueli A, Vardi MY (2001) Verification by augmented abstraction: the automata-theoretic view. J Comput Syst Sci 62(4):668\u2013690","journal-title":"J Comput Syst Sci"},{"issue":"4","key":"117_CR28","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1145\/138873.138877","volume":"10","author":"R Ladin","year":"1992","unstructured":"Ladin R, Liskov B, Shrira L, Ghemawat S (1992) Providing high availability using lazy replication. ACM Trans Comput Syst 10(4):360\u2013391","journal-title":"ACM Trans Comput Syst"},{"issue":"2","key":"117_CR29","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L Lamport","year":"1977","unstructured":"Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng SE-3(2):125\u2013143","journal-title":"IEEE Trans Softw Eng"},{"issue":"3","key":"117_CR30","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport L (1994) The temporal logic of actions. ACM Trans Program Lang Syst 16(3):872\u2013923","journal-title":"ACM Trans Program Lang Syst"},{"key":"117_CR31","volume-title":"Specifying systems: the TLA+ language and tools for hardware and software engineers","author":"L Lamport","year":"2002","unstructured":"Lamport L (2002) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, Reading"},{"issue":"6","key":"117_CR32","doi-asserted-by":"crossref","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"BH Liskov","year":"1994","unstructured":"Liskov BH, Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst 16(6):1811\u20131841","journal-title":"ACM Trans Program Lang Syst"},{"key":"117_CR33","unstructured":"Lynch NA, Tuttle MR (1989) An introduction to input\/output automata. Technical Report CWI-Quarterly, 2(3):219\u2013246, Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands, Sept 1989"},{"issue":"2","key":"117_CR34","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"NA Lynch","year":"1995","unstructured":"Lynch NA, Vaandrager FW (1995) Forward and backward simulations\u2014part I: untimed systems. Inf Comput 121(2):214\u2013233","journal-title":"Inf Comput"},{"issue":"1","key":"117_CR35","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"NA Lynch","year":"2003","unstructured":"Lynch NA, Segala R, Vaandraager F (2003) Hybrid I\/O automata. Inf Comput 185(1):105\u2013157. Technical Report MIT-LCS-TR-827d, MIT Laboratory for Computer Science, Cambridge, MA 02139, 13 Jan 2003","journal-title":"Inf Comput"},{"key":"117_CR36","volume-title":"ACM principles of programming languages","author":"Z Manna","year":"1983","unstructured":"Manna Z, Pnueli A (1983) How to cook a temporal proof system for your pet language. In: ACM principles of programming languages, Austin, Texas, Jan 1983"},{"key":"117_CR37","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/93385.93442","volume-title":"9th podc","author":"Z Manna","year":"1990","unstructured":"Manna Z, Pnueli A (1990) A hierarchy of temporal properties. In: 9th podc, Quebec, Canada, Aug 1990, pp 377\u2013408"},{"issue":"1","key":"117_CR38","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Manna Z, Pnueli A (1991) Completing the temporal picture. Chic J Theor Comput Sci 83(1):97\u2013130","journal-title":"Chic J Theor Comput Sci"},{"key":"117_CR39","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems","author":"Z Manna","year":"1992","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems. Springer, Berlin"},{"key":"117_CR40","series-title":"NATO ASI series, series F: Computer and system sciences","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/978-3-662-02880-3_10","volume-title":"Program design calculi","author":"Z Manna","year":"1993","unstructured":"Manna Z, Pnueli A (1993) A temporal proof methodology for reactive systems. In: Program design calculi. NATO ASI series, series F: Computer and system sciences, vol 118. Springer, Berlin, pp 287\u2013323"},{"key":"117_CR41","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"726","DOI":"10.1007\/3-540-57887-0_123","volume-title":"International symposium on theoretical aspects of computer software","author":"Z Manna","year":"1994","unstructured":"Manna Z, Pnueli A (1994) Temporal verification diagrams. In: International symposium on theoretical aspects of computer software. Lecture notes in computer science, vol\u00a0789. Springer, Berlin, pp 726\u2013765"},{"key":"117_CR42","series-title":"LNCS","first-page":"28","volume-title":"AMAST\u201998","author":"Z Manna","year":"1998","unstructured":"Manna Z, Browne A, Sipma H, Uribe T (1998) Visual abstraction for temporal verification. In: AMAST\u201998. LNCS, vol\u00a01548. Springer, Berlin, pp 28\u201341"},{"key":"117_CR43","volume-title":"Communication and concurrency","author":"R Milner","year":"1989","unstructured":"Milner R (1989) Communication and concurrency. Prentice-Hall, Englewood Cliffs"},{"key":"117_CR44","volume-title":"Communicating and mobile systems: the \u03c0-calculus","author":"R Milner","year":"1999","unstructured":"Milner R (1999) Communicating and mobile systems: the \u03c0-calculus. Addison-Wesley, Reading"},{"key":"117_CR45","volume-title":"IEEE INFOCOM","author":"A Myers","year":"1999","unstructured":"Myers A, Dinda P, Zhang H (1999) Performance characteristics of mirror servers on the Internet. In: IEEE INFOCOM"},{"issue":"3","key":"117_CR46","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S Owicki","year":"1982","unstructured":"Owicki S, Lamport L (1982) Proving liveness properties of concurrent programs. ACM Trans Program Lang Syst 4(3):455\u2013495","journal-title":"ACM Trans Program Lang Syst"},{"key":"117_CR47","volume-title":"Proceedings CADE 11","author":"S Owre","year":"1992","unstructured":"Owre S, Shankar N, Rushby J (1992) PVS: a\u00a0prototype verification system. In: Proceedings CADE 11, Saratoga Springs, NY, Jun 1992"},{"key":"117_CR48","first-page":"46","volume-title":"IEEE symposium on foundations of computer science","author":"A Pnueli","year":"1977","unstructured":"Pnueli A (1977) The temporal logic of programs. In: IEEE symposium on foundations of computer science. IEEE Press, New York, pp 46\u201357"},{"issue":"3","key":"117_CR49","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1137\/S0895480198342310","volume":"13","author":"K Pruhs","year":"2000","unstructured":"Pruhs K, Kalyanasundaram B (2000) The online transportation problem. SIAM J Discrete Math 13(3):370\u2013383","journal-title":"SIAM J Discrete Math"},{"key":"117_CR50","series-title":"LNCS","first-page":"234","volume-title":"CONCUR\u201995: concurrency theory (6th international conference)","author":"R Segala","year":"1995","unstructured":"Segala R (1995) A compositional trace-based semantics for probabilistic automata. In: Lee I, Smolka SA (eds) CONCUR\u201995: concurrency theory (6th international conference). LNCS, vol 962. Springer, Berlin, pp 234\u2013248"},{"key":"117_CR51","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0020-0190(89)90063-X","volume":"32","author":"AP Sistla","year":"1989","unstructured":"Sistla AP (1989) On verifying that a concerrent program satisfies a non-deterministic specification. Inf Process Lett 32:17\u201323","journal-title":"Inf Process Lett"},{"key":"117_CR52","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0020-0190(91)90061-L","volume":"39","author":"AP Sistla","year":"1991","unstructured":"Sistla AP (1991) Proving correctness with respect to non-deterministic safety specifications. Inf Process Lett 39:45\u201349","journal-title":"Inf Process Lett"},{"key":"117_CR53","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla AP (1994) Safety, liveness and fairness in temporal logic. Form Asp Comput 6:495\u2013511","journal-title":"Form Asp Comput"},{"key":"117_CR54","unstructured":"Sogaard-Andersen JF, Lynch NA, Lampson BW (1993) Correctness of communication protocols: a\u00a0case study. Technical report MIT\/LCS\/TR-589, MIT Laboratory for Computer Science, Boston, Mass, Nov 1993"},{"key":"117_CR55","unstructured":"Uribe TE (1998) Abstraction-based deductive-algorithmic verification of reactive systems. PhD thesis, Computer Science Department, Stanford University, Dec 1998. Technical Report STAN-CS-TR-99-1618"},{"key":"117_CR56","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"MY Vardi","year":"1991","unstructured":"Vardi MY (1991) Verification of concurrent programs\u2014the automata theoretic framework. Ann Pure Appl Log 51:79\u201398","journal-title":"Ann Pure Appl Log"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0117-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0117-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0117-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,22]],"date-time":"2021-11-22T14:21:28Z","timestamp":1637590888000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0117-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,4]]},"references-count":56,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["117"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0117-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5,4]]}}}