{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:17:24Z","timestamp":1725484644733},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434009"},{"type":"electronic","value":"9783540459958"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45995-2_36","type":"book-chapter","created":{"date-parts":[[2007,5,29]],"date-time":"2007-05-29T22:33:34Z","timestamp":1180478014000},"page":"400-414","source":"Crossref","is-referenced-by-count":0,"title":["Verification of Embedded Reactive Fiffo Systems"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Herbreteau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franck","family":"Cassez","sequence":"additional","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":"Gr\u00e9goire","family":"Sutre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"36_CR1","doi-asserted-by":"crossref","unstructured":"P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 160\u2013170. IEEE Computer Society Press, 1993.","DOI":"10.1109\/LICS.1993.287591"},{"key":"36_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-58201-0_78","volume-title":"Undecidable veri.cation problems for programs with unreliable channels","author":"P. Abdulla","year":"1994","unstructured":"P. Abdulla and B. Jonsson. Undecidable veri.cation problems for programs with unreliable channels. In S. Abiteboul and E. Shamir, editors, Automata, Languages and Programming, 21st International Colloquium, volume 820 of Lecture Notes in Computer Science, pages 316\u2013327, Jerusalem, Israel, 11\u201314 July 1994. Springer-Verlag."},{"issue":"1-2","key":"36_CR3","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"Parosh Aziz Abdulla","year":"2000","unstructured":"P. A. Abdulla, K. \u010cer\u0101ns, B. Jonsson, and Y-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. INFCTRL: Information and Computation (formerly Information and Control), 160, 2000.","journal-title":"Information and Computation"},{"key":"36_CR4","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. 8th Int. Conf. Concurrency Theory (CONCUR\u201997), Warsaw, Poland, Jul. 1997, volume 1243 of Lecture Notes in omputer Science, pages 135\u2013150. Springer, 1997.","DOI":"10.1007\/3-540-63141-0_10"},{"key":"36_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-49116-3_30","volume-title":"Model checking lossy vector addition systems","author":"A. Bouajjani","year":"1999","unstructured":"A. Bouajjani and R. Mayr. Model checking lossy vector addition systems. In Proc. 16th Ann. Symp. Theoretical Aspects of Computer Science (STACS\u201999), Trier, Germany, Mar. 1999, volume 1563 of Lecture Notes in Computer Science, pages 323\u2013333. Springer, 1999."},{"issue":"2","key":"36_CR6","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. Journal of the ACM, 30(2):323\u2013342, April 1983.","journal-title":"Journal of the ACM"},{"issue":"2","key":"36_CR7","doi-asserted-by":"publisher","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 J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, 1992.","journal-title":"Information and Computation"},{"issue":"1","key":"36_CR8","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/0304-3975(94)00136-7","volume":"146","author":"F. Cassez","year":"1995","unstructured":"F. Cassez and O. Roux. Compilation of the ELECTRE reactive language into finite transition systems. Theoretical Computer Science, 146(1\u20132):109\u2013143, 24 July 1995.","journal-title":"Theoretical Computer Science"},{"key":"36_CR9","unstructured":"CCITT. Recommendation Z.100: Specification and Description Language SDL, blue book, volume x.1 edition, 1988."},{"key":"36_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/3-540-48523-6_27","volume-title":"Boundedness of Reset P\/T nets","author":"C. Dufourd","year":"1999","unstructured":"C. Dufourd, P. Jan\u010dar, and Ph. Schnoebelen. Boundedness of Reset P\/T nets. In Proc. 26th Int. Coll. Automata, Languages, and Programming (ICALP\u201999), Prague, Czech Republic, July 1999, volume 1644 of Lecture Notes in Computer Science, pages 301\u2013310. Springer, 1999."},{"key":"36_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-18088-5_43","volume-title":"A generalization of the procedure of Karp and Miller to well structured transition systems","author":"A. Finkel","year":"1987","unstructured":"A. Finkel. A generalization of the procedure of Karp and Miller to well structured transition systems. In Thomas Ottmann, editor, Proceedings of the 14th International Colloquium on Automata, Languages, and Programming, volume 267 of LNCS, pages 499\u2013508, Karlsruhe, FRG, July 1987. Berlin: Springer."},{"issue":"2","key":"36_CR12","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0890-5401(90)90009-7","volume":"89","author":"A. Finkel","year":"1990","unstructured":"A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89(2):144\u2013179, December 1990.","journal-title":"Information and Computation"},{"issue":"1","key":"36_CR13","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(1\u20132):217\u2013230, 15 March 1997.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"36_CR14","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"A. Finkel and Ph. Schnoebelen. Well structured transition systems everywhere! Theoretical Computer Science, 256(1\u20132):63\u201392, 2001.","journal-title":"Theoretical Computer Science"},{"key":"36_CR15","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In Proc. 2nd Int. Workshop on Verification of Infinite State Systems (INFINITY\u201997), Bologna, Italy, July 1997, volume 9 of Electronic Notes in Theor. Comp. Sci., pages 30\u201340. Elsevier Science, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"issue":"1","key":"36_CR16","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"s3-2","author":"Graham Higman","year":"1952","unstructured":"G. Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society (3), 2(7):326\u2013336, September 1952.","journal-title":"Proceedings of the London Mathematical Society"},{"issue":"1","key":"36_CR17","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(1):93\u2013117, 1993.","journal-title":"Theoretical Computer Science"},{"key":"36_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/3-540-63371-5_6","volume-title":"A formal framework for the analysis of recursive-parallel programs","author":"O. Kushnarenko","year":"1997","unstructured":"O. Kushnarenko and Ph. Schnoebelen. A formal framework for the analysis of recursive-parallel programs. Lecture Notes in Computer Science, 1277:45\u2013--, 1997."},{"key":"36_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Undecidable problems in unreliable computations","author":"R. Mayr","year":"2000","unstructured":"R. Mayr. Undecidable problems in unreliable computations. In International Symposium on Latin American Theoretical Informatics (LATIN\u20192000), volume 1776 of Lecture Notes in Computer Science, Punta del Este, Uruguay, 2000. Springer-Verlag."},{"key":"36_CR20","volume-title":"Computation: Finite and Infinite Machines","author":"M. L. Minsky","year":"1967","unstructured":"M. L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, London, 1 edition, 1967.","edition":"1 edition"},{"issue":"4","key":"36_CR21","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"R. J. Parikh","year":"1966","unstructured":"R. J. Parikh. On context-free languages. Journal of the ACM, 13(4):570\u2013581, October 1966.","journal-title":"Journal of the ACM"},{"key":"36_CR22","series-title":"Lect Notes Comput Sci","first-page":"106","volume-title":"Effective recognizability and model checking of reactive fiffo automata","author":"G. Sutre","year":"1999","unstructured":"G. Sutre, A. Finkel, O. Roux, and F. Cassez. Effective recognizability and model checking of reactive fiffo automata. In Proc. 7th Int. Conf. Algebraic Methodology and Software Technology (AMAST\u201998), Amazonia, Brazil, Jan. 1999, volume 1548 of Lecture Notes in Computer Science, pages 106\u2013123. Springer, 1999."}],"container-title":["Lecture Notes in Computer Science","LATIN 2002: Theoretical Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45995-2_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T08:30:20Z","timestamp":1556440220000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45995-2_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434009","9783540459958"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-45995-2_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2002]]}}}