{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:27:41Z","timestamp":1750307261766,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2011,5,1]],"date-time":"2011-05-01T00:00:00Z","timestamp":1304208000000},"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":[[2011,5]]},"abstract":"<jats:p>We present an effective algorithm for the automatic construction of finite modal transition systems as abstractions of potentially infinite concurrent processes. Modal transition systems are recognized as valuable abstractions for model checking because they allow for the validation as well as refutation of safety and liveness properties. However, the algorithmic construction of finite abstractions from potentially infinite concurrent processes is a missing link that prevents their more widespread usage for model checking of concurrent systems. Our algorithm is a worklist algorithm using concepts from abstract interpretation and operating upon mappings from sets to intervals in order to express simultaneous over- and underapproximations of the multisets of process actions available in a particular state. We obtain a finite abstraction that is 3-valued in both states and transitions and that supports the definition of a 3-valued modal logic for validating as well as refuting properties of systems. The construction is illustrated on a few examples, including the Ingemarsson-Tang-Wong key agreement protocol.<\/jats:p>","DOI":"10.1145\/1929954.1929955","type":"journal-article","created":{"date-parts":[[2011,5,17]],"date-time":"2011-05-17T12:59:03Z","timestamp":1305637143000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Modal abstractions of concurrent behavior"],"prefix":"10.1145","volume":"12","author":[{"given":"Flemming","family":"Nielson","sequence":"first","affiliation":[{"name":"Technical University of Denmark, Kongens Lyngby, Denmark"}]},{"given":"Sebastian","family":"Nanz","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Hanne Riis","family":"Nielson","sequence":"additional","affiliation":[{"name":"Technical University of Denmark"}]}],"member":"320","published-online":{"date-parts":[[2011,5,16]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Baier C. and Katoen J.-P. 2008. Principles of Model Checking. MIT Press.   Baier C. and Katoen J.-P. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.04.002"},{"volume":"2031","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01)","author":"Ball T.","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/646733.701449"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Boyd C. and Mathuria A. 2003. Protocols for Authentication and Key Establishment. Springer.   Boyd C. and Mathuria A. 2003. Protocols for Authentication and Key Establishment. Springer.","DOI":"10.1007\/978-3-662-09527-0"},{"volume":"1633","volume-title":"Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99)","author":"Bruns G.","key":"e_1_2_1_6_1"},{"volume":"1877","volume-title":"Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'00)","author":"Bruns G.","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0036-x"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/990010.990011"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_12_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press.   Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021870"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_15"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/111693.111710"},{"volume":"4595","volume-title":"Proceedings of the 14th International SPIN Workshop (SPIN'07)","author":"Fecher H.","key":"e_1_2_1_19_1"},{"volume":"2154","volume-title":"Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01)","author":"Godefroid P.","key":"e_1_2_1_20_1"},{"volume":"1254","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97)","author":"Graf S.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.10.009"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_14"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_25"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.008"},{"volume":"2028","volume-title":"Proceedings of the 10th European Symposium on Programming Languages and Systems (ESOP'01)","author":"Huth M.","key":"e_1_2_1_26_1"},{"volume-title":"Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 266--277","author":"Jonsson B.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00290339"},{"volume":"4590","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07)","author":"Katoen J.-P.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_24"},{"key":"e_1_2_1_31_1","volume-title":"Biblioteca Mathematica","volume":"1","author":"Kleene S. C.","year":"1952"},{"volume-title":"Proceedings of the 3rd Annual Symposium on Logic in Computer Science (LICS'88)","author":"Larsen K. G.","key":"e_1_2_1_32_1"},{"volume-title":"Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS '90)","author":"Larsen K. G.","key":"e_1_2_1_33_1"},{"key":"e_1_2_1_34_1","unstructured":"Milner R. 1989. Communication and Concurrency. Prentice Hall.   Milner R. 1989. Communication and Concurrency. Prentice Hall."},{"key":"e_1_2_1_35_1","unstructured":"Milner R. 1999. Communicating and Mobile Systems: The pi-calculus. Cambridge University Press.   Milner R. 1999. Communicating and Mobile Systems: The pi-calculus. Cambridge University Press."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392200.2392218"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_11"},{"volume-title":"Programs as Data Objects","series-title":"Lecture Notes in Computer Science","author":"Nielson F.","key":"e_1_2_1_38_1"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Nielson F. Riis Nielson H. and Hankin C. 1999. Principles of Program Analysis. Springer.   Nielson F. Riis Nielson H. and Hankin C. 1999. Principles of Program Analysis. Springer.","DOI":"10.1007\/978-3-662-03811-6"},{"volume":"1782","volume-title":"Proceedings of the European Symposium on Programming (ESOP'00)","author":"Nielson F.","key":"e_1_2_1_40_1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(01)00155-7"},{"key":"e_1_2_1_42_1","first-page":"1","article-title":"Pathway analysis for BioAmbients","volume":"77","author":"Pilegaard H.","year":"2008","journal-title":"J. Logic Algeb. Prog."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/860256.860268"},{"volume":"4444","volume-title":"Program Analysis and Compilation. Theory and Practice. Lecture Notes in Computer Science","author":"Riis Nielson H.","key":"e_1_2_1_44_1"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.4"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2008.07.001"},{"volume":"3148","volume-title":"Proceedings of the 11th International Static Analysis Symposium (SAS'04)","author":"Riis Nielson H.","key":"e_1_2_1_47_1"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292552"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.008"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297659"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1929954.1929955","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1929954.1929955","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:38Z","timestamp":1750243958000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1929954.1929955"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,5]]}},"alternative-id":["10.1145\/1929954.1929955"],"URL":"https:\/\/doi.org\/10.1145\/1929954.1929955","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2011,5]]},"assertion":[{"value":"2009-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-05-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}