{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:13:31Z","timestamp":1760202811493,"version":"3.41.2"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030171261"},{"type":"electronic","value":"9783030171278"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T00:00:00Z","timestamp":1554422400000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper poses that transition systems constitute a good model of distributed systems only in combination with a criterion telling which paths model complete runs of the represented systems. Among such criteria, progress is too weak to capture relevant liveness properties, and fairness is often too strong; for typical applications we advocate the intermediate criterion of justness. Previously, we proposed a definition of justness in terms of an asymmetric concurrency relation between transitions. Here we define such a concurrency relation for the transition systems associated to the process algebra CCS as well as its extensions with broadcast communication and signals, thereby making these process algebras suitable for capturing liveness properties requiring justness.<\/jats:p>","DOI":"10.1007\/978-3-030-17127-8_29","type":"book-chapter","created":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T11:11:46Z","timestamp":1554462706000},"page":"505-522","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Justness"],"prefix":"10.1007","author":[{"given":"Rob","family":"van Glabbeek","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,5]]},"reference":[{"issue":"4","key":"29_CR1","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/BF01872848","volume":"2","author":"KR Apt","year":"1988","unstructured":"Apt, K.R., Francez, N., Katz, S.: Appraising fairness in languages for distributed programming. Distrib. Comput. 2(4), 226\u2013241 (1988). https:\/\/doi.org\/10.1007\/BF01872848","journal-title":"Distrib. Comput."},{"unstructured":"Bednarczyk, M.: Categories of asynchronous systems. Ph.D. thesis, Computer Science, University of Sussex, Brighton (1987)","key":"29_CR2"},{"unstructured":"Bouwman, M.S.: Liveness analysis in process algebra: simpler techniques to model mutex algorithms. Technical report, Eindhoven University of Technology (2018). http:\/\/www.win.tue.nl\/~timw\/downloads\/bouwman_seminar.pdf","key":"29_CR3"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-38493-6_4","volume-title":"Coordination Models and Languages","author":"M Coppo","year":"2013","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: Inference of global progress properties for dynamically interleaved multiparty sessions. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 45\u201359. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38493-6_4"},{"issue":"2","key":"29_CR5","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R De Nicola","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458\u2013487 (1995). https:\/\/doi.org\/10.1145\/201019.201032","journal-title":"J. ACM"},{"doi-asserted-by":"publisher","unstructured":"Dyseryn, V., van Glabbeek, R.J., H\u00f6fner, P.: Analysing mutual exclusion using process algebra with signals. In: Peters, K., Tini, S. (eds.) Proceedings of the Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, Electronic Proceedings in Theoretical Computer Science 255. Open Publishing Association, pp. 18\u201334 (2017). https:\/\/doi.org\/10.4204\/EPTCS.255.2","key":"29_CR6","DOI":"10.4204\/EPTCS.255.2"},{"issue":"3","key":"29_CR7","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982). https:\/\/doi.org\/10.1016\/0167-6423(83)90017-5","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"29_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u2018Sometimes\u2019 and \u2018Not Never\u2019 revisited: on branching time versus linear time temporal logic. J. ACM 33(1), 151\u2013178 (1986). https:\/\/doi.org\/10.1145\/4904.4999","journal-title":"J. ACM"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-28869-2_15","volume-title":"Programming Languages and Systems","author":"A Fehnker","year":"2012","unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 295\u2013315. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_15"},{"unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical report 5513, NICTA (2013). http:\/\/arxiv.org\/abs\/1312.7645","key":"29_CR10"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-23506-6_9","volume-title":"Correct System Design","author":"RJ van Glabbeek","year":"2015","unstructured":"van Glabbeek, R.J.: Structure preserving bisimilarity, supporting an operational petri net semantics of CCSP. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 99\u2013130. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23506-6_9. http:\/\/arxiv.org\/abs\/1509.05842"},{"unstructured":"van Glabbeek, R.J.: Ensuring Liveness Properties of Distributed Systems (A Research Agenda). Position paper (2016). http:\/\/arxiv.org\/abs\/org\/abs\/1711.04240","key":"29_CR12"},{"unstructured":"van Glabbeek, R.J.: Justness: a completeness criterion for capturing liveness properties. Technical report, Data61, CSIRO (2018). http:\/\/www.cse.unsw.edu.au\/~rvg\/synchrons.pdf. Full version of the present paper","key":"29_CR13"},{"doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J., H\u00f6fner, P.: CCS: It\u2019s not fair! Acta Inform. 52(2\u20133), 175\u2013205 (2015). https:\/\/doi.org\/10.1007\/s00236-015-0221-6","key":"29_CR14","DOI":"10.1007\/s00236-015-0221-6"},{"unstructured":"van Glabbeek, R.J., H\u00f6fner, P.: Progress, fairness and justness in process algebra. Technical report 8501, NICTA (2015). http:\/\/arxiv.org\/abs\/1501.03268","key":"29_CR15"},{"unstructured":"van Glabbeek, R.J., H\u00f6fner, P.: Progress, justness and fairness. Survey paper, Data61, CSIRO, Sydney, Australia (2018). https:\/\/arxiv.org\/abs\/1810.07414","key":"29_CR16"},{"unstructured":"Kuiper, R., de\u00a0Roever, W.-P.: Fairness assumptions for CSP in a temporal logic framework. In: Bj\u00f8rner, D. (ed.) Formal Description of Programming Concepts II, North-Holland, pp. 159\u2013170 (1983)","key":"29_CR17"},{"issue":"2","key":"29_CR18","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977). https:\/\/doi.org\/10.1109\/TSE.1977.229904","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"29_CR19","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/PL00008921","volume":"13","author":"L Lamport","year":"2000","unstructured":"Lamport, L.: Fairness and hyperfairness. Distrib. Comput. 13(4), 239\u2013245 (2000). https:\/\/doi.org\/10.1007\/PL00008921","journal-title":"Distrib. Comput."},{"key":"29_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","year":"1980","unstructured":"Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3"},{"unstructured":"Misra, J.: A Rebuttal of Dijkstra\u2019s position on fairness (1988). http:\/\/www.cs.utexas.edu\/users\/misra\/Notes.dir\/fairness.pdf","key":"29_CR21"},{"key":"29_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8528-6","volume-title":"A Discipline of Multiprogramming\u2014Programming Theory for Distributed Applications","author":"J Misra","year":"2001","unstructured":"Misra, J.: A Discipline of Multiprogramming\u2014Programming Theory for Distributed Applications. Springer, New York (2001). https:\/\/doi.org\/10.1007\/978-1-4419-8528-6"},{"issue":"3","key":"29_CR23","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"SS Owicki","year":"1982","unstructured":"Owicki, S.S., Lamport, L.: Proving liveness properties of concurrent programs. ACM TOPLAS 4(3), 455\u2013495 (1982). https:\/\/doi.org\/10.1145\/357172.357178","journal-title":"ACM TOPLAS"},{"doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS 1977), pp. 46\u201357. IEEE (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","key":"29_CR24","DOI":"10.1109\/SFCS.1977.32"},{"key":"29_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-53982-4_19","volume-title":"TAPSOFT \u201991","author":"KVS Prasad","year":"1991","unstructured":"Prasad, K.V.S.: A calculus of broadcasting systems. In: Abramsky, S., Maibaum, T.S.E. (eds.) CAAP 1991. LNCS, vol. 493, pp. 338\u2013358. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53982-4_19"},{"key":"29_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33278-4","volume-title":"Understanding Petri Nets\u2014Modeling Techniques, Analysis Methods, Case Studies","author":"W Reisig","year":"2013","unstructured":"Reisig, W.: Understanding Petri Nets\u2014Modeling Techniques, Analysis Methods, Case Studies. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-33278-4"},{"issue":"5","key":"29_CR27","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1093\/comjnl\/28.5.449","volume":"28","author":"MW Shields","year":"1985","unstructured":"Shields, M.W.: Concurrent machines. Comput. J. 28(5), 449\u2013465 (1985). https:\/\/doi.org\/10.1093\/comjnl\/28.5.449","journal-title":"Comput. J."},{"issue":"3","key":"29_CR28","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0304-3975(89)90050-9","volume":"64","author":"EW Stark","year":"1989","unstructured":"Stark, E.W.: Concurrent transition systems. Theor. Comput. Sci. 64(3), 221\u2013269 (1989). https:\/\/doi.org\/10.1016\/0304-3975(89)90050-9","journal-title":"Theor. Comput. Sci."},{"key":"29_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-17906-2_31","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"G Winskel","year":"1987","unstructured":"Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986, Part II. LNCS, vol. 255, pp. 325\u2013392. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-17906-2_31"},{"key":"29_CR30","first-page":"1","volume-title":"Handbook of Logic in Computer Science, Chap. 1, 4: Semantic Modelling","author":"G Winskel","year":"1995","unstructured":"Winskel, G., Nielsen, M.: Models for concurrency. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, Chap. 1, 4: Semantic Modelling, pp. 1\u2013148. Oxford University Press, Oxford (1995)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17127-8_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T22:22:53Z","timestamp":1753309373000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17127-8_29"}},"subtitle":["A Completeness Criterion for Capturing Liveness Properties (Extended Abstract)"],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171261","9783030171278"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17127-8_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}