{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:20Z","timestamp":1761597020752,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48778-6_15","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T10:18:07Z","timestamp":1178014687000},"page":"244-264","source":"Crossref","is-referenced-by-count":20,"title":["Bisimulation Algorithms for Stochastic Process Algebras and Their BDD-Based Implementation"],"prefix":"10.1007","author":[{"given":"Holger","family":"Hermanns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Siegle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"15_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/3-540-63166-6_14","volume-title":"Proc. CAV\u2019 97","author":"C. Baier","year":"1997","unstructured":"C. Baier and H. Hermanns. Weak Bisimulation for Fully Probabilistic Processes. In Proc. CAV\u2019 97, Springer LNCS 1254:119\u2013130, 1997."},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00127-8","volume":"202","author":"M. Bernardo","year":"1998","unstructured":"M. Bernardo and R. Gorrieri. A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. Theoretical Computer Science 202:1\u201354, 1998.","journal-title":"Theoretical Computer Science"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T. Bolognesi","year":"1987","unstructured":"T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14:25\u201359, 1987.","journal-title":"Computer Networks and ISDN Systems"},{"key":"15_CR4","series-title":"Rapports de Recherche","volume-title":"Weak and branching bisimulation in FCTOOL","author":"A. Bouali","year":"1992","unstructured":"A. Bouali. Weak and branching bisimulation in FCTOOL. Rapports de Recherche 1575, INRIA Sophia Antipolis, Valbonne Cedex, France, 1992."},{"key":"15_CR5","unstructured":"H. Bruchner. Symbolische Manipulation von stochastischen Transitionssystemen. Internal study, Universit\u00e4t Erlangen-N\u00fcrnberg, IMMD VII, 1998. in German."},{"issue":"8","key":"15_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transaction on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transaction on Computers"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"R.E. Bryant and Y. Chen. Verification of Arithmetic Functions with Binary Moment Diagrams. In Proc. 32nd Design Automation Conference, 535\u2013541, ACM\/IEEE, 1995.","DOI":"10.1145\/217474.217583"},{"key":"15_CR8","unstructured":"E.M. Clarke, M. Fujita, P. McGeer, K. McMillan, J. Yang, and X. Zhao. Multi-terminal Binary Decision Diagrams: An efficient data structure for matrix representation. In Proc. International Workshop on Logic Synthesis, Tahoe City, May 1993."},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"D. Coppersmith and S. Winograd. Matrix Multiplication via Arithmetic Progressions. In Proc. 19th ACM Symposium on Theory of Computing, 1987.","DOI":"10.1145\/28395.28396"},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/BF02242704","volume":"6","author":"R. Enders","year":"1993","unstructured":"R. Enders, T. Filkorn, and D. Taubner. Generating BDDs for symbolic model checking in CCS. Distributed Computing, 6:155\u2013164, 1993.","journal-title":"Distributed Computing"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","volume":"13","author":"J.C. Fernandez","year":"1989","unstructured":"J.C. Fernandez. An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming, 13:219\u2013236, 1989.","journal-title":"Science of Computer Programming"},{"issue":"3","key":"15_CR12","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R. J. Glabbeek van","year":"1996","unstructured":"R. J. van Glabbeek and W. Weijland:. Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM, 43(3):555\u2013600, 1996.","journal-title":"Journal of the ACM"},{"key":"15_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1007\/BFb0032063","volume-title":"Proc. ICALP\u201990","author":"J. F. Groote","year":"1990","unstructured":"J. F. Groote and F.W. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In Proc. ICALP\u201990, Springer LNCS 443:626\u2013638, 1990."},{"issue":"12","key":"15_CR14","doi-asserted-by":"publisher","first-page":"1479","DOI":"10.1109\/43.552081","volume":"15","author":"G. D. Hachtel","year":"1996","unstructured":"G. D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Markovian Analysis of Large Finite State Machines. IEEE Transactions on CAD, 15(12):1479\u20131493, 1996.","journal-title":"IEEE Transactions on CAD"},{"key":"15_CR15","unstructured":"H. Hermanns. Interactive Markov Chains. PhD thesis, Universit\u00e4t Erlangen-N\u00fcrnberg, 1998."},{"issue":"9\u201310","key":"15_CR16","doi-asserted-by":"publisher","first-page":"901","DOI":"10.1016\/S0169-7552(97)00133-5","volume":"30","author":"H. Hermanns","year":"1998","unstructured":"H. Hermanns, U. Herzog, and V. Mertsiotakis. Stochastic Process Algebras-Between LOTOS and Markov Chains. Computer Networks and ISDN Systems, 30(9\u201310):901\u2013924, 1998.","journal-title":"Computer Networks and ISDN Systems"},{"issue":"4","key":"15_CR17","first-page":"71","volume":"27","author":"H. Hermanns","year":"1994","unstructured":"H. Hermanns and M. Rettelbach. Syntax, Semantics, Equivalences, and Axioms for MTIPP. In Proc. 2nd PAPM Workshop. University of Erlangen-N\u00fcrnberg, IMMD 27(4):71\u201387, 1994.","journal-title":"Proc. 2nd PAPM Workshop"},{"key":"15_CR18","unstructured":"H. Hermanns and J.P. Katoen. Automated Compositional Markov Chain Generation for a Plain Old Telephony System. to appear in Science of Computer Programming, 1998."},{"key":"15_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/BFb0055626","volume-title":"Proc. CONCUR\u201998","author":"H. Hermanns","year":"1998","unstructured":"H. Hermanns and M. Lohrey. Priority and maximal progress are completely axiomatisable. In Proc. CONCUR\u201998, Springer LNCS 1466:237\u2013252, 1998."},{"key":"15_CR20","unstructured":"H. Hermanns and M. Siegle. Computing Bisimulations for Stochastic Process Algebras using Symbolic Techniques. In Proc. 6th Int. PAPM Workshop, 103\u2013118, Nice, 1998."},{"key":"15_CR21","unstructured":"H. Hermanns, J. Meyer-Kayser and M. Siegle. Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains. submitted for publication, 1999."},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511569951"},{"key":"15_CR23","doi-asserted-by":"crossref","first-page":"211","DOI":"10.3233\/FI-1992-17304","volume":"17","author":"T. Huynh","year":"1992","unstructured":"T. Huynh and L. Tian. On some Equivalence Relations for Probabilistic Processes. Fundamenta Informaticae, 17:211\u2013234, 1992.","journal-title":"Fundamenta Informaticae"},{"key":"15_CR24","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P. Kanellakis","year":"1990","unstructured":"P. Kanellakis and S. Smolka. CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Information and Computation, 86:43\u201368, 1990.","journal-title":"Information and Computation"},{"key":"15_CR25","unstructured":"J. G. Kemeny and J.L. Snell. Finite Markov Chains. Springer, 1976."},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Y.-T. Lai and S. Sastry. Edge-Valued Binary Decision Diagrams for Multi-Level Hierarchical Verification. In 29th Design Automation Conference,608\u2013613, ACM\/IEEE, 1992.","DOI":"10.1109\/DAC.1992.227813"},{"issue":"1","key":"15_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K. Larsen","year":"1991","unstructured":"K. Larsen and A. Skou. Bisimulation through Probabilistic Testing. Information and Computation, 94(1):1\u201328, 1991.","journal-title":"Information and Computation"},{"key":"15_CR28","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, London, 1989."},{"issue":"6","key":"15_CR29","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"R. Paige and R. Tarjan. Three Partition Refinement Algorithms. SIAM Journal of Computing, 16(6):973\u2013989, 1987.","journal-title":"SIAM Journal of Computing"},{"key":"15_CR30","unstructured":"M. Siegle. Technique and tool for symbolic representation and manipulation of stochastic transition systems. TR IMMD 7 2\/98, Universit\u00e4t Erlangen-N\u00fcrnberg, March 1998."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:07:29Z","timestamp":1736986049000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}