{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:57:21Z","timestamp":1725663441097},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540562870"},{"type":"electronic","value":"9783540475071"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-56287-7_117","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T06:01:30Z","timestamp":1330236090000},"page":"342-355","source":"Crossref","is-referenced-by-count":4,"title":["Reasoning about safety and liveness properties for probabilistic processes"],"prefix":"10.1007","author":[{"given":"Linda","family":"Christoff","sequence":"first","affiliation":[]},{"given":"Ivan","family":"Christoff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"26_CR1","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"J.A. Bergstra","year":"1984","unstructured":"J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60:109\u2013137, 1984.","journal-title":"Information and Control"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"L. Christoff and I. Christoff. Efficient algorithms for verification of equivalences for probabilistic processes. In Proc. 3 rd Intl. Workshop on Computer Aided Verification, LNCS 575, 310\u2013321. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55179-4_30"},{"key":"26_CR3","volume-title":"Technical Report DoCS 92\/34","author":"L. Christoff","year":"1992","unstructured":"L. Christoff and I. Christoff. Reasoning about safety and liveness properties for probabilistic processes. Technical Report DoCS 92\/34, Department of Computer Systems, Uppsala University, Uppsala, Sweden, 1992."},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"E. Clarke and A. Emerson. Design and synthesis of synchronization skeletons using branching time Temporal Logic. In Proc. Workshop on Logics of Programs, LNCS 131, 52\u201371. Springer-Verlag, 1982.","DOI":"10.1007\/BFb0025774"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"I. Christoff. Testing equivalences and fully abstract models for probabilistic processes. In Proc. CONCUR '90 Theories of Concurrency: Unification and Extension, LNCS 458, 126\u2013140. Springer-Verlag, 1990.","DOI":"10.1007\/BFb0039056"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, S. Smolka, and A. Zwarico. Testing preorders for probabilistic processes. In Proc. 19 th Intl. Coll. on Automata, Languages and Programming, LNCS 623, 708\u2013719. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55719-9_116"},{"key":"26_CR7","unstructured":"A. Giacalone, C.-C. Jou, and S. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proc. IFIP Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, April 1990."},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"R. van Glabbeek, S. Smolka, B. Steffen, and C. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proc. 5 th IEEE Symp. on Logic in Computer Science, 130\u2013141, 1990.","DOI":"10.1109\/LICS.1990.113740"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"H. Hansson and B. Jonsson. A framework for reasoning about time and reliability. In Proc. 10 th IEEE Real-Time Systems Symp., 1989.","DOI":"10.1109\/REAL.1989.63561"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"H. Hansson and B. Jonsson. A calculus for communicating systems with time and probabilities. In Proc. 11 th IEEE Real-Time Systems Symp., 1990.","DOI":"10.1109\/REAL.1990.128759"},{"issue":"1","key":"26_CR11","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137\u2013161, 1985.","journal-title":"Journal of the ACM"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"S. Hart and M. Sharir. Probabilistic Temporal Logics for finite and bounded models. In Proc. 16th ACM Symp. on Theory of Computing, 1\u201313, 1984.","DOI":"10.1145\/800057.808660"},{"key":"26_CR14","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"26_CR15","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"K.G. Larsen","year":"1990","unstructured":"K.G. Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72:265\u2013288, 1990.","journal-title":"Theoretical Computer Science"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. In Proc. 16 th ACM Symp. on Principles of Programming Languages, 344\u2013352, 1989.","DOI":"10.1145\/75277.75307"},{"key":"26_CR17","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In Proc. 12 th Intl. Coll. on Automata, Languages and Programming, LNCS 194, 15\u201332. Springer-Verlag, 1985.","DOI":"10.1007\/BFb0015727"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"C. Stirling and D. Walker. Local model checking in the modal mu-calculus. In Proc. Intl. Joint Conf. on Theory and Practice of Software Development, LNCS 351, 369\u2013383. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-50939-9_144"},{"key":"26_CR20","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285\u2013309, 1955.","journal-title":"Pacific Journal of Mathematics"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56287-7_117.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,30]],"date-time":"2021-12-30T23:45:06Z","timestamp":1640907906000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56287-7_117"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540562870","9783540475071"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-56287-7_117","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}