{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:45:29Z","timestamp":1725486329748},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540654629"},{"type":"electronic","value":"9783540492535"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49253-4_10","type":"book-chapter","created":{"date-parts":[[2007,6,7]],"date-time":"2007-06-07T02:56:45Z","timestamp":1181185005000},"page":"106-123","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Effective Recognizability and Model Checking of Reactive Fiffo Automata"],"prefix":"10.1007","author":[{"given":"Gregoire","family":"Sutre","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Finkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier","family":"Roux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franck","family":"Cassez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,1,15]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy fifo channels. In Proc. of the 10th Conference on Computer-Aided Verification (CAV), 1998.","DOI":"10.1007\/BFb0028754"},{"key":"10_CR2","unstructured":"P. Adulla and B. Jonsson. Verifying programs with unreliable channels. In Proc. of the 8\n                           th\n                           IEEE Symposium on Logic in Computer Science, 1993."},{"key":"10_CR3","unstructured":"F. Boniol, A. Burgue\u00f1o, O. Roux, and V. Rusu. \u00c9tude d\u2019un mod\u00e9le hybride discret-continu pour la sp\u00e9cification de syst\u00e9mes temps-r\u00e9el embarqu\u00e9s. Rapport de contrat CERT\/ONERA-IRCyN N0 DERI 3703-33, February 1998."},{"key":"10_CR4","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proc. of the 8th Conference on Computer-Aided Verification (CAV)","author":"B. Boigelot","year":"1996","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using qdds. In Proc. of the 8th Conference on Computer-Aided Verification (CAV), volume 1102, pages 1\u201312. LNCS, August 1996."},{"key":"10_CR5","unstructured":"B. Boigelot, P. Godefroid, B. Willems, and P. Wolper. The power of qdds. In Proceedings of SAS\u201997, September 1997."},{"key":"10_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1007\/3-540-63165-8_211","volume-title":"Proc. of the 24th International Colloquium on Automata, Languages, and Programming (ICALP)","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani and P. Habermehl. Symbolic reachability analysis of FIFOchannel systems with nonregular sets of configurations. In Proc. of the 24th International Colloquium on Automata, Languages, and Programming (ICALP), volume 1256, pages 560\u2013570. LNCS, July 1997."},{"issue":"2","key":"10_CR7","doi-asserted-by":"publisher","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. JACM, 30(2):323\u2013342, 1983.","journal-title":"JACM"},{"key":"10_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/3-540-63166-6_31","volume-title":"Proc. of the 9th Conference on Computer-Aided Verification (CAV)","author":"G. C\u00e9c\u00e9","year":"1997","unstructured":"G. C\u00e9c\u00e9 and A. Finkel. Programs with quasi-stable channels are effectively recognizable. In Proc. of the 9th Conference on Computer-Aided Verification (CAV), volume 1254, pages 304\u2013315. LNCS, June 1997."},{"issue":"1","key":"10_CR9","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1006\/inco.1996.0003","volume":"124","author":"G. C\u00e9c\u00e9","year":"1996","unstructured":"G. C\u00e9c\u00e9, A. Finkel, and I. S. Purushothaman. Unreliable channels are easier to verify than perfect channels. Information and Computation, 124(1):20\u201331, 1996.","journal-title":"Information and Computation"},{"issue":"10","key":"10_CR10","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1145\/362759.362813","volume":"14","author":"P. J. Courtois","year":"1971","unstructured":"P. J. Courtois, F. Heymans, and D. L. Parnas. Concurrent control with \u201creaders\u201d and \u201cwriters\u201d. Communications of the ACM, 14(10):667\u2013668, October 1971.","journal-title":"Communications of the ACM"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"F. Cassez and O. Roux. Compilation of the Electre reactive language into finite transition systems. Theoretical Computer Science, 146(1-2):109\u2013143, July 1995.","DOI":"10.1016\/0304-3975(94)00136-7"},{"key":"10_CR12","unstructured":"F. Cassez and O. Roux. Modelling and verifying reactive systems with event memorisation. Revised version submitted, 1997."},{"key":"10_CR13","unstructured":"E. A. Emerson. Handbook of Theoretical Computer Science, chapter 16, pages 996\u20131072. Elsevier Science Publishers, 1990."},{"key":"10_CR14","unstructured":"A. Finkel and A. Choquet. Simulation of linear fifo nets by petri nets having a structured set of terminal markings. In Proc. of the 8th European Workshop on Application and Theory of Petri Nets, Saragoza, pages 95\u2013112, 1987."},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/S0304-3975(96)00026-6","volume":"174","author":"A. Finkel","year":"1997","unstructured":"A. Finkel and P. McKenzie. Verifying identical communicating processes is undecidable. Theoretical Computer Science, 174:217\u2013230, 1997.","journal-title":"Theoretical Computer Science"},{"key":"10_CR16","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/0304-3975(93)90212-C","volume":"113","author":"T. J\u00e9ron","year":"1993","unstructured":"T. J\u00e9ron and C. Jard. Testing for unboundedness of fifo channels. Theoretical Computer Science, 113:93\u2013117, 1993.","journal-title":"Theoretical Computer Science"},{"key":"10_CR17","unstructured":"L. Lamport. What good is temporal logic? In Information Processing\u201983. Proc. IFIP 9th World Computer Congress, pages 657\u2013668. North-Holland, September 1983."},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"10_CR19","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."},{"key":"10_CR20","series-title":"PhD thesis","volume-title":"V\u00e9rification de protocoles \u00e1 espace d\u2019\u00e9tats infini repr\u00e9sentable par une grammaire de graphes","author":"Y. M. Quemener","year":"1996","unstructured":"Y. M. Quemener. V\u00e9rification de protocoles \u00e1 espace d\u2019\u00e9tats infini repr\u00e9sentable par une grammaire de graphes. PhD thesis, Universit\u00e9 de Rennes 1 (FRANCE), 1996."},{"issue":"3","key":"10_CR21","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1985","unstructured":"A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733\u2013749, 1985.","journal-title":"Journal of the ACM"},{"key":"10_CR22","unstructured":"G. Sutre. V\u00e9rification de propri\u00e9t\u00e9s sur les automates \u00e1 file r\u00e9actifs produits par compilation de programmes Electre. M\u00e9moire de DEA, Univ. Paris VII et Ecole Polytechnique, 1997."}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49253-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:48:46Z","timestamp":1558273726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49253-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540654629","9783540492535"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-49253-4_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"15 January 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}