乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,8]],"date-time":"2024-04-08T07:08:56Z","timestamp":1712560136447},"reference-count":55,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2012,2,28]],"date-time":"2012-02-28T00:00:00Z","timestamp":1330387200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2012,4]]},"abstract":"The concurrency theory literature offers a wealth of examples of characteristic-formula constructions for various behavioural relations over finite labelled transition systems and Kripke structures that are defined in terms of fixed points of suitable functions. Such constructions and their proofs of correctness have been developed independently, but have a common underlying structure. This paper provides a general view of characteristic formulae that are expressed in terms of logics that have a facility for the recursive definition of formulae. We show how several examples of characteristic-formula constructions in the literature can be recovered as instances of the proposed general framework, and how the framework can be used to yield novel constructions. The paper also offers general results pertaining to the definition of co-characteristic formulae and of characteristic formulae expressed in terms of infinitary modal logics.<\/jats:p>","DOI":"10.1017\/s0960129511000375","type":"journal-article","created":{"date-parts":[[2012,2,28]],"date-time":"2012-02-28T12:01:44Z","timestamp":1330430504000},"page":"125-173","source":"Crossref","is-referenced-by-count":12,"title":["Characteristic formulae for fixed-point semantics: a general framework"],"prefix":"10.1017","volume":"22","author":[{"given":"LUCA","family":"ACETO","sequence":"first","affiliation":[]},{"given":"ANNA","family":"INGOLFSDOTTIR","sequence":"additional","affiliation":[]},{"given":"PAUL BLAIN","family":"LEVY","sequence":"additional","affiliation":[]},{"given":"JOSHUA","family":"SACK","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2012,2,28]]},"reference":[{"key":"S0960129511000375_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084809"},{"key":"S0960129511000375_ref48","first-page":"46","volume-title":"Proceedings 18th Annual Symposium on Foundations of Computer Science","author":"Pnueli","year":"1997"},{"key":"S0960129511000375_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46691-6_31"},{"key":"S0960129511000375_ref55","first-page":"148","volume-title":"Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science","author":"Ulidowski","year":"1992"},{"key":"S0960129511000375_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"S0960129511000375_ref51","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90012-0"},{"key":"S0960129511000375_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2355-7"},{"key":"S0960129511000375_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"S0960129511000375_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"S0960129511000375_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039617"},{"key":"S0960129511000375_ref47","unstructured":"Plotkin G. D. (2004) A structural approach to operational semantics. Journal of Logic and Algebraic Programming (60-61) 17\u2013139."},{"key":"S0960129511000375_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.11.031"},{"key":"S0960129511000375_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55179-4_3"},{"key":"S0960129511000375_ref16","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005245900406"},{"key":"S0960129511000375_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/233551.233556"},{"key":"S0960129511000375_ref37","doi-asserted-by":"crossref","unstructured":"Lassen S. B. (1998) Relational Reasoning about Functions and Nondeterminism, Ph.D. thesis, University of Aarhus.","DOI":"10.7146\/brics.v4i24.18950"},{"key":"S0960129511000375_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90276-L"},{"key":"S0960129511000375_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200876"},{"key":"S0960129511000375_ref50","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1028"},{"key":"S0960129511000375_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482830-9\/50019-9"},{"key":"S0960129511000375_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60246-1_158"},{"key":"S0960129511000375_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/201019.201032"},{"key":"S0960129511000375_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"S0960129511000375_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90038-J"},{"key":"S0960129511000375_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017309"},{"key":"S0960129511000375_ref19","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, Vol. B","author":"Emerson","year":"1990"},{"key":"S0960129511000375_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80031-6"},{"key":"S0960129511000375_ref54","unstructured":"Thomsen B. (1987) An extended bisimulation induced by a preorder on actions. Master's thesis, Aalborg University Centre."},{"key":"S0960129511000375_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54233-7_129"},{"key":"S0960129511000375_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56610-4_89"},{"key":"S0960129511000375_ref46","unstructured":"Pitcher C. (2001) Functional Programming and Erratic Non-Determinism, Ph.D. thesis, Oxford University."},{"key":"S0960129511000375_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814105"},{"key":"S0960129511000375_ref42","unstructured":"Moran A. K. (1998) Call-by-name, Call-by-need, and McCarthy's Amb, Ph.D. thesis, Department of Computing Science, Chalmers University of Technology and University of Gothenburg, Gothenburg, Sweden."},{"key":"S0960129511000375_ref17","first-page":"226","article-title":"Operational and epistemic approaches to protocol anlaysis: Bridging the gap. In: Proceedings of the 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'07)","volume":"4790","author":"Dechesne","year":"2007","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129511000375_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147527"},{"key":"S0960129511000375_ref10","volume-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"S0960129511000375_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90013-6"},{"key":"S0960129511000375_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"S0960129511000375_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-007-9052-4"},{"key":"S0960129511000375_ref38","unstructured":"Levy P. B. (2009) Boolean precongruences."},{"key":"S0960129511000375_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"S0960129511000375_ref52","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"S0960129511000375_ref39","volume-title":"Proceedings EDAC\u2013EUROASIC'93: IEEE European Design Automation Conference, Paris, France","author":"Margaria","year":"1993"},{"key":"S0960129511000375_ref4","unstructured":"Barwise J. and Moss L. (1996) Vicious Circles: On the mathematics of non-wellfounded phenomena, CSLI Lecture Notes 60, CSLI Publications."},{"key":"S0960129511000375_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10828-9_52"},{"key":"S0960129511000375_ref41","volume-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"S0960129511000375_ref44","article-title":"Derivation of characteristic formulae. In: MFCS'98 Workshop on Concurrency, Brno, Czech Republic","volume":"18","author":"M\u00fcller-Olm","year":"1998","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"S0960129511000375_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.01.021"},{"key":"S0960129511000375_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039058"},{"key":"S0960129511000375_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03741-2_16"},{"key":"S0960129511000375_ref28","unstructured":"Ingolfsdottir A. , Godskesen J. C. and Zeeberg M. (1987) Fra Hennessy\u2013Milner logik til CCS-processer. Master's thesis, Department of Computer Science, Aalborg University. (In Danish.)"},{"key":"S0960129511000375_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774"},{"key":"S0960129511000375_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"S0960129511000375_ref3","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2000131"},{"key":"S0960129511000375_ref5","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004268613379"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129511000375","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T22:47:36Z","timestamp":1556232456000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129511000375\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,28]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["S0960129511000375"],"URL":"https:\/\/doi.org\/10.1017\/s0960129511000375","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,2,28]]}}}