{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T22:43:38Z","timestamp":1782859418186,"version":"3.54.5"},"reference-count":27,"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,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2026,9]]},"DOI":"10.1016\/j.tcs.2026.116124","type":"journal-article","created":{"date-parts":[[2026,6,23]],"date-time":"2026-06-23T16:12:51Z","timestamp":1782231171000},"page":"116124","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Translation of semi-extended regular expressions using linear forms"],"prefix":"10.1016","volume":"1083","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3263-7669","authenticated-orcid":false,"given":"Antoine","family":"Martin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9013-4413","authenticated-orcid":false,"given":"Etienne","family":"Renault","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6623-2512","authenticated-orcid":false,"given":"Alexandre","family":"Duret-Lutz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2026.116124_bib0001","series-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"10.1016\/j.tcs.2026.116124_bib0002","series-title":"Introduction to Runtime Verification","first-page":"1","author":"Bartocci","year":"2018"},{"key":"10.1016\/j.tcs.2026.116124_bib0003","series-title":"Dependable Software Systems Engineering","first-page":"72","article-title":"Synthesis of reactive systems","volume":"volume 45","author":"Finkbeiner","year":"2016"},{"key":"10.1016\/j.tcs.2026.116124_bib0004","article-title":"A Practical Introduction to PSL","author":"Eisner","year":"2006"},{"key":"10.1016\/j.tcs.2026.116124_bib0005","series-title":"1800\u20132017 - IEEE Standard for SystemVerilog\u2013Unified Hardware Design, Specification, and Verification Language","year":"2018"},{"key":"10.1016\/j.tcs.2026.116124_bib0006","series-title":"Proceedings of the 33rd International Joint Conference on Artificial Intelligence (IJCAI\u201913)","first-page":"854","article-title":"Linear temporal logic and linear dynamic logic on finite traces","author":"Giacomo","year":"2013"},{"issue":"2","key":"10.1016\/j.tcs.2026.116124_bib0007","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"Fischer","year":"1979","journal-title":"J. Comput. Syst. Sci."},{"key":"10.1016\/j.tcs.2026.116124_bib0008","series-title":"Proceedings of the 28th International Conference on Implementation and Applications of Automata (CIAA\u201924)","first-page":"234","article-title":"Translation of semi-extended regular expressions using derivatives","volume":"volume 15015","author":"Martin","year":"2024"},{"issue":"3","key":"10.1016\/j.tcs.2026.116124_bib0009","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/j.tcs.2026.116124_bib0010","series-title":"Proceedings of the 41st Annual Symposium on Principles of Programming Languages (POPL\u201914)","first-page":"541","article-title":"Minimization of symbolic automata","author":"D\u2019Antoni","year":"2014"},{"issue":"4","key":"10.1016\/j.tcs.2026.116124_bib0011","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1145\/321239.321249","article-title":"Derivatives of regular expressions","volume":"11","author":"Brzozowski","year":"1964","journal-title":"J. ACM"},{"issue":"2","key":"10.1016\/j.tcs.2026.116124_bib0012","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","article-title":"Partial derivatives of regular expressions and finite automaton constructions","volume":"155","author":"Antimirov","year":"1996","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.tcs.2026.116124_bib0013","series-title":"Language, Life, Limits \u2014 Proceedings of the 10th Conference on Computability in Europe (CiE\u201914)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-319-08019-2_8","article-title":"On the equivalence of automata for KAT-expressions","author":"Broda","year":"2014","ISBN":"https:\/\/id.crossref.org\/isbn\/9783319080192"},{"key":"10.1016\/j.tcs.2026.116124_bib0014","series-title":"Proceedings of the 20th International Conference on Implementation and Application of Automata (CIAA\u201915)","first-page":"49","article-title":"Deciding synchronous kleene algebra with derivatives","author":"Broda","year":"2015"},{"key":"10.1016\/j.tcs.2026.116124_bib0015","series-title":"Proceedings of the 29th International Conference on Implementation and Applications of Automata (CIAA\u201925)","first-page":"129","article-title":"Engineering an LTLf synthesis tool","volume":"volume 15981","author":"Duret-Lutz","year":"2025"},{"key":"10.1016\/j.tcs.2026.116124_bib0016","series-title":"Proceedings of the 5th International Conference on Language and Automata Theory and Applications (LATA\u201911)","first-page":"179","article-title":"Partial derivatives of an extended regular expression","author":"Caron","year":"2011"},{"key":"10.1016\/j.tcs.2026.116124_bib0017","series-title":"Proceedings of the 23rd International Conference on Implementation and Application of Automata (CIAA\u201918)","first-page":"248","article-title":"Two routes to automata minimization and the ways to reach it efficiently","volume":"vol. 10977","author":"Lombardy","year":"2018"},{"key":"10.1016\/j.tcs.2026.116124_bib0018","series-title":"Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI\u201921)","first-page":"6530","article-title":"On-the-fly synthesis for LTL over finite traces","volume":"volume 35","author":"Xiao","year":"2021"},{"key":"10.1016\/j.tcs.2026.116124_bib0019","series-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS\u201984)","first-page":"287","article-title":"Alg\u00e8bre de machines et logique temporelle","volume":"volume 166","author":"Michel","year":"1984"},{"issue":"1","key":"10.1016\/j.tcs.2026.116124_bib0020","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/0022-0000(87)90036-5","article-title":"Complementing deterministic B\u00fcchi automata in polynomial time","volume":"35","author":"Kurshan","year":"1987","journal-title":"J. Comput. Syst. Sci."},{"key":"10.1016\/j.tcs.2026.116124_bib0021","series-title":"Proceedings of the 19th International Symposium on Mathematical Foundations of Computer Science (MFCS\u201994)","first-page":"504","article-title":"On the minimization problem for \u03c9-automata","volume":"vol. 841","author":"Le Sa\u00ebc","year":"1994"},{"key":"10.1016\/j.tcs.2026.116124_bib0022","series-title":"Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201902)","article-title":"From states to transitions: improving translation of LTL formul\u00e6 to B\u00fcchi automata","volume":"vol. 2529","author":"Giannakopoulou","year":"2002"},{"key":"10.1016\/j.tcs.2026.116124_bib0023","series-title":"Parity and Generalized B\u00fcchi Automata \u2014 Determinisation and Complementation","author":"Varghese","year":"2014"},{"issue":"1\/2","key":"10.1016\/j.tcs.2026.116124_bib0024","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1504\/IJCCBS.2014.059594","article-title":"LTL translation improvements in spot 1.0","volume":"5","author":"Duret-Lutz","year":"2014","journal-title":"Int. J. Crit. Comput. Based Syst."},{"key":"10.1016\/j.tcs.2026.116124_bib0025","series-title":"Proceedings of the 34th International Conference on Computer Aided Verification (CAV\u201922)","article-title":"From spot 2.0 to spot 2.10: what\u2019s new?","volume":"vol. 13372","author":"Duret-Lutz","year":"2022"},{"key":"10.1016\/j.tcs.2026.116124_bib0026","series-title":"Technical Report","article-title":"\u201cProperty-by-Example\u201d Guide: A Handbook of PSL Examples","author":"Ben-David","year":"2005"},{"key":"10.1016\/j.tcs.2026.116124_bib0027","series-title":"Tools and Algorithms for the Construction and Analysis of Systems","first-page":"505","article-title":"Syntactic optimizations for PSL verification","author":"Cimatti","year":"2007"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397526003531?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397526003531?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,6,30]],"date-time":"2026-06-30T21:45:07Z","timestamp":1782855907000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397526003531"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,9]]},"references-count":27,"alternative-id":["S0304397526003531"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2026.116124","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2026,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Translation of semi-extended regular expressions using linear forms","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.tcs.2026.116124","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"116124"}}