{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T03:12:02Z","timestamp":1775013122725,"version":"3.50.1"},"reference-count":33,"publisher":"Pleiades Publishing Ltd","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Program Comput Soft"],"published-print":{"date-parts":[[2011,7]]},"DOI":"10.1134\/s0361768811040013","type":"journal-article","created":{"date-parts":[[2011,7,25]],"date-time":"2011-07-25T21:54:45Z","timestamp":1311630885000},"page":"200-209","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Game-theoretic simulation checking tool"],"prefix":"10.1134","volume":"37","author":[{"given":"P. E.","family":"Bulychev","sequence":"first","affiliation":[]}],"member":"137","published-online":{"date-parts":[[2011,7,27]]},"reference":[{"key":"6109_CR1","unstructured":"Clarke, E. M., Grumberg, O., and Peled, D., Model Checking, MIT Press, 1999. Translated under the title Verifikatsiya modelei program: Model Checking, Moscow: MTsNMO, 2002."},{"issue":"5","key":"6109_CR2","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H., Counterexample-Guided Abstraction Refinement for Symbolic Model Checking, J. ACM, 2003, vol. 50, no. 5, pp. 752\u2013794.","journal-title":"J. ACM"},{"key":"6109_CR3","unstructured":"Butler, M., Incremental Design of Distributed Systems with Event-b, in Engineering Methods and Tools for Software Safety and Security-Marktoberdoif Summer School, 2008, IOS, pp. 131\u2013160."},{"key":"6109_CR4","doi-asserted-by":"crossref","unstructured":"Konnov, I.V. and Zakharov, V.A., An Invariant-Based Approach to the Verification of Asynchronous Parameterized Networks, J. Symbolic Computation, 2009.","DOI":"10.1016\/j.jsc.2008.11.006"},{"key":"6109_CR5","unstructured":"van Langevelde, I.A., Symmetry in Labeled Transition Systems, 2003."},{"key":"6109_CR6","unstructured":"Wimmer, R., Herbstritt, M., and Becker, B., Minimization of Large State Spaces Using Symbolic Branching Bisimulation, Proc. of the 9th IEEE Workshop on Design Diagnostics of Electronic Circuits Systems (DDECS), IEEE Computer Society, 2006, pp. 9\u201314."},{"issue":"2","key":"6109_CR7","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/635499.635502","volume":"4","author":"D. Bustan","year":"2003","unstructured":"Bustan, D. and Grumberg, O., Simulation-Based Minimization, ACM Trans. Computational Logic, 2003, vol. 4, no. 2, pp. 181\u2013206.","journal-title":"ACM Trans. Computational Logic"},{"key":"6109_CR8","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Confidentiality for Multithreaded Programs via Bisimulation, in Andrei Ershov Int. Conf. on Perspectives of System Informatics, Springer, 2003, pp. 260\u2013273.","DOI":"10.1007\/978-3-540-39866-0_27"},{"issue":"13","key":"6109_CR9","first-page":"219","volume":"13","author":"J.-C. Fernandez","year":"1989","unstructured":"Fernandez, J.-C., An Implementation of an Efficient Algorithm for Bisimulation Equivalence, Sci. Comput. Programming, 1989, vol. 13, no. 13, p. 219.","journal-title":"Sci. Comput. Programming"},{"key":"6109_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, M.R., Henzinger, T.A., and Kopke, P.W., Computing Simulations on Finite and Infinite Graphs, 36th IEEE Symp. on Foundations of Corp. Sci, IEEE Computer Society, 1996, pp. 453\u2013462.","DOI":"10.1109\/SFCS.1995.492576"},{"issue":"5","key":"6109_CR11","doi-asserted-by":"publisher","first-page":"1159","DOI":"10.1137\/S0097539703420675","volume":"34","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Wilke, T., and Schuller, R.A., Fair Simulation Relations, Parity Games, and State Space Reduction for Buchi Automata, SIAM J. Computing, 2005, vol. 34, no. 5, pp. 1159\u20131175.","journal-title":"SIAM J. Computing"},{"key":"6109_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., and Roveri, M., Nusmv: A New Symbolic Model Checker, Int. J. Software Tools Technology Transfer, vol. 2, 2000.","DOI":"10.1007\/s100090050046"},{"issue":"8","key":"6109_CR13","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E., Graph-Based Algorithms for Boolean Function Manipulation, IEEE Trans. Comput., 1986, vol. 35, no. 8, pp. 677\u2013G91.","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"6109_CR14","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., and Sistla, A.P., Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM Trans. Program. Lang. Syst., 1986, vol. 8, no. 2, pp. 244\u2013263.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6109_CR15","doi-asserted-by":"crossref","unstructured":"Amir Pnueli, A Temporal Logic of Concurrent Programs, Theor. Comput. Sci., vol. 13, pp. 45\u201360.","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"6109_CR16","first-page":"657","volume":"83","author":"L. Lamport","year":"1983","unstructured":"Lamport, L., What Good Is Temporal Logic?, in 1F1P, 1983, vol. 83, pp. 657\u2013668.","journal-title":"1F1P"},{"issue":"5","key":"6109_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J., The Model Checker Spin, Software Engineering, 1997, vol. 23, no. 5, pp. 279\u2013295.","journal-title":"Software Engineering"},{"issue":"s.1\u20132","key":"6109_CR18","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., and Grumberg, O., Characterizing Finite Kripke Structures in Propositional Temporal Logic, Theor. Comput. Sci., 1988, vol. 59, nos. 1\u20132, pp. 115\u2013131.","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"6109_CR19","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. De Nicola","year":"1995","unstructured":"De Nicola, R. and Vaandrager, F., Three Logics for Branching Bisimulation, J. ACM, 1995, vol. 42, no. 2, pp. 458\u2013487.","journal-title":"J. ACM"},{"key":"6109_CR20","doi-asserted-by":"crossref","unstructured":"Etessami, K., A Hierarchy of Polynomial-Time Computable Simulations for Automata, CONCUR 2002, 2002.","DOI":"10.1007\/3-540-45694-5_10"},{"issue":"3","key":"6109_CR21","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J. van Glabbeek","year":"1996","unstructured":"van Glabbeek, R.J. and Weijland, W.P., Branching Time and Abstraction in Bisimulation Semantics, J. ACM, 1996, vol. 43, no. 3, pp. 555\u2013600.","journal-title":"J. ACM"},{"issue":"1","key":"6109_CR22","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1006\/inco.2001.3085","volume":"173","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Kupferman, O., and Rajamani, S.K., Fair Simulation, Information Computation, 2002, vol. 173, no. 1, pp. 64\u201381.","journal-title":"Information Computation"},{"key":"6109_CR23","first-page":"59","volume":"12","author":"P.E. Bulychev","year":"2007","unstructured":"Bulychev, P.E., Konnov, I.V., and Zakharov, V.A., Computing (Bi)simulation Relations Preserving ctlx Logic for Ordinary and Fair Kripke Structures, Trudy institute sistemnogo programnmirovaniya (Proc. of Inst. of System Programming), 2007, vol. 12, pp. 59\u201376.","journal-title":"Trudy institute sistemnogo programnmirovaniya"},{"key":"6109_CR24","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1007\/978-3-642-04081-8_36","volume-title":"CONCUR 2009: Proc. of the 20th Int. Conf. on Concurrency Theory","author":"F. Ranzato","year":"2009","unstructured":"Ranzato, F. and Tapparo, F., Computing Stuttering Simulations, CONCUR 2009: Proc. of the 20th Int. Conf. on Concurrency Theory, Berlin, Heidelberg: Verlag, 2009, pp. 542\u2013556."},{"key":"6109_CR25","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/11901914_35","volume":"4218","author":"R. Wimmer","year":"2006","unstructured":"Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., and Becker, B., Sigref-A Symbolic Bisimulation Tool Box, Lecture Notes in Computer Science (Proc. of the 4 Int. Symp. on Automated Technology for Verification and Analysis (ATVA)), vol. 4218, Springer, 2006, pp. 477\u2013492.","journal-title":"Lecture Notes in Computer Science"},{"key":"6109_CR26","doi-asserted-by":"crossref","unstructured":"Groote, J.P. and Vaandrager, F.W., An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence, in Automata, Languages and Programming, 1990, pp. 626\u2013638.","DOI":"10.1007\/BFb0032063"},{"issue":"1","key":"6109_CR27","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H.R. Andersen","year":"1994","unstructured":"Andersen, H.R., Model Checking and Boolean Graphs, Theor. Comput. Sci., 1994, vol. 126, no. 1, pp. 3\u201330.","journal-title":"Theor. Comput. Sci."},{"key":"6109_CR28","doi-asserted-by":"crossref","unstructured":"Tarski, A., A Lattice-Theoretical Fixpoint Theorem and Its Applications, 1955.","DOI":"10.2140\/pjm.1955.5.285"},{"key":"6109_CR29","unstructured":"Edelkamp, S., Symbolic Exploration in Two-Player Games: Preliminary Results, Proc. of the Sixth Int. Conf. on AI Planning and Scheduling (A1PS-02) Workshop on Model Checking, 2002, pp. 40\u201348."},{"key":"6109_CR30","unstructured":"Ellson, J., Gansner, E.R., Koutsofios, E., North, S.C., and Woodhull, G."},{"key":"6109_CR31","unstructured":"Cudd: Colorado University BDD Package, http:\/\/vlsi.colorado.edu\/\u201cfabio\/CUDD."},{"key":"6109_CR32","unstructured":"Pycudd: An Enhanced Python Interface to the Colorado University BDD Package, http:\/\/www.ece.ucsb.edu\/bears\/pycudd.html."},{"key":"6109_CR33","unstructured":"Moller, F. and Stevens, P., Edinburgh Concurrency Workbench User Manual (Version 7.1), 1999."}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768811040013.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768811040013","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768811040013","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768811040013.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:05:49Z","timestamp":1775009149000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768811040013"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,7]]}},"alternative-id":["6109"],"URL":"https:\/\/doi.org\/10.1134\/s0361768811040013","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7]]},"assertion":[{"value":"12 October 2010","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 July 2011","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}