{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:15:12Z","timestamp":1761610512209,"version":"build-2065373602"},"reference-count":52,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2005,4,23]],"date-time":"2005-04-23T00:00:00Z","timestamp":1114214400000},"content-version":"vor","delay-in-days":2669,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1998]]},"DOI":"10.1016\/s1571-0661(05)80591-2","type":"journal-article","created":{"date-parts":[[2005,4,24]],"date-time":"2005-04-24T07:16:06Z","timestamp":1114326966000},"page":"42-59","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":7,"title":["Specifying Real-Time Finite-State Systems in Linear Logic (Extended Abstract)"],"prefix":"10.1016","volume":"16","author":[{"given":"Max I.","family":"Kanovich","sequence":"first","affiliation":[]},{"given":"Mitsuhiro","family":"Okada","sequence":"additional","affiliation":[]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"5","key":"10.1016\/S1571-0661(05)80591-2_BIB1","doi-asserted-by":"crossref","first-page":"1543","DOI":"10.1145\/186025.186058","article-title":"An old-fashioned recipe for real time","volume":"16","author":"Abadi","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB2","series-title":"Real Time: Theory in Practice","first-page":"74","article-title":"Logics and models of real time: a survey","author":"Alur","year":"1992"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB3","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","year":"1993","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB4","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","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB5","series-title":"In Formal Methods for Real-Time Computing","first-page":"55","article-title":"Automata-theoretic verification of real-time systems","author":"Alur","year":"1996"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB6","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":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB7","unstructured":"N. Shankar. Mechanical verification of real-time systems using PVS. In C. Courcoubetis, editor, 5-th International Conference on Computer-Aided Verification. Springer LNCS 697, 1993. Expanded version available as a Technical Report SRI-CSL-92-12, November, 1992."},{"key":"10.1016\/S1571-0661(05)80591-2_BIB8","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(04)00044-1","article-title":"Specifying real-time systems in rewriting logic","volume":"4","author":"Olveczky","year":"1996","journal-title":"Electronic Notes in Theoretical Computer Science"},{"year":"1990","series-title":"Temporal Logic of Real-Time Systems","author":"Ostroff","key":"10.1016\/S1571-0661(05)80591-2_BIB9"},{"year":"1992","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","key":"10.1016\/S1571-0661(05)80591-2_BIB10"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB11","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"issue":"3","key":"10.1016\/S1571-0661(05)80591-2_BIB12","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lamport","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB13","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/0304-3975(94)00169-J","article-title":"A brief history of Timed CSP","volume":"138","author":"Davies","year":"1989","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB14","first-page":"401","article-title":"A temporal calculus of communicating systems","author":"Moller","year":"1990"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB15","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1006\/inco.1994.1083","article-title":"The algebra of timed processes ATP: Theory and application","volume":"114","author":"Nicollin","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB16","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1006\/inco.1995.1041","article-title":"A process algebra for timed systems","volume":"117","author":"Hennessy","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB17","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1006\/inco.1997.2657","article-title":"A complete axiomatization of finite-state ACSR processes","volume":"138","author":"Br\u00e9mond-Gr\u00e9goire","year":"1997","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB18","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","article-title":"The complementation problem for B\u00fcchi automata with applications to temporal logic","volume":"49","author":"Sistla","year":"1987","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"10.1016\/S1571-0661(05)80591-2_BIB19","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logics","volume":"32","author":"Sistla","year":"1985","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB21","series-title":"Advances in linear logic. London Mathematical Society Lecture Note Series","article-title":"Linear logic: its syntax and semantics","author":"Girard","year":"1995"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB22","series-title":"Current Trends in Theoretical Computer Science","first-page":"377","article-title":"A brief guide to linear logic","author":"Scedrov","year":"1993"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB23","series-title":"Proof and Computation, Proceedings Marktoberdorf Summer School 1993","first-page":"281","article-title":"Linear logic and computation: a survey","author":"Scedrov","year":"1994"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB24","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/0168-0072(94)90085-X","article-title":"The complexity of Horn fragments of linear logic","volume":"69","author":"Kanovich","year":"1994","journal-title":"Annals of Pure and Applied Logic"},{"issue":"3","key":"10.1016\/S1571-0661(05)80591-2_BIB25","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"Journal of Logic and Computation"},{"issue":"4","key":"10.1016\/S1571-0661(05)80591-2_BIB26","doi-asserted-by":"crossref","DOI":"10.1007\/BF03037301","article-title":"Static analysis of linear logic programming","volume":"15","author":"Andreoli","year":"1997","journal-title":"New Generation Computing"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB27","article-title":"Logic programming in intuitionistic linear logic: theory, design, and implementation","author":"Hodas","year":"1994","journal-title":"Dissertation, University of Pennsylvania"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB28","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1006\/inco.1994.1036","article-title":"Logic programming in a fragment of intuitionistic linear logic","volume":"110","author":"Hodas","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB29","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","article-title":"A multiple-conclusion specification logic","volume":"165","author":"Miller","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB30","article-title":"Concurrent linear logic programming","author":"Kobayashi","year":"1996","journal-title":"Dissertation, University of Tokyo"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB31","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/BF01211602","article-title":"Asynchronous communication model based on linear logic","volume":"7","author":"Kobayashi","year":"1995","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB32","first-page":"137","article-title":"Higher-order concurrent linear logic programming","volume":"907","author":"Kobayashi","year":"1995"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB33","series-title":"In Proc. 11-th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, NJ","first-page":"264","article-title":"A linear logical framework","author":"Cervesato","year":"1996"},{"key":"10.1016\/S1571-0661(05)80591-2_bib34","unstructured":"P. Fradet and D. Le M\u00e9tayer, Structured Gamma. Science of Computer Programming, to appear"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB35","unstructured":"C. Hankin, D. Le M\u00e9tayer, and D. Sands. Refining multiset transformers. Theoretical Computer Science, to appear."},{"key":"10.1016\/S1571-0661(05)80591-2_BIB36","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1142\/S0129054191000182","article-title":"From Petri nets to linear logic through categories: A survey","volume":"2","author":"Marti-Oliet","year":"1991","journal-title":"Internat. J. Foundations Comp. Sci."},{"key":"10.1016\/S1571-0661(05)80591-2_BIB37","article-title":"A logic for concurrency","author":"Asperti","year":"1987","journal-title":"Technical report, Dipartimento di Informatica, Universit\u00e1 di Pisa"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB38","series-title":"Proc. 10-th International Conference on Application and Theory of Petri Nets, Bonn","first-page":"174","article-title":"Nets as tensor theories","author":"Gunter","year":"1989"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB39","series-title":"In Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia","article-title":"Normal process representatives","author":"Gehlot","year":"1990"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB40","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1017\/S0960129500000062","article-title":"From Petri nets to linear logic","volume":"1","author":"Mart\u00ed-Oliet","year":"1991","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB41","series-title":"Proceedings of CAAP \u201990. Springer LNCS 431","article-title":"Petri nets as models of linear logic","author":"Engberg","year":"1990"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB42","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0168-0072(92)90075-B","article-title":"Decision problems for propositional linear logic","volume":"56","author":"Lincoln","year":"1992","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB43","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0304-3975(94)00108-1","article-title":"Constant-Only Multiplicative Linear Logic is NP-Complete","volume":"135","author":"Lincoln","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB44","series-title":"In Proc. 9-th Annual IEEE Symposium on Logic in Computer Science, Paris","first-page":"282","article-title":"Proof search in first order linear logic and other cut free sequent calculi","author":"Lincoln","year":"1994"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB45","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/0304-3975(94)00107-3","article-title":"First order linear logic without modalities is NEXPTIME-hard","volume":"135","author":"Lincoln","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB46","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","article-title":"The algorithmic analysis of hybrid systems","volume":"138","author":"Alur","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB47","series-title":"In Proc. 37-th IEEE Conference on Decision and Control","article-title":"Symbolic analysis of hybrid systems","author":"Alur","year":"1997"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB48","series-title":"In Proc. 13-th Annual IEEE Symposium on Logic in Computer Science, Indianapolis","article-title":"Phase semantics and verification of concurrent constraint programs","author":"Fages","year":"1998"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB49","article-title":"Encoding transition systems in sequent calculus: Preliminary report","volume":"3","author":"Miller","year":"1996","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB50","first-page":"133","article-title":"Effective calculi as a technique for search reduction","volume":"178","author":"Kanovich","year":"1987","journal-title":"American Mathematical Society Translations"},{"key":"10.1016\/S1571-0661(05)80591-2_BIB51","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0743-1066(90)90038-7","article-title":"Effective program synthesis in computational models","volume":"9","author":"Kanovich","year":"1990","journal-title":"Journal of Logic Programming"},{"journal-title":"The relational knowledge-base interpretation and feasible theorem-proving for intuitionistic propositional logic. University of Amsterdam, Institute for Logic, Language and Computation, ILLC Prepublication Series ML-","year":"1993","author":"Kanovich","key":"10.1016\/S1571-0661(05)80591-2_BIB52"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105805912?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105805912?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:08:42Z","timestamp":1761610122000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105805912"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"references-count":52,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998]]}},"alternative-id":["S1571066105805912"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80591-2","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Specifying Real-Time Finite-State Systems in Linear Logic (Extended Abstract)","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)80591-2","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1998 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}