{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:14:58Z","timestamp":1760202898332,"version":"3.37.3"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"3-5","license":[{"start":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T00:00:00Z","timestamp":1588723200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T00:00:00Z","timestamp":1588723200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003005","name":"Eindhoven University of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003005","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2020,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We enrich the operational semantics of a simple process calculus with ACP-style communication with a concurrency relation, so that for every process expression there exists an associated notion of <jats:italic>just path<\/jats:italic>. We then present sufficient conditions on the communication function and the syntax of process expressions that facilitate the formulation of justness on the level of labels rather than on individual transitions, taking a designated set of signals into account. This paves the way for the formulation of liveness properties under justness assumptions in the modal <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03bc<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus and their verification on process specifications with the mCRL2 toolset.<\/jats:p>","DOI":"10.1007\/s00236-020-00371-w","type":"journal-article","created":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T15:04:01Z","timestamp":1588777441000},"page":"551-590","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Off-the-shelf automated analysis of liveness properties for just paths"],"prefix":"10.1007","volume":"57","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5131-008X","authenticated-orcid":false,"given":"Mark","family":"Bouwman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6710-8436","authenticated-orcid":false,"given":"Bas","family":"Luttik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3049-7962","authenticated-orcid":false,"given":"Tim","family":"Willemse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,5,6]]},"reference":[{"key":"371_CR1","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(85)90088-X","volume":"37","author":"JA Bergstra","year":"1985","unstructured":"Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theor. Comput. Sci. 37, 77\u2013121 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"371_CR2","doi-asserted-by":"crossref","unstructured":"Bunte, O., Groote, J.F., Keiren, J.J.A., Laveaux, M., Neele, T., de\u00a0Vink, E.P., Wesselink, W., Wijs, A., Willemse, T.A.C.: The mCRL2 toolset for analysing concurrent systems\u2014improvements in expressivity and usability. In: TACAS (2), volume 11428 of Lecture Notes in Computer Science, pp. 21\u201339. Springer (2019)","DOI":"10.1007\/978-3-030-17465-1_2"},{"key":"371_CR3","unstructured":"Cranen, S., Luttik, B., Willemse, T.A.C.: Evidence for fixpoint logic. In: CSL, volume\u00a041 of LIPIcs, pp. 8\u201393. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"371_CR4","doi-asserted-by":"crossref","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 Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics and 14th Workshop on Structural Operational Semantics, EXPRESS\/SOS 2017, Berlin, Germany, 4th September 2017, volume 255 of EPTCS, pp. 18\u201334 (2017)","DOI":"10.4204\/EPTCS.255.0"},{"issue":"3","key":"371_CR5","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"EA Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"371_CR6","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89\u2013107 (2013)","journal-title":"STTT"},{"issue":"2\u20133","key":"371_CR7","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s00236-015-0221-6","volume":"52","author":"RJ van Glabbeek","year":"2015","unstructured":"van Glabbeek, R.J., H\u00f6fner, P.: CCS: it\u2019s not fair!\u2014fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions. Acta Inf. 52(2\u20133), 175\u2013205 (2015)","journal-title":"Acta Inf."},{"issue":"4","key":"371_CR8","first-page":"69:1","volume":"52","author":"RJ van Glabbeek","year":"2019","unstructured":"van Glabbeek, R.J., H\u00f6fner, P.: Progress, justness, and fairness. ACM Comput. Surv. 52(4), 69:1\u201369:38 (2019)","journal-title":"ACM Comput. Surv."},{"key":"371_CR9","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J.: Justness\u2014a completeness criterion for capturing liveness properties (extended abstract). In: FoSSaCS, volume 11425 of Lecture Notes in Computer Science, pp. 505\u2013522. Springer (2019)","DOI":"10.1007\/978-3-030-17127-8_29"},{"issue":"4","key":"371_CR10","doi-asserted-by":"publisher","first-page":"371","DOI":"10.3233\/FI-2009-109","volume":"93","author":"RJ van Glabbeek","year":"2009","unstructured":"van Glabbeek, R.J., Luttik, B., Trcka, N.: Branching bisimilarity with explicit divergence. Fundam. Inform. 93(4), 371\u2013392 (2009)","journal-title":"Fundam. Inform."},{"key":"371_CR11","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J., Luttik, B., Trcka, N.: Computation tree logic with deadlock detection. Log. Methods Comput. Sci. 5(4) (2009)","DOI":"10.2168\/LMCS-5(4:5)2009"},{"issue":"3","key":"371_CR12","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/j.scico.2004.08.002","volume":"56","author":"JF Groote","year":"2005","unstructured":"Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Sci. Comput. Program. 56(3), 251\u2013273 (2005)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"371_CR13","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985)","journal-title":"J. ACM"},{"issue":"3","key":"371_CR14","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1982","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theoret. Comput. Sci. 27(3), 333\u2013354 (1982)","journal-title":"Theoret. Comput. Sci."},{"issue":"8","key":"371_CR15","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"key":"371_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Theoretical Computer Science. Lecture Notes in Computer Science, vol. 104, pp. 167\u2013183. Springer, Berlin (1981)"},{"issue":"3","key":"371_CR17","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"371_CR18","unstructured":"Wesselink, W., Willemse, T.A.C.: Evidence extraction from parameterised Boolean equation systems. In: ARQNL@IJCAR, volume 2095 of CEUR Workshop Proceedings, pp. 86\u2013100. CEUR-WS.org (2018)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00371-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-020-00371-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00371-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,5]],"date-time":"2021-05-05T23:29:23Z","timestamp":1620257363000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-020-00371-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,6]]},"references-count":18,"journal-issue":{"issue":"3-5","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["371"],"URL":"https:\/\/doi.org\/10.1007\/s00236-020-00371-w","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2020,5,6]]},"assertion":[{"value":"15 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 February 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 May 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}