{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:07:39Z","timestamp":1759032459233},"reference-count":22,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":4598,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1996,8]]},"abstract":"<jats:title>Summary<\/jats:title><jats:p>Since Pnueli\u2019s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, \u2018sound and complete\u2019 with respect to process specification and interconnection techniques.<\/jats:p>","DOI":"10.1017\/s0960129500001067","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T04:00:02Z","timestamp":1236139202000},"page":"353-373","source":"Crossref","is-referenced-by-count":17,"title":["Mirror, mirror in my hand: a duality between specifications and models of process behaviour"],"prefix":"10.1017","volume":"6","author":[{"given":"J. L.","family":"Fiadeiro","sequence":"first","affiliation":[]},{"given":"J. F.","family":"Costa","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500001067_ref003","volume-title":"Parallel Program Design - A Foundation","author":"Chandy","year":"1988"},{"key":"S0960129500001067_ref002","volume-title":"Temporal Logics and their Applications","author":"Barringer","year":"1987"},{"key":"S0960129500001067_ref006","unstructured":"Dionisio K. M. (1991) Um Modelo e Submodelos Categoriais de Processos Concorrentes, M.Sc. Thesis, Department of Mathematics, Faculty of Engineering, Technical University of Lisbon."},{"key":"S0960129500001067_ref004","unstructured":"Burstall R. and Goguen J. (1977) Putting Theories together to make Specifications. In: Reddy R. (ed.) Proc Fifth International Joint Conference on Artificial Intelligence 1045\u20131058."},{"key":"S0960129500001067_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12896-4_366"},{"key":"S0960129500001067_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55808-X_18"},{"key":"S0960129500001067_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0019445"},{"key":"S0960129500001067_ref008","unstructured":"Fiadeiro J. and Costa J. F. (1993) Mirror, Mirror in My Hand: a Topological Adjunction between Temporal Theories and Processes, Research Report, DI-FCUL."},{"key":"S0960129500001067_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0960129500001067_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0019447"},{"key":"S0960129500001067_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51803-7_23"},{"key":"S0960129500001067_ref020","first-page":"45","volume-title":"Proc 18th Annual Symposium on Foundations of Computer Science","author":"Pnueli","year":"1977"},{"key":"S0960129500001067_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BF01212304"},{"key":"S0960129500001067_ref015","volume-title":"Logics of Time and Computation","author":"Goldblatt","year":"1987"},{"key":"S0960129500001067_ref012","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56379-2_43"},{"key":"S0960129500001067_ref014","first-page":"257","volume-title":"Applied General Systems Research","author":"Goguen","year":"1978"},{"key":"S0960129500001067_ref001","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"S0960129500001067_ref017","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Manna","year":"1991"},{"key":"S0960129500001067_ref018","volume-title":"Logic Colloquium 87","author":"Meseguer","year":"1989"},{"key":"S0960129500001067_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014433"},{"key":"S0960129500001067_ref019","volume-title":"INRIA Advanced Nato Study Institute on Logics and Models for Verification and Specification of Concurrent Systems, Nice, France","author":"Misra","year":"1984"},{"key":"S0960129500001067_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_7"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500001067","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T16:50:27Z","timestamp":1557679827000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500001067\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,8]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1996,8]]}},"alternative-id":["S0960129500001067"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500001067","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,8]]}}}