{"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":1750307204126,"version":"3.41.0"},"reference-count":27,"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>Systems consisting of several finite components that communicate via unbounded perfect FIFO channels (i.e., FIFO systems) arise naturally in modeling distributed systems. Despite well-known difficulties in analyzing such systems, they are of significant interest as they can describe a wide range of communication protocols.<\/jats:p>\n          <jats:p>\n            In this article, we study the problem of computing the set of reachable states of a FIFO system composed of\n            <jats:italic>piecewise<\/jats:italic>\n            components. This problem is closely related to calculating the set of all possible channel contents, that is, the\n            <jats:italic>limit language<\/jats:italic>\n            , for each control location. We present an algorithm for calculating the limit language of a system with a single communication channel. For multichannel systems, we show that the limit language is piecewise if the initial language is piecewise. Our construction is not effective in general; however, we provide algorithms for calculating the limit language of a restricted class of multichannel systems in which messages are not passed around in cycles through different channels. We show that the worst case complexity of our algorithms for single-channel and important subclasses of multichannel systems is exponential in the size of the initial content of the channels.\n          <\/jats:p>","DOI":"10.1145\/2071368.2071375","type":"journal-article","created":{"date-parts":[[2012,1,31]],"date-time":"2012-01-31T14:49:20Z","timestamp":1328021360000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Reachability Problems in Piecewise FIFO Systems"],"prefix":"10.1145","volume":"13","author":[{"given":"Naghmeh","family":"Ghafari","sequence":"first","affiliation":[{"name":"Critical Systems Labs"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}]},{"given":"Nils","family":"Klarlund","sequence":"additional","affiliation":[{"name":"Google Inc."}]},{"given":"Richard","family":"Trefler","sequence":"additional","affiliation":[{"name":"University of Waterloo"}]}],"member":"320","published-online":{"date-parts":[[2012,1]]},"reference":[{"volume-title":"Proceedings of the 8th IEEE Symposium on Logic in Computer Science (LICS\u201993)","author":"Abdulla P. A.","key":"e_1_2_1_1_1","unstructured":"Abdulla , P. A. and Jonsson , B . 1993. Verifying programs with unreliable channels . In Proceedings of the 8th IEEE Symposium on Logic in Computer Science (LICS\u201993) . 160--170. Abdulla, P. A. and Jonsson, B. 1993. Verifying programs with unreliable channels. In Proceedings of the 8th IEEE Symposium on Logic in Computer Science (LICS\u201993). 160--170."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691608"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008719024240"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/647166.717985"},{"volume-title":"Proceedings of 2nd IP Telephony Workshop.","author":"Bond G. W.","key":"e_1_2_1_6_1","unstructured":"Bond , G. W. , Ivan\u010di\u0107 , F. , Klarlund , N. , and Trefler , R . 2001. ECLIPSE feature logic analysis . In Proceedings of 2nd IP Telephony Workshop. Bond, G. W., Ivan\u010di\u0107, F., Klarlund, N., and Trefler, R. 2001. ECLIPSE feature logic analysis. In Proceedings of 2nd IP Telephony Workshop."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 12th International Conference on Computer Aided Verification (CAV\u201900)","volume":"1855","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Jonsson , B. , Nilsson , M. , and Touili , T . 2000. Regular model checking . In Proceedings of the 12th International Conference on Computer Aided Verification (CAV\u201900) . Lecture Notes in Computer Science , vol. 1855 , 403--418. Bouajjani, A., Jonsson, B., Nilsson, M., and Touili, T. 2000. Regular model checking. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV\u201900). Lecture Notes in Computer Science, vol. 1855, 403--418."},{"volume-title":"Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS\u201901)","author":"Bouajjani A.","key":"e_1_2_1_8_1","unstructured":"Bouajjani , A. , Muscholl , A. , and Touili , T . 2001. Permutation rewriting and algorithmic verification . In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS\u201901) . 399--408. Bouajjani, A., Muscholl, A., and Touili, T. 2001. Permutation rewriting and algorithmic verification. In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS\u201901). 399--408."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0012-365X(73)80005-6"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0003"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/61211.61217"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(02)00027-5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11784180_17"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_17"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1333874.1334163"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"e_1_2_1_18_1","unstructured":"IBM. 2007. Business Process Execution Language for Web Services (BPEL) Version 1.1. IBM. http:\/\/www-128.ibm.com\/developerworks\/library\/specification\/ws-bpel.  IBM. 2007. Business Process Execution Language for Web Services (BPEL) Version 1.1 . IBM. http:\/\/www-128.ibm.com\/developerworks\/library\/specification\/ws-bpel."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.729683"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.002"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(72)90063-5"},{"key":"e_1_2_1_22_1","unstructured":"M\u00f8ller A. 2007. An automaton\/regular expression library for Java. http:\/\/www.brics.dk\/automaton. M\u00f8ller A. 2007. An automaton\/regular expression library for Java. http:\/\/www.brics.dk\/automaton."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 7th International Conference on Protocol Specification, Testing and Verification. 207--219","author":"Pachl J. K.","year":"1987","unstructured":"Pachl , J. K. 1987 . Protocol description and analysis based on a state transition model with channel expressions . In Proceedings of the 7th International Conference on Protocol Specification, Testing and Verification. 207--219 . Pachl, J. K. 1987. Protocol description and analysis based on a state transition model with channel expressions. In Proceedings of the 7th International Conference on Protocol Specification, Testing and Verification. 207--219."},{"volume-title":"Proceedings of the 3rd International Workshop on Computer Aided Verification (CAV\u201991)","author":"Sistla A. P.","key":"e_1_2_1_24_1","unstructured":"Sistla , A. P. and Zuck , L. D . 1991. Automatic temporal verification of buffer systems . In Proceedings of the 3rd International Workshop on Computer Aided Verification (CAV\u201991) . 59--69. Sistla, A. P. and Zuck, L. D. 1991. Automatic temporal verification of buffer systems. In Proceedings of the 3rd International Workshop on Computer Aided Verification (CAV\u201991). 59--69."},{"volume-title":"Proceedings of the 2nd Symposium on Logics in Computer Science.","author":"Sistla P.","key":"e_1_2_1_25_1","unstructured":"Sistla , P. and Zuck , L . 1987. On the eventuality operation in temporal logic . In Proceedings of the 2nd Symposium on Logics in Computer Science. Sistla, P. and Zuck, L. 1987. On the eventuality operation in temporal logic. In Proceedings of the 2nd Symposium on Logics in Computer Science."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1006"},{"volume-title":"Proceedings of 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE&rsquo;\u201903)","author":"Wodey P.","key":"e_1_2_1_27_1","unstructured":"Wodey , P. , Camarroque , G. , Baray , F. , Hersemeule , R. , and Cousin , J . -P. 2003. LOTOS code generation for model checking of STBus Based SoC: The STBus interconnect . In Proceedings of 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE&rsquo;\u201903) . Wodey, P., Camarroque, G., Baray, F., Hersemeule, R., and Cousin, J.-P. 2003. LOTOS code generation for model checking of STBus Based SoC: The STBus interconnect. In Proceedings of 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE&rsquo;\u201903)."},{"volume-title":"Handbook of Language Theory","author":"Yu S.","key":"e_1_2_1_28_1","unstructured":"Yu , S. 1997. Regular languages . In Handbook of Language Theory , Vol. I , Rozenberg and Salomaa Eds., Springer . Yu, S. 1997. Regular languages. In Handbook of Language Theory, Vol. I, Rozenberg and Salomaa Eds., Springer."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071368.2071375","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2071368.2071375","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.2071375"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["10.1145\/2071368.2071375"],"URL":"https:\/\/doi.org\/10.1145\/2071368.2071375","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-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-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"}}]}}