{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T05:08:43Z","timestamp":1769317723530,"version":"3.49.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>There exist a rich and well-developed theory of enhancements of the coinduction proof method, widely used on behavioural relations such as bisimilarity. We study how to develop an analogous theory for inductive behaviour relations, i.e., relations defined from inductive observables. Similarly to the coinductive setting, our theory makes use of (semi)-progressions of the form R-&gt;F(R), where R is a relation on processes and F is a function on relations, meaning that there is an appropriate match on the transitions that the processes in R can perform in which the process derivatives are in F(R). For a given preorder, an enhancement corresponds to a sound function, i.e., one for which R-&gt;F(R) implies that R is contained in the preorder; and similarly for equivalences. We introduce weights on the observables of an inductive relation, and a weight-preserving condition on functions that guarantees soundness. We show that the class of functions contains non-trivial functions and enjoys closure properties with respect to desirable function constructors, so to be able to derive sophisticated sound functions (and hence sophisticated proof techniques) from simpler ones. We consider both strong semantics (in which all actions are treated equally) and weak semantics (in which one abstracts from internal transitions). We test our enhancements on a few non-trivial examples.<\/jats:p>","DOI":"10.1145\/3498679","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["From enhanced coinduction towards enhanced induction"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5823-3235","authenticated-orcid":false,"given":"Davide","family":"Sangiorgi","sequence":"first","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/30.6.498"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003900"},{"key":"e_1_2_2_3_1","volume-title":"On generalised coinduction and probabilistic specification formats. Ph. D. Dissertation","author":"Bartels F.","unstructured":"F. Bartels . 2004. On generalised coinduction and probabilistic specification formats. Ph. D. Dissertation . CWI , Amsterdam . F. Bartels. 2004. On generalised coinduction and probabilistic specification formats. Ph. D. Dissertation. CWI, Amsterdam."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CALCO.2017.5"},{"key":"e_1_2_2_5_1","volume-title":"IFIP Formal Description of Programming Concepts \u2013 III","author":"Bergstra J.A.","unstructured":"J.A. Bergstra , J.W. Klop , and E.-R. Olderog . 1987. Failures without Chaos: a Process Semantics for Fair Abstraction . In IFIP Formal Description of Programming Concepts \u2013 III , M. Wirsing (Ed.). Elsevier Science Publishers B.V. , 77\u2013101. J.A. Bergstra, J.W. Klop, and E.-R. Olderog. 1987. Failures without Chaos: a Process Semantics for Fair Abstraction. In IFIP Formal Description of Programming Concepts \u2013 III, M. Wirsing (Ed.). Elsevier Science Publishers B.V., 77\u2013101."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200876"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209169"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_31"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.17"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0271-4"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429124"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1998-33401"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Stephen D. Brookes and A. W. Roscoe. 1984. An Improved Failures Model for Communicating Processes. In Seminar on Concurrency Stephen D. Brookes A. W. Roscoe and Glynn Winskel (Eds.) (Lecture Notes in Computer Science Vol. 197). Springer Verlag 281\u2013305.  Stephen D. Brookes and A. W. Roscoe. 1984. An Improved Failures Model for Communicating Processes. In Seminar on Concurrency Stephen D. Brookes A. W. Roscoe and Glynn Winskel (Eds.) (Lecture Notes in Computer Science Vol. 197). Springer Verlag 281\u2013305.","DOI":"10.1007\/3-540-15670-4_14"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211314"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.12.003"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(3:12)2019"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_26"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_6"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/b978-044482830-9\/50019-9"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90013-6"},{"key":"e_1_2_2_23_1","volume-title":"Algebraic Theory of Processes","author":"Hennessy M.","unstructured":"M. Hennessy . 1988. Algebraic Theory of Processes . The MIT Press , Cambridge, Mass .. M. Hennessy. 1988. Algebraic Theory of Processes. The MIT Press, Cambridge, Mass.."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63121-9_22"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_2_26_1","volume-title":"Ullman","author":"Hopcroft John E.","year":"2006","unstructured":"John E. Hopcroft , Rajeev Motwani , and Jeffrey D . Ullman . 2006 . Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley , Boston, MA, USA. isbn:0321455363 John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. 2006. Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley, Boston, MA, USA. isbn:0321455363"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.03.006"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80265-8"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80350-0"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(3:28)2013"},{"key":"e_1_2_2_32_1","volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"R. Milner . 1989. Communication and Concurrency . Prentice Hall . R. Milner. 1989. Communication and Concurrency. Prentice Hall."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268075"},{"key":"e_1_2_2_34_1","volume-title":"A New Equivalence notion for Communicating Systems","author":"Park D.","year":"1981","unstructured":"D. Park . 1981. A New Equivalence notion for Communicating Systems . In Bulletin EATCS, G. Maurer (Ed.). 14, 78\u201380. Abstract of the talk presented at the Second Workshop on the Semantics of Programming Languages, Bad Honnef, March 16\u201320 1981 . Abstracts collected in the Bulletin by B. Mayoh D. Park. 1981. A New Equivalence notion for Communicating Systems. In Bulletin EATCS, G. Maurer (Ed.). 14, 78\u201380. Abstract of the talk presented at the Second Workshop on the Semantics of Programming Languages, Bad Honnef, March 16\u201320 1981. Abstracts collected in the Bulletin by B. Mayoh"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(2:11)2016"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90117-4"},{"key":"e_1_2_2_37_1","volume-title":"12th ICALP","author":"Pnueli A.","unstructured":"A. Pnueli . 1985. Linear and Branching Structures in the Semantics and Logics of Reactive Systems . In 12th ICALP , W. Brauer (Ed.) (Lecture Notes in Computer Science, Vol . 194). Springer Verlag , 15\u201332. A. Pnueli. 1985. Linear and Branching Structures in the Semantics and Logics of Reactive Systems. In 12th ICALP, W. Brauer (Ed.) (Lecture Notes in Computer Science, Vol. 194). Springer Verlag, 15\u201332."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0016202"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_24"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934564"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_7"},{"key":"e_1_2_2_42_1","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pous Damien","unstructured":"Damien Pous and Davide Sangiorgi . 2012. Enhancements of the bisimulation proof method . In Advanced Topics in Bisimulation and Coinduction , Davide Sangiorgi and Jan Rutten (Eds.). Cambridge University Press . Damien Pous and Davide Sangiorgi. 2012. Enhancements of the bisimulation proof method. In Advanced Topics in Bisimulation and Coinduction, Davide Sangiorgi and Jan Rutten (Eds.). Cambridge University Press."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00497-w"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58027-1_25"},{"key":"e_1_2_2_45_1","volume-title":"The theory and practice of concurrency","author":"Roscoe A. W.","unstructured":"A. W. Roscoe . 1998. The theory and practice of concurrency . Prentice Hall . isbn:0-13-6774409-5 http:\/\/www.cs.ox.ac.uk\/people\/bill.roscoe\/publications\/68b.pdf A. W. Roscoe. 1998. The theory and practice of concurrency. Prentice Hall. isbn:0-13-6774409-5 http:\/\/www.cs.ox.ac.uk\/people\/bill.roscoe\/publications\/68b.pdf"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000523"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.11.009"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/321312.321326"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511777110"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2971339"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084781"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2010.272"},{"key":"e_1_2_2_54_1","volume-title":"Modal and temporal properties of processes","author":"Stirling Colin","unstructured":"Colin Stirling . 2001. Modal and temporal properties of processes . Springer Verlag . Colin Stirling. 2001. Modal and temporal properties of processes. Springer Verlag."},{"key":"e_1_2_2_55_1","first-page":"366","article-title":"Recursion Schemes from Comonads","volume":"8","author":"Uustalu Tarmo","year":"2001","unstructured":"Tarmo Uustalu , Varmo Vene , and Alberto Pardo . 2001 . Recursion Schemes from Comonads . Nord. J. Comput. , 8 , 3 (2001), 366 \u2013 390 . http:\/\/www.cs.helsinki.fi\/njc\/References\/uustaluvp2001:366.html Tarmo Uustalu, Varmo Vene, and Alberto Pardo. 2001. Recursion Schemes from Comonads. Nord. J. Comput., 8, 3 (2001), 366\u2013390. http:\/\/www.cs.helsinki.fi\/njc\/References\/uustaluvp2001:366.html","journal-title":"Nord. J. Comput."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498679","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498679","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498679"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498679"],"URL":"https:\/\/doi.org\/10.1145\/3498679","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}