{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:26:44Z","timestamp":1750307204893,"version":"3.41.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,1]]},"abstract":"<jats:p>\n            We analyze the problem of solving Boolean equation systems through the use of\n            <jats:italic>structure graphs<\/jats:italic>\n            . The latter are obtained through an elegant set of Plotkin-style deduction rules. Our main contribution is that we show that equation systems with bisimilar structure graphs have the same solution. We show that our work conservatively extends earlier work, conducted by Keiren and Willemse, in which\n            <jats:italic>dependency graphs<\/jats:italic>\n            were used to analyze a subclass of Boolean equation systems,\n            <jats:italic>viz<\/jats:italic>\n            ., equation systems in\n            <jats:italic>standard recursive form<\/jats:italic>\n            . We illustrate our approach by a small example, demonstrating the effect of simplifying an equation system through minimization of its structure graph.\n          <\/jats:p>","DOI":"10.1145\/2071368.2071376","type":"journal-article","created":{"date-parts":[[2012,1,31]],"date-time":"2012-01-31T14:49:20Z","timestamp":1328021360000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Structural Analysis of Boolean Equation Systems"],"prefix":"10.1145","volume":"13","author":[{"given":"Jeroen J. A.","family":"Keiren","sequence":"first","affiliation":[{"name":"Eindhoven University of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel A.","family":"Reniers","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim A. C.","family":"Willemse","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,1]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90266-6"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90029-4"},{"key":"e_1_2_1_3_1","first-page":"293","article-title":"Modal logics and mu-calculi: An introduction. In Handbook of Process Algebra. J. Bergstra, A. Ponse, and S. Smolka Eds","volume":"4","author":"Bradfield J. C.","year":"2001","journal-title":"Elsevier Chapter"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Chen T. Ploeger B. van de Pol J. and \n      \n      \n      Willemse T. A. C\n      \n  \n  . \n  2007\n  . Equivalence checking for infinite systems using parameterized Boolean equation systems. In Proceedings of the 18th International Conference on Concurrency Theory. L. Caires and V. T. Vasconcelos Eds. Lecture Notes in Computer Science vol. \n  4703 Springer 120--135. Chen T. Ploeger B. van de Pol J. and Willemse T. A. C. 2007. Equivalence checking for infinite systems using parameterized Boolean equation systems. In Proceedings of the 18th International Conference on Concurrency Theory . L. Caires and V. T. Vasconcelos Eds. Lecture Notes in Computer Science vol. 4703 Springer 120--135.","DOI":"10.1007\/978-3-540-74407-8_9"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11779148_7"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Garavel H. Mateescu R. Lang F. and \n      \n      \n      Serwe W\n      \n  \n  . \n  2007\n  . CADP 2006: A toolbox for the construction and analysis of distributed processes. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907). W. Damm and H. Hermanns Eds. Lecture Notes in Computer Science vol. \n  4590 Springer 158--163. Garavel H. Mateescu R. Lang F. and Serwe W. 2007. CADP 2006: A toolbox for the construction and analysis of distributed processes. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907) . W. Damm and H. Hermanns Eds. Lecture Notes in Computer Science vol. 4590 Springer 158--163.","DOI":"10.1007\/978-3-540-73368-3_18"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90111-6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.08.002"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006930"},{"volume-title":"Process Algebra for Parallel and Distributed Processing","author":"Groote J. F.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(98)00150-1"},{"key":"e_1_2_1_12_1","unstructured":"Kein\u00e4nen M. K. 2006. Techniques for solving Boolean equation systems. Ph.D. thesis Helsinki University of Technology. Kein\u00e4nen M. K. 2006. Techniques for solving Boolean equation systems. Ph.D. thesis Helsinki University of Technology."},{"volume":"6405","volume-title":"Proceedings of the 5th International Haifa Verification Conference. Lecture Notes in Computer Science","author":"Keiren J. J. A.","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/647761.735342"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Liu X.\n     and \n      \n      \n      Smolka S\n      \n  \n  . \n  1998\n  . Simple linear-time algorithms for minimal fixed points. In Proceedings of the International Colloquium on Automata Languages and Programming. K. G. Larsen S. Skyum and G. Winskel Eds. Lecture Notes in Computer Science vol. \n  1443 Springer 53--66. Liu X. and Smolka S. 1998. Simple linear-time algorithms for minimal fixed points. In Proceedings of the International Colloquium on Automata Languages and Programming . K. G. Larsen S. Skyum and G. Winskel Eds. Lecture Notes in Computer Science vol. 1443 Springer 53--66.","DOI":"10.1007\/BFb0055040"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Liu X. Ramakrishnan C. and \n      \n      \n      Smolka S\n      \n  \n  . \n  1998\n  . Fully local and efficient evaluation of alternating fixed points. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems. B. Steffen Ed. Lecture Notes in Computer Science vol. \n  1384 Springer\n  . 5--19. Liu X. Ramakrishnan C. and Smolka S. 1998. Fully local and efficient evaluation of alternating fixed points. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems . B. Steffen Ed. Lecture Notes in Computer Science vol. 1384 Springer. 5--19.","DOI":"10.1007\/BFb0054161"},{"key":"e_1_2_1_18_1","unstructured":"Mader A. 1997. Verification of modal properties using Boolean equation systems. Ph.D. thesis Technische Universit\u00e4t M\u00fcnchen. Mader A. 1997. Verification of modal properties using Boolean equation systems. Ph.D. thesis Technische Universit\u00e4t M\u00fcnchen."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765881"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-005-0194-9"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.03.002"},{"volume-title":"Proceedings of the 5th G1 Conference","series-title":"Lecture Notes in Computer Science","author":"Park D. M.","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Plotkin G. D. 2004. A structural approach to operational semantics. J. Logic Alg. Program. 60--61 17--139. Plotkin G. D. 2004. A structural approach to operational semantics. J. Logic Alg. Program. 60--61 17--139.","DOI":"10.1016\/j.jlap.2004.05.001"},{"volume":"18","volume-title":"Proceedings of the Workshop on Structural Operational Semantics (SOS\u201909)","author":"Reniers M. A.","key":"e_1_2_1_24_1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1781794.1781833"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Stevens P.\n     and \n      \n      \n      Stirling C\n      \n  \n  . \n  1998\n  . Practical model checking using games. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems. B. Steffen Ed. Lecture Notes in Computer Science vol. \n  1384 Springer 85--101. Stevens P. and Stirling C. 1998. Practical model checking using games. In Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems . B. Steffen Ed. Lecture Notes in Computer Science vol. 1384 Springer 85--101.","DOI":"10.1007\/BFb0054166"},{"volume-title":"Notes for Mathfit Instructional Meeting on Games and Computation","year":"1997","author":"Stirling C.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654.1887694"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00009-7"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071368.2071376","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2071368.2071376","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:22Z","timestamp":1750241182000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071368.2071376"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["10.1145\/2071368.2071376"],"URL":"https:\/\/doi.org\/10.1145\/2071368.2071376","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2012,1]]},"assertion":[{"value":"2010-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}