{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:02:30Z","timestamp":1750309350313,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,6,26]],"date-time":"2024-06-26T00:00:00Z","timestamp":1719360000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Youth Project of National Science Foundation of China","award":["62102329"],"award-info":[{"award-number":["62102329"]}]},{"name":"the Project of National Science Foundation of Chongqing","award":["cstc2021jcyj-bshX0120"],"award-info":[{"award-number":["cstc2021jcyj-bshX0120"]}]},{"name":"Capacity Development Grant of Southwest University","award":["SWU116007"],"award-info":[{"award-number":["SWU116007"]}]},{"name":"Project of National Science Foundation of China","award":["62272397"],"award-info":[{"award-number":["62272397"]}]},{"name":"Key Projects of National Science Foundation of China","award":["61732019 and 62032019"],"award-info":[{"award-number":["61732019 and 62032019"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2024,6,30]]},"abstract":"\n The polychronous or multi-clock paradigm is adequate to model large distributed systems where achieving a full timed synchronization is not only very costly but also often not necessary. It concerns systems made of a set of components with loose synchronization constraints. We study an approach where those components are orchestrated using\n logical clocks<\/jats:italic>\n , made popular by L. Lamport and synchronous languages. The temporal and causal specification of those systems is built by defining a set of\n clock relations<\/jats:italic>\n that would constrain the instant when clocks can tick or must not tick, thus defining families of\n valid schedules<\/jats:italic>\n . In this article, we propose a specification language, called\n \n \\(\\mathit {LTL}_c\/\\mathit {CCSL}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , for specifying temporal properties of multi-clock systems. While traditional temporal logics (LTL, MTL, CTL*), whether linear or branching, rely on a global step, our language,\n \n \\(\\mathit {LTL}_c\/\\mathit {CCSL}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , builds a partial order on logical clocks, thus allowing both a hierarchical approach based on refinement of clock hierarchies and compositionality, as what happens in one clock domain may remain largely independent of what may happen in other domains. This good property helps preserve the properties without requiring to perform the proofs again. An\n \n \\(\\mathit {LTL}_c\/\\mathit {CCSL}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n specification consists of a clock temporal logic\n \n \\(\\mathit {LTL}_c\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , accompanied by a clock calculus called\n CCSL<\/jats:italic>\n for specifying clock relations. We build the syntax and semantics of\n \n \\(\\mathit {LTL}_c\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n and link its semantics with CCSL. After that, we mainly focus on the verification aspect of\n \n \\(\\mathit {LTL}_c\/\\mathit {CCSL}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n specifications using a model checking technique. We show how\n \n \\(\\mathit {LTL}_c\/\\mathit {CCSL}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n can be used for specifying multi-clock systems with an example.\n <\/jats:p>\n ","DOI":"10.1145\/3670794","type":"journal-article","created":{"date-parts":[[2024,6,8]],"date-time":"2024-06-08T10:33:57Z","timestamp":1717842837000},"page":"1-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Specification and Verification of Multi-Clock Systems Using a Temporal Logic with Clock Constraints"],"prefix":"10.1145","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0685-6905","authenticated-orcid":false,"given":"Yuanrui","family":"Zhang","sequence":"first","affiliation":[{"name":"College of Computer Science and Technology\/College of Software, Nanjing University of Aeronautics and Astronautics, Nanjing, China and Southwest University, Chongqing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9088-9821","authenticated-orcid":false,"given":"Frederic","family":"Mallet","sequence":"additional","affiliation":[{"name":"Universite Cote d'Azur, Nice, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1938-2902","authenticated-orcid":false,"given":"Min","family":"Zhang","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9771-3071","authenticated-orcid":false,"given":"Zhiming","family":"Liu","sequence":"additional","affiliation":[{"name":"Northwest University, Xi'an, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,26]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"MathWorks. n.d. Simulink. Retrieved June 10 2024 from https:\/\/www.mathworks.com\/products\/simulink.html"},{"key":"e_1_3_3_3_2","unstructured":"Polychrony. n.d. The Polychrony Toolset. Retrieved June 10 2024 from http:\/\/www.irisa.fr\/espresso\/Polychrony"},{"key":"e_1_3_3_4_2","article-title":"IEEE Standard for Property Specification Language (PSL) - Redline","author":"IEEE","unstructured":"IEEE. 2010. IEEE Standard for Property Specification Language (PSL) - Redline. IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005) - Redline. IEEE.","journal-title":"IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005) - Redline."},{"issue":"2","key":"e_1_3_3_5_2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur Rajeev","year":"1994","unstructured":"Rajeev Alur and David L. Dill. 1994. A theory of timed automata. Theoretical Computer Science 126, 2 (1994), 183\u2013235.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"e_1_3_3_6_2","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","article-title":"The benefits of relaxing punctuality","volume":"43","author":"Alur Rajeev","year":"1996","unstructured":"Rajeev Alur, Tom\u00e1s Feder, and Thomas A. Henzinger. 1996. The benefits of relaxing punctuality. Journal of the ACM 43, 1 (Jan.1996), 116\u2013146.","journal-title":"Journal of the ACM"},{"issue":"1","key":"e_1_3_3_7_2","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1993.1025","article-title":"Real-time logics: Complexity and expressiveness","volume":"104","author":"Alur R.","year":"1993","unstructured":"R. Alur and T. A. Henzinger. 1993. Real-time logics: Complexity and expressiveness. Information and Computation 104, 1 (1993), 35\u201377.","journal-title":"Information and Computation"},{"key":"e_1_3_3_8_2","volume-title":"Syntax and Semantics of the Clock Constraint Specification Language (CCSL)","author":"Andr\u00e9 Charles","year":"2009","unstructured":"Charles Andr\u00e9. 2009. Syntax and Semantics of the Clock Constraint Specification Language (CCSL). Research Report RR-6925. INRIA."},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1007\/978-3-540-75209-7_38","volume-title":"Model Driven Engineering Languages and Systems","author":"Andr\u00e9 Charles","year":"2007","unstructured":"Charles Andr\u00e9, Fr\u00e9d\u00e9ric Mallet, and Robert de Simone. 2007. Modeling time(s). In Model Driven Engineering Languages and Systems, Gregor Engels, Bill Opdyke, Douglas C. Schmidt, and Frank Weil (Eds.). Springer, Berlin, Germany, 559\u2013573."},{"issue":"7","key":"e_1_3_3_10_2","first-page":"97","article-title":"That \u201cInternet of Things\u201d thing","volume":"22","author":"Ashton K.","year":"2009","unstructured":"K. Ashton. 2009. That \u201cInternet of Things\u201d thing. RFID Journal 22, 7 (July2009), 97\u2013114.","journal-title":"RFID Journal"},{"key":"e_1_3_3_11_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost P. Katoen. 2008. Principles of Model Checking. MIT Press."},{"issue":"2","key":"e_1_3_3_12_2","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","article-title":"Synchronous programming with events and relations: The SIGNAL language and its semantics","volume":"16","author":"Benveniste Albert","year":"1991","unstructured":"Albert Benveniste, Paul Le Guernic, and Christian Jacquemot. 1991. Synchronous programming with events and relations: The SIGNAL language and its semantics. Science of Computer Programming 16, 2 (1991), 103\u2013149.","journal-title":"Science of Computer Programming"},{"issue":"2","key":"e_1_3_3_13_2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","article-title":"The Esterel synchronous programming language: Design, semantics, implementation","volume":"19","author":"Berry G\u00e9rard","year":"1992","unstructured":"G\u00e9rard Berry and Georges Gonthier. 1992. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming 19, 2 (1992), 87\u2013152.","journal-title":"Science of Computer Programming"},{"key":"e_1_3_3_14_2","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/978-3-642-29645-1_12","volume-title":"Models in Software Engineering","author":"Boulanger Fr\u00e9d\u00e9ric","year":"2012","unstructured":"Fr\u00e9d\u00e9ric Boulanger, Ayman Dogui, C\u00e9cile Hardebolle, Christophe Jacquet, Dominique Marcadet, and Iuliana Prodan. 2012. Semantic adaptation using CCSL clock constraints. In Models in Software Engineering, J\u00f6rg Kienzle (Ed.). Springer, Berlin, Germany, 104\u2013118."},{"key":"e_1_3_3_15_2","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/j.ic.2014.01.012","article-title":"STL*: Extending signal temporal logic with signal-value freezing operator","volume":"236","author":"Brim L.","year":"2014","unstructured":"L. Brim, P. Dluho\u0161, D. \u0160afr\u00e1nek, and T. Vejpustek. 2014. STL*: Extending signal temporal logic with signal-value freezing operator. Information and Computation 236 (2014), 52\u201367.","journal-title":"Information and Computation"},{"key":"e_1_3_3_16_2","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1145\/41625.41641","volume-title":"Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","author":"Caspi P.","year":"1987","unstructured":"P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. 1987. LUSTRE: A declarative language for real-time programming. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages(POPL\u201987). ACM, New York, NY, USA, 178\u2013188."},{"key":"e_1_3_3_17_2","series-title":"Lecture Notes in Computer Science","volume-title":"AllAbout Maude\u2014A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic","author":"Clavel Manuel","year":"2007","unstructured":"Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jose Meseguer, and Carolyn Talcott. 2007. AllAbout Maude\u2014A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. Lecture Notes in Computer Science, Vol. 4350. Springer."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","unstructured":"Jean-Louis Cola\u00e7o Bruno Pagano and Marc Pouzet. 2017. SCADE 6: A formal language for embedded critical software development (invited paper). In Proceedings of the 2017 11th International Symposium on Theoretical Aspects of Software Engineering (TASE\u201917). IEEE 1\u201311. 10.1109\/TASE.2017.8285623","DOI":"10.1109\/TASE.2017.8285623"},{"key":"e_1_3_3_19_2","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-33386-6_9","volume-title":"Automated Technology for Verification and Analysis","author":"Donz\u00e9 Alexandre","year":"2012","unstructured":"Alexandre Donz\u00e9, Oded Maler, Ezio Bartocci, Dejan Nickovic, Radu Grosu, and Scott Smolka. 2012. On temporal logic and signal processing. In Automated Technology for Verification and Analysis, Supratik Chakraborty and Madhavan Mukund (Eds.). Springer, Berlin, Germany, 92\u2013106."},{"key":"e_1_3_3_20_2","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1007\/3-540-45061-0_67","volume-title":"Automata, Languages and Programming","author":"Eisner Cindy","year":"2003","unstructured":"Cindy Eisner, Dana Fisman, John Havlicek, Anthony McIsaac, and David Van Campenhout. 2003. The definition of a temporal clock operator. In Automata, Languages and Programming, Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger (Eds.). Springer, Berlin, Germany, 857\u2013870."},{"issue":"2","key":"e_1_3_3_21_2","doi-asserted-by":"crossref","first-page":"9\u2013es","DOI":"10.1145\/1217295.1217298","article-title":"Polychronous design of embedded real-time applications","volume":"16","author":"Gamati\u00e9 Abdoulaye","year":"2007","unstructured":"Abdoulaye Gamati\u00e9, Thierry Gautier, Paul Le Guernic, and Jean-Pierre Talpin. 2007. Polychronous design of embedded real-time applications. ACM Transactions on Software Engineering and Methodology 16, 2 (2007), 9\u2013es.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"e_1_3_3_22_2","first-page":"141","volume-title":"Proceedings of the 2011 18th International Symposium on Temporal Representation and Reasoning","author":"Gascon R.","year":"2011","unstructured":"R. Gascon, F. Mallet, and J. Deantoni. 2011. Logical time and temporal logics: Comparing UML MARTE\/CCSL and PSL. In Proceedings of the 2011 18th International Symposium on Temporal Representation and Reasoning. 141\u2013148."},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-012-9093-y"},{"key":"e_1_3_3_24_2","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-45449-7_12","volume-title":"Embedded Software","author":"Henzinger Thomas A.","year":"2001","unstructured":"Thomas A. Henzinger, Benjamin Horowitz, and Christoph Meyer Kirsch. 2001. Giotto: A time-triggered language for embedded programming. In Embedded Software, Thomas A. Henzinger and Christoph M. Kirsch (Eds.). Springer, Berlin, Germany, 166\u2013184."},{"issue":"5","key":"e_1_3_3_25_2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzmann Gerard J.","year":"1997","unstructured":"Gerard J. Holzmann. 1997. The model checker SPIN. IEEE Transactions on Software Engineering 23, 5 (May1997), 279\u2013295.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_3_3_26_2","volume-title":"Proceedings of the 56th Annual Design Automation Conference 2019","author":"Hu Ming","year":"2019","unstructured":"Ming Hu, Tongquan Wei, Min Zhang, Fr\u00e9d\u00e9ric Mallet, and Mingsong Chen. 2019. Sample-guided automated synthesis for CCSL specifications. In Proceedings of the 56th Annual Design Automation Conference 2019(DAC\u201919). ACM, New York, NY, USA, Article 98, 6 pages. 10.1145\/3316781.3317904"},{"issue":"7","key":"e_1_3_3_27_2","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1145\/359545.359563","article-title":"Time, clocks, and the ordering of events in a distributed system","volume":"21","author":"Lamport Leslie","year":"1978","unstructured":"Leslie Lamport. 1978. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21, 7 (July1978), 558\u2013565.","journal-title":"Communications of the ACM"},{"issue":"3","key":"e_1_3_3_28_2","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1142\/S0218126603000763","article-title":"POLYCHRONY for system design","volume":"12","author":"Guernic Paul Le","year":"2003","unstructured":"Paul Le Guernic, Jean-Pierre Talpin, and Jean-Christophe Le Lann. 2003. POLYCHRONY for system design. Journal of Circuits, Systems and Computers 12, 3 (2003), 261\u2013303.","journal-title":"Journal of Circuits, Systems and Computers"},{"key":"e_1_3_3_29_2","first-page":"363","volume-title":"Proceedings of the 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC\u201908)","author":"Lee E. A.","year":"2008","unstructured":"E. A. Lee. 2008. Cyber physical systems: Design Challenges. In Proceedings of the 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC\u201908). 363\u2013369."},{"key":"e_1_3_3_30_2","first-page":"213","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"Lee Edward A.","year":"2021","unstructured":"Edward A. Lee and Marten Lohstroh. 2021. Time for all programs, not just real-time programs. In Leveraging Applications of Formal Methods, Verification and Validation, Tiziana Margaria and Bernhard Steffen (Eds.). Springer International Publishing, Cham, Switzerland, 213\u2013232."},{"issue":"12","key":"e_1_3_3_31_2","doi-asserted-by":"crossref","first-page":"1217","DOI":"10.1109\/43.736561","article-title":"A framework for comparing models of computation","volume":"17","author":"Lee Edward A.","year":"1998","unstructured":"Edward A. Lee and Alberto L. Sangiovanni-Vincentelli. 1998. A framework for comparing models of computation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 17, 12 (1998), 1217\u20131229.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"e_1_3_3_32_2","volume-title":"Introduction to Embedded Systems: A Cyber-Physical Systems Approach","author":"Lee Edward A.","year":"2011","unstructured":"Edward A. Lee and Sanjit A. Seshia. 2011. Introduction to Embedded Systems: A Cyber-Physical Systems Approach. MIT Press."},{"issue":"5","key":"e_1_3_3_33_2","first-page":"699","article-title":"Dealing with multiple granularity of time in temporal logic programming","volume":"22","author":"Liu Chuchang","year":"1996","unstructured":"Chuchang Liu and Mehmet A. Orgun. 1996. Dealing with multiple granularity of time in temporal logic programming. Journal of Symbolic Computation 22, 5-6 (1996), 699\u2013720.","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"e_1_3_3_34_2","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1016\/S0304-3975(99)00008-0","article-title":"Verification of reactive systems using temporal logic with clocks","volume":"220","author":"Liu Chuchang","year":"1999","unstructured":"Chuchang Liu and Mehmet A. Orgun. 1999. Verification of reactive systems using temporal logic with clocks. Theoretical Computer Science 220, 2 (June 1999), 377\u2013408.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_3_35_2","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"Maler Oded","year":"2004","unstructured":"Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Yassine Lakhnech and Sergio Yovine (Eds.). Springer, Berlin, Germany, 152\u2013166."},{"issue":"3","key":"e_1_3_3_36_2","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/s11334-008-0055-2","article-title":"Clock constraint specification language: Specifying clock constraints with UML\/MARTE","volume":"4","author":"Mallet Fr\u00e9d\u00e9ric","year":"2008","unstructured":"Fr\u00e9d\u00e9ric Mallet. 2008. Clock constraint specification language: Specifying clock constraints with UML\/MARTE. Innovations in Systems and Software Engineering 4, 3 (2008), 309\u2013314.","journal-title":"Innovations in Systems and Software Engineering"},{"key":"e_1_3_3_37_2","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1016\/j.scico.2015.03.001","article-title":"Correctness issues on MARTE\/CCSL constraints","volume":"106","author":"Mallet Fr\u00e9d\u00e9ric","year":"2015","unstructured":"Fr\u00e9d\u00e9ric Mallet and Robert de Simone. 2015. Correctness issues on MARTE\/CCSL constraints. Science of Computer Programming 106 (2015), 78\u201392.","journal-title":"Science of Computer Programming"},{"key":"e_1_3_3_38_2","unstructured":"Fr\u00e9d\u00e9ric Mallet Jean-Vivien Millo and Robert de Simone. 2013. Safe CCSL specifications and marked graphs. In Proceedings of the 2013 11th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMCODE\u201913). IEEE 157\u2013166."},{"volume-title":"UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems","year":"2011","key":"e_1_3_3_39_2","unstructured":"OMG. 2011. UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems. Technical Report. OMG."},{"key":"e_1_3_3_40_2","volume-title":"System Design, Modeling, and Simulation Using Ptolemy II","author":"Ptolemaeus Claudius","year":"2014","unstructured":"Claudius Ptolemaeus (Ed.). 2014. System Design, Modeling, and Simulation Using Ptolemy II. Ptolemy.org."},{"key":"e_1_3_3_41_2","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1145\/3078633.3081035","volume-title":"Proceedings of the 18th ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems","author":"Zhang Min","year":"2017","unstructured":"Min Zhang and Yunhui Ying. 2017. Towards SMT-based LTL model checking of clock constraint specification language for real-time and embedded systems. In Proceedings of the 18th ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems(LCTES\u201917). ACM, New York, NY, USA, 61\u201370. 10.1145\/3078633.3081035"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102591"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670794","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3670794","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:41Z","timestamp":1750291541000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670794"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,26]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6,30]]}},"alternative-id":["10.1145\/3670794"],"URL":"https:\/\/doi.org\/10.1145\/3670794","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2024,6,26]]},"assertion":[{"value":"2022-07-24","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-23","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}