{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,13]],"date-time":"2026-08-13T03:28:49Z","timestamp":1786591729362,"version":"3.56.0"},"reference-count":31,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T00:00:00Z","timestamp":1780617600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100018693","name":"HORIZON EUROPE Framework Programme","doi-asserted-by":"publisher","award":["101214553"],"award-info":[{"award-number":["101214553"]}],"id":[{"id":"10.13039\/100018693","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100011757","name":"SNS Nordic Forest Research","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100011757","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100009473","name":"University of Malaga","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100009473","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Logical and Algebraic Methods in Programming"],"published-print":{"date-parts":[[2026,9]]},"DOI":"10.1016\/j.jlamp.2026.101142","type":"journal-article","created":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T06:41:49Z","timestamp":1780728109000},"page":"101142","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Towards a formal digital twin of the PTP protocol using automata learning"],"prefix":"10.1016","volume":"151","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3825-196X","authenticated-orcid":false,"given":"Rafael","family":"L\u00f3pez-G\u00f3mez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4310-4729","authenticated-orcid":false,"given":"Delia","family":"Rico","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6399-6162","authenticated-orcid":false,"given":"Laura","family":"Panizo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3481-5307","authenticated-orcid":false,"given":"Mar\u00eda-del-Mar","family":"Gallardo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.jlamp.2026.101142_bib0001","series-title":"Framework and overall objectives of the future development of IMT for 2030 and beyond","year":"2023"},{"key":"10.1016\/j.jlamp.2026.101142_bib0002","first-page":"1","article-title":"IEEE Standard for a precision clock synchronization protocol for networked measurement and control systems","author":"Group","year":"2020","journal-title":"IEEE Std 1588\u20142019"},{"issue":"4","key":"10.1016\/j.jlamp.2026.101142_bib0003","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1049\/cps2.12088","article-title":"A petri net model for time-delay attack detection in precision time protocol-based networks","volume":"9","author":"Moradi","year":"2024","journal-title":"IET Cyber-Phys. Syst.: Theory Appl."},{"key":"10.1016\/j.jlamp.2026.101142_bib0004","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1186\/s42400-021-00080-y","article-title":"Precision time protocol attack strategies and their resistance to existing security extensions","volume":"4","author":"Alghamdi","year":"2021","journal-title":"Cybersecurity"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101142_bib0005","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1109\/TDSC.2017.2748583","article-title":"A security analysis and revised security extension for the precision time protocol","volume":"17","author":"Itkin","year":"2020","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"10.1016\/j.jlamp.2026.101142_bib0006","series-title":"2016 International Conference on Information Science and Communications Technologies (ICISCT)","first-page":"1","article-title":"A timed colored petri-net modeling for precision time protocol","author":"Igorevich","year":"2016"},{"key":"10.1016\/j.jlamp.2026.101142_bib0007","series-title":"2019 IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC)","first-page":"531","article-title":"A discrete model of IEEE 1588\u20132008 precision time protocol with clock servo using PI controller","volume":"2","author":"Maegawa","year":"2019"},{"key":"10.1016\/j.jlamp.2026.101142_bib0008","unstructured":"M. L\u00e9vesque, D. Tipper, PTP++: a precision time protocol simulation model for OMNeT++\/INET, (2015). 10.48550\/arXiv.1509.03169."},{"key":"10.1016\/j.jlamp.2026.101142_bib0009","doi-asserted-by":"crossref","unstructured":"B.K. Aichernig, E. Mu\u0161kardin, A. Pferscher, Active vs. passive: a comparison of automata learning paradigms for network protocols, arXiv preprint arXiv: 2209.14031(2022).","DOI":"10.4204\/EPTCS.371.1"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101142_bib0010","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3605360","article-title":"Benchmarking combinations of learning and testing algorithms for automata learning","volume":"36","author":"Aichernig","year":"2024","journal-title":"Form. Asp. Comput."},{"key":"10.1016\/j.jlamp.2026.101142_bib0011","series-title":"International Workshop on Automated Verification of Critical Systems","first-page":"185","article-title":"Learning-based testing the sliding window behavior of TCP implementations","author":"Fiter\u0103u-Bro\u015ftean","year":"2017"},{"key":"10.1016\/j.jlamp.2026.101142_bib0012","series-title":"2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)","first-page":"276","article-title":"Model-based testing IoT communication via active automata learning","author":"Tappler","year":"2017"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101142_bib0013","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10703-023-00425-y","article-title":"Fingerprinting and analysis of bluetooth devices with automata learning","volume":"61","author":"Pferscher","year":"2022","journal-title":"Form. Methods Syst. Des."},{"issue":"1","key":"10.1016\/j.jlamp.2026.101142_bib0014","article-title":"Model-based grey-box fuzzing of network protocols","volume":"2022","author":"Pan","year":"2022","journal-title":"Secur. Commun. Netw."},{"key":"10.1016\/j.jlamp.2026.101142_bib0015","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","article-title":"A tutorial on uppaal","author":"Behrmann","year":"2004","journal-title":"Form. Methods Des. Real-time Syst."},{"key":"10.1016\/j.jlamp.2026.101142_bib0016","unstructured":"L.P. Project, ptp4l Manual, 2025. https:\/\/linux.die.net\/man\/8\/ptp4l."},{"issue":"4","key":"10.1016\/j.jlamp.2026.101142_bib0017","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","article-title":"Uppaal SMC tutorial","volume":"17","author":"David","year":"2015","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.jlamp.2026.101142_bib0018","series-title":"Grammatical Inference: Theoretical Results and Applications (ICGI 2010)","first-page":"203","article-title":"A likelihood-ratio test for identifying probabilistic deterministic real-time automata from positive data","volume":"Vol. 6339","author":"Verwer","year":"2010"},{"key":"10.1016\/j.jlamp.2026.101142_bib0019","series-title":"36th AAAI Conf. on Artificial Intelligence","first-page":"3949","article-title":"TAG: learning timed automata from logs","author":"Cornanguer","year":"2022"},{"issue":"6","key":"10.1016\/j.jlamp.2026.101142_bib0020","doi-asserted-by":"crossref","first-page":"592","DOI":"10.1109\/TC.1972.5009015","article-title":"On the synthesis of finite-state machines from samples of their behavior","volume":"C-21","author":"Biermann","year":"1972","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/j.jlamp.2026.101142_bib0021","series-title":"10th IEEE International Conference on Software Testing, Verification and Validation (ICST)","first-page":"401","article-title":"Timed k-tail: automatic inference of timed automata","author":"Pastore","year":"2017"},{"key":"10.1016\/j.jlamp.2026.101142_bib0022","series-title":"Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004","first-page":"200","article-title":"A tutorial on uppaal","author":"Behrmann","year":"2004"},{"issue":"22","key":"10.1016\/j.jlamp.2026.101142_bib0023","article-title":"A modular experimentation methodology for 5G deployments: the 5GENESIS approach","volume":"20","author":"D\u00e1az Zayas","year":"2020","journal-title":"Sensors"},{"key":"10.1016\/j.jlamp.2026.101142_bib0024","unstructured":"Linuxptp project changelogs, 2024, https:\/\/www.rpmfind.net\/linux\/RPM\/opensuse\/16.0\/ppc64le\/linuxptp-4.4-160000.2.2.ppc64le.html."},{"key":"10.1016\/j.jlamp.2026.101142_bib0025","unstructured":"E.U.o. T. AIS Group, CPN tools, 2025, https:\/\/cpntools.org."},{"key":"10.1016\/j.jlamp.2026.101142_bib0026","series-title":"24th USENIX Security Symposium (USENIX Security 15)","first-page":"193","article-title":"Protocol state fuzzing of {TLS} implementations","author":"De Ruiter","year":"2015"},{"issue":"2","key":"10.1016\/j.jlamp.2026.101142_bib0027","doi-asserted-by":"crossref","first-page":"790","DOI":"10.1109\/TITS.2018.2823418","article-title":"MOHA: a multi-mode hybrid automaton model for learning car-following behaviors","volume":"20","author":"Lin","year":"2019","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"10.1016\/j.jlamp.2026.101142_bib0028","article-title":"A novel anomaly detection algorithm for hybrid production systems based on deep learning and timed automata","volume":"abs\/2010.15415","author":"Hranisavljevic","year":"2020","journal-title":"CoRR"},{"key":"10.1016\/j.jlamp.2026.101142_bib0029","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/978-3-662-57805-6_3","article-title":"Enable learning of hybrid timed automata in absence of discrete events through self-organizing maps","author":"von Birgelen","year":"2018","journal-title":"IMPROVE-Innov. Model. Approaches Prod. Syst. Raise Validatable Effic.: Intell. Methods Fact. Future"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101142_bib0030","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","article-title":"The benefits of relaxing punctuality","volume":"43","author":"Alur","year":"1996","journal-title":"J. ACM"},{"key":"10.1016\/j.jlamp.2026.101142_bib0031","series-title":"Runtime Verification: Third International Conference, RV 2012, Istanbul, Turkey, September 25\u201328, 2012, Revised Selected Papers 3","first-page":"260","article-title":"Rewrite-based statistical model checking of WMTL","author":"Bulychev","year":"2013"}],"container-title":["Journal of Logical and Algebraic Methods in Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000349?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000349?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,8,13]],"date-time":"2026-08-13T02:55:10Z","timestamp":1786589710000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2352220826000349"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,9]]},"references-count":31,"alternative-id":["S2352220826000349"],"URL":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101142","relation":{},"ISSN":["2352-2208"],"issn-type":[{"value":"2352-2208","type":"print"}],"subject":[],"published":{"date-parts":[[2026,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Towards a formal digital twin of the PTP protocol using automata learning","name":"articletitle","label":"Article Title"},{"value":"Journal of Logical and Algebraic Methods in Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101142","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Author(s). Published by Elsevier Inc.","name":"copyright","label":"Copyright"}],"article-number":"101142"}}