{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:20Z","timestamp":1725490220203},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678977"},{"type":"electronic","value":"9783540446187"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44618-4_40","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T10:38:51Z","timestamp":1188297531000},"page":"566-581","source":"Crossref","is-referenced-by-count":5,"title":["Well-Abstracted Transition Systems"],"prefix":"10.1007","author":[{"given":"Alain","family":"Finkel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Purushothaman","family":"Iyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregoire","family":"Sutre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,12,21]]},"reference":[{"key":"40_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/3-540-49059-0_15","volume-title":"Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol","author":"P. Abdulla","year":"1999","unstructured":"P. Abdulla, A. Annichini, and A. Bouajjani. Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol. Lecture Notes in Computer Science, 1579:208\u2013222, 1999."},{"issue":"2","key":"40_CR2","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"40_CR3","first-page":"172","volume":"1302","author":"B. Boigelot","year":"1997","unstructured":"B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of QDDs. In Proc. 4th Int. Symp. Static Analysis, Paris, France, September 1997, volume 1302, pages 172\u2013186. Springer-Verlag, 1997.","journal-title":"Proc. 4th Int. Symp. Static Analysis, Paris, France, September 1997"},{"key":"40_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1007\/3-540-63165-8_211","volume-title":"Proc. 24th Int. Coll. Automata, Languages, and Programming (ICALP\u201997), Bologna, Italy, July 1997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani and P. Habermehl. Symbolic reachability analysis of FIFO channel systems with nonregular sets of configurations. In Proc. 24th Int. Coll. Automata, Languages, and Programming (ICALP\u201997), Bologna, Italy, July 1997, volume 1256 of Lecture Notes in Computer Science, pages 560\u2013570. Springer-Verlag, 1997."},{"key":"40_CR5","doi-asserted-by":"crossref","unstructured":"Janusz A. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11(4):481\u2013494, October 1964.","DOI":"10.1145\/321239.321249"},{"issue":"2","key":"40_CR6","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323\u2013342, April 1983.","journal-title":"Journal of the ACM"},{"key":"40_CR7","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual Symposium on Principles of Programming Languages, pages 238\u2013252. ACM SIGACT and SIGPLAN, ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"key":"40_CR8","unstructured":"G. C\u00e9c\u00e9. V\u00e9rification, analyse et approximations symboliques des automates communicants. Th\u00e8se ENS de Cachan, January 1998."},{"key":"40_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Proc. 10th Int. Conf. Computer Aided Verification (CAV\u201998), Vancouver, BC, Canada, June\u2013July 1998","author":"H. Comon","year":"1998","unstructured":"H. Comon and Y. Jurski. Multiple counters automata, safety analysis and Presburger arithmetic. In Proc. 10th Int. Conf. Computer Aided Verification (CAV\u201998), Vancouver, BC, Canada, June\u2013July 1998, volume 1427 of Lecture Notes in Computer Science, pages 268\u2013279. Springer, 1998."},{"key":"40_CR10","series-title":"Research Report LSV-2000-6","volume-title":"Lab. Specification and Verification","author":"A. Finkel","year":"2000","unstructured":"A. Finkel, S. P. Iyer, and G. Sutre. Well-abstracted transition systems: application to fifo automata. Research Report LSV-2000-6, Lab. Specification and Verification, ENS de Cachan, Cachan, France, June 2000."},{"key":"40_CR11","unstructured":"A. Finkel and O. Marc\u00e9. A minimal symbolic coverability graph for infinite-state comunicating automata. Technical report, LIFAC, 1996."},{"key":"40_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-46541-3_29","volume-title":"Proc. 17th Ann. Symp. Theoretical Aspects of Computer Science (STACS\u20192000), Lille, France, Feb. 2000","author":"A. Finkel","year":"2000","unstructured":"A. Finkel and G. Sutre. Decidability of reachability problems for classes of two counters automata. In Proc. 17th Ann. Symp. Theoretical Aspects of Computer Science (STACS\u20192000), Lille, France, Feb. 2000, volume 1770 of Lecture Notes in Computer Science, pages 346\u2013357. Springer, 2000."},{"issue":"1","key":"40_CR13","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/0304-3975(93)90212-C","volume":"113","author":"T. J\u00e9ron","year":"1993","unstructured":"Thierry J\u00e9ron and Claude Jard. Testing for unboundedness of fifo channels. Theoretical Computer Science, 113(1):93\u2013117, 1993.","journal-title":"Theoretical Computer Science"},{"key":"40_CR14","unstructured":"J. K. Pachl. Protocol description and analysis based on a state transition model with channel expressions. In Proc. of Protocol Specification, Testing and Verification, VII, 1987."},{"issue":"3","key":"40_CR15","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1145\/117009.117015","volume":"13","author":"Wuxu Peng","year":"1991","unstructured":"Wuxu Peng and S. Purushothaman. Data flow analysis of communicating finite state machines. ACM Transactions on Programming Languages and Systems, 13(3):399\u2013442, July 1991.","journal-title":"ACM Transactions on Programming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2000 \u2014 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44618-4_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T13:09:41Z","timestamp":1556802581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44618-4_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678977","9783540446187"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-44618-4_40","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}