{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:20:30Z","timestamp":1725456030439},"publisher-location":"Berlin\/Heidelberg","reference-count":26,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019021X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0026106","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:47:21Z","timestamp":1132645641000},"page":"215-230","source":"Crossref","is-referenced-by-count":40,"title":["Proof systems for Hennessy-Milner Logic with recursion"],"prefix":"10.1007","author":[{"given":"Kim G.","family":"Larsen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Aczel, P.: An Introduction to Inductive Definitions, North-Holland, in the Handbook of Mathematical Logic, 1983."},{"key":"15_CR2","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"Ben-Ari, M., Pnueli, A. and Manna, Z.: The Temporal Logic of Branching Time, Acta Informatica, 20, pp 207\u2013226, 1983.","journal-title":"Acta Informatica"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Bloom and Troeger: A Logical Characterization of Observation Equivalence, TCS, vol 35, no 1, 1985","DOI":"10.1016\/0304-3975(85)90004-0"},{"key":"15_CR4","unstructured":"Brookes, S. and Rounds, R.: Behavioural Equivalence Relations Induced by Programming Logics, LNCS 154, 1983."},{"key":"15_CR5","first-page":"52","volume":"131","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M. and Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic, in: Logics of Programs, LNCS 131, 52\u201371, 1981.","journal-title":"LNCS"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A, Sistla, A.P.: Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach, Proc 10th ACM POPL, 117\u2013126, 1983.","DOI":"10.1145\/567067.567080"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Graf, S. and Sifakis, J.: A modal Characterization of observational congruence on finite terms of CCS, LNCS 172, 1984.","DOI":"10.1007\/3-540-13345-3_20"},{"key":"15_CR8","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/BF00288467","volume":"23","author":"S. Graf","year":"1986","unstructured":"Graf, S. and Sifakis, J.: A Logic for the Specification and Proof of Regular Controllable Processes of CCS, Acta Informatica, 23, pp 507\u2013527, 1986.","journal-title":"Acta Informatica"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Graf, S. Sifakis, J.: A Logic for the Description of Non-deterministic Programs and Their Properties, Information and Control, vol. 68, nos 1\u20133, 1986.","DOI":"10.1016\/S0019-9958(86)80038-9"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Hennessy, M. and Milner, R.: Algebraic Laws for Nondeterminism and Concurrency, Journal of the Association for Computing Machinery, 1985.","DOI":"10.1145\/2455.2460"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Results on the Propositional Mu-Calculus, 9th ICALP, LNCS 140, 1982.","DOI":"10.7146\/dpb.v11i146.7420"},{"key":"15_CR12","unstructured":"Larsen, K.G.: Proof Systems for Hennessy-Milner Logic with Recursion, Aalborg University, Department of Mathematics and Computer Science, R 87-20, 1987."},{"key":"15_CR13","unstructured":"Manna, Z. and Wolper, P. Synthesis of Communicating Processes from Temporal Logic Specifications, LNCS 131, 1981."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Milner, R.: A Calculus of Communicating Systems, LNCS 92, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Milner, R.: A Modal Characterization of Observable Machine-behaviour, LNCS 112, 1981.","DOI":"10.1007\/3-540-10828-9_52"},{"key":"15_CR16","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R. Milner","year":"1983","unstructured":"Milner, R.: Calculi for Synchrony and Asynchrony, TCS 25, pp 267\u2013310, 1983.","journal-title":"TCS"},{"key":"15_CR17","unstructured":"Park, D.: Concurrency and automata on infinite sequences, LNCS 84, 1980."},{"key":"15_CR18","volume-title":"A Structural Approach to Operational Semantics","author":"G. Plotkin","year":"1981","unstructured":"Plotkin, G.: A Structural Approach to Operational Semantics, DAIMI-FN-19, Aarhus University, Computer Science Department, Denmark, 1981."},{"key":"15_CR19","unstructured":"Pnueli, A.: Linear and Branching Structures in the Semantics and Logics of Reactive Systems, 12th ICALP, LNCS 194, 1985."},{"key":"15_CR20","unstructured":"Stirling, C.: A Proof Theoretic Characterization of Observationl Equivalence, FCT-TCS Bangalore, To appear in TCS, 1983."},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Stirling, C.: A Complete Proof System for a Subset of SCCS, LNCS 185, to appear in CAAP'85, 1985.","DOI":"10.1007\/3-540-15198-2_16"},{"key":"15_CR22","unstructured":"Stirling, C.: A Compositional Modal Proof System for a Subset of CCS, 12th ICALP, LNCS 194, full version to appear in TCS., 1985."},{"key":"15_CR23","unstructured":"Stirling, C.: Modal Logics for Communicating Systems, to appear in TCS., 1986."},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Lattice-Theoretical Fixpoint Theorem and its Applications, Pacific Journal of Math. 5, 1955.","DOI":"10.2140\/pjm.1955.5.285"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Winskel, G.: On the Composition and Decomposition of Assertions, LNCS 197, 1984.","DOI":"10.1007\/3-540-15670-4_3"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Winskel, G.: A Complete Proof System for SCCS with Modal Assertions, Technical Report, Computer Laboratory, University of Cambridge, 1985.","DOI":"10.1007\/3-540-16042-6_22"}],"container-title":["Lecture Notes in Computer Science","CAAP '88"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0026106.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,20]],"date-time":"2021-07-20T03:50:48Z","timestamp":1626753048000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0026106"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019021X"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0026106","relation":{},"subject":[]}}