{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T18:40:05Z","timestamp":1747248005486,"version":"3.40.5"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662459164"},{"type":"electronic","value":"9783662459171"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-45917-1_7","type":"book-chapter","created":{"date-parts":[[2014,12,22]],"date-time":"2014-12-22T14:34:17Z","timestamp":1419258857000},"page":"97-111","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Class of Automata for the Verification of Infinite, Resource-Allocating Behaviours"],"prefix":"10.1007","author":[{"given":"Vincenzo","family":"Ciancia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Sammartino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,12,23]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Ciancia, V., Sammartino, M.: A class of automata for the verification of infinite, resource-allocating behaviours - extended version. CoRR abs\/1310.3945 (2014)","DOI":"10.1007\/978-3-662-45917-1_7"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Schlingloff, B.H.: Model checking. In: Handbook of Automated Reasoning, pp. 1635\u20131790. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66\u201392 (1960)","journal-title":"Z. Math. Logik Grundl. Math."},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1090\/S0002-9947-1961-0139530-9","volume":"98","author":"CC Elgot","year":"1961","unstructured":"Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc. 98, 21\u201351 (1961)","journal-title":"Trans. Amer. Math. Soc."},{"issue":"1","key":"7_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I\/II. Inf. Comput. 100(1), 1\u201377 (1992)","journal-title":"I\/II. Inf. Comput."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Fiore, M.P., Turi, D.: Semantics of name and value passing. In: LICS 2001, pp. 93\u2013104. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932486"},{"issue":"2","key":"7_CR7","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-011-9224-3","volume":"49","author":"F Bonchi","year":"2012","unstructured":"Bonchi, F., Buscemi, M.G., Ciancia, V., Gadducci, F.: A presheaf environment for the explicit fusion calculus. J. Autom. Reasoning 49(2), 161\u2013183 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/j.entcs.2008.10.017","volume":"218","author":"M Miculan","year":"2008","unstructured":"Miculan, M.: A categorical model of the fusion calculus. Electr. Not. Theor. Comp. Sci. 218, 275\u2013293 (2008)","journal-title":"Electr. Not. Theor. Comp. Sci."},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.entcs.2004.02.027","volume":"106","author":"N Ghani","year":"2004","unstructured":"Ghani, N., Yemane, K., Victor, B.: Relationally staged computations in calculi of mobile processes. Electr. Not. Theor. Comp. Sci. 106, 105\u2013120 (2004)","journal-title":"Electr. Not. Theor. Comp. Sci."},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/j.tcs.2014.03.009","volume":"546","author":"U Montanari","year":"2014","unstructured":"Montanari, U., Sammartino, M.: A network-conscious $$\\pi $$-calculus and its coalgebraic semantics. Theor. Comput. Sci. 546, 188\u2013224 (2014)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"7_CR11","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1016\/j.tcs.2005.03.014","volume":"340","author":"U Montanari","year":"2005","unstructured":"Montanari, U., Pistore, M.: Structured coalgebras and minimal hd-automata for the $$\\pi $$-calculus. Theor. Comput. Sci. 340(3), 539\u2013576 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Bojanczyk, M., Klin, B., Lasota, S.: Automata with group actions. In: LICS 2011, pp. 355\u2013364. IEEE Computer Society (2011)","DOI":"10.1109\/LICS.2011.48"},{"issue":"2\u20133","key":"7_CR13","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/s10990-006-8749-3","volume":"19","author":"F Gadducci","year":"2006","unstructured":"Gadducci, F., Miculan, M., Montanari, U.: About permutation algebras, (pre)sheaves and named sets. Higher-Ord. Symb. Comp. 19(2\u20133), 283\u2013304 (2006)","journal-title":"Higher-Ord. Symb. Comp."},{"issue":"4","key":"7_CR14","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1016\/j.ic.2005.08.004","volume":"204","author":"MP Fiore","year":"2006","unstructured":"Fiore, M.P., Staton, S.: Comparing operational models of name-passing process calculi. Inf. Comput. 204(4), 524\u2013560 (2006)","journal-title":"Inf. Comput."},{"issue":"2","key":"7_CR15","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.entcs.2010.07.014","volume":"264","author":"V Ciancia","year":"2010","unstructured":"Ciancia, V., Kurz, A., Montanari, U.: Families of symmetries as efficient models of resource binding. Electr. Not. Theor. Comp. Sci. 264(2), 63\u201381 (2010)","journal-title":"Electr. Not. Theor. Comp. Sci."},{"issue":"12","key":"7_CR16","doi-asserted-by":"publisher","first-page":"1349","DOI":"10.1016\/j.ic.2009.10.007","volume":"208","author":"V Ciancia","year":"2010","unstructured":"Ciancia, V., Montanari, U.: Symmetries, local names and dynamic (de)-allocation of names. Inf. Comput. 208(12), 1349\u20131367 (2010)","journal-title":"Inf. Comput."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Tzevelekos, N.: Fresh-register automata. In: POPL 2011, pp. 295\u2013306. ACM (2011)","DOI":"10.1145\/1925844.1926420"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-642-28729-9_17","volume-title":"Foundations of Software Science and Computational Structures","author":"A Kurz","year":"2012","unstructured":"Kurz, A., Suzuki, T., Tuosto, E.: On nominal regular languages with binders. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 255\u2013269. Springer, Heidelberg (2012)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-19805-2_25","volume-title":"Foundations of Software Science and Computational Structures","author":"MJ Gabbay","year":"2011","unstructured":"Gabbay, M.J., Ciancia, V.: Freshness and name-restriction in sets of traces with names. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 365\u2013380. Springer, Heidelberg (2011)"},{"issue":"2","key":"7_CR20","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1006\/inco.1995.1070","volume":"118","author":"O Maler","year":"1995","unstructured":"Maler, O., Pnueli, A.: On the learnability of infinitary regular sets. Inf. Comput. 118(2), 316\u2013326 (1995)","journal-title":"Inf. Comput."},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-78800-3_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Farzan","year":"2008","unstructured":"Farzan, A., Chen, Y.-F., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Extending automated compositional verification to the full class of omega-regular languages. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 2\u201317. Springer, Heidelberg (2008)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-32784-1_6","volume-title":"Coalgebraic Methods in Computer Science","author":"V Ciancia","year":"2012","unstructured":"Ciancia, V., Venema, Y.: Stream automata are coalgebras. In: Pattinson, D., Schr\u00f6der, L. (eds.) CMCS 2012. LNCS, vol. 7399, pp. 90\u2013108. Springer, Heidelberg (2012)"},{"issue":"3\u20135","key":"7_CR23","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M Gabbay","year":"2002","unstructured":"Gabbay, M., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Asp. Comput. 13(3\u20135), 341\u2013363 (2002)","journal-title":"Formal Asp. Comput."},{"key":"7_CR24","unstructured":"Pistore, M.: History Dependent Automata. PhD thesis, University of Pisa (1999)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"554","DOI":"10.1007\/3-540-58027-1_27","volume-title":"Mathematical Foundations of Programming Semantics","author":"H Calbrix","year":"1994","unstructured":"Calbrix, H., Nivat, M., Podelski, A.: Ultimately periodic words of rational w-languages. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 554\u2013556. Springer, Heidelberg (1994)"},{"key":"7_CR26","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: 1960 International Congress on Logic, Methodology and Philosophy of Science, pp. 1\u201311. Stanford University Press (1962)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Johansson, M., Parrow, J., Victor, B.: Psi-calculi: a framework for mobile processes with nominal data and logic. LMCS 7(1) (2011)","DOI":"10.2168\/LMCS-7(1:11)2011"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-642-39992-3_3","volume-title":"Logic, Language, Information, and Computation","author":"M Boja\u0144czyk","year":"2013","unstructured":"Boja\u0144czyk, M.: Modelling infinite structures with atoms. In: Libkin, L., Kohlenbach, U., de Queiroz, R. (eds.) WoLLIC 2013. LNCS, vol. 8071, pp. 13\u201328. Springer, Heidelberg (2013)"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"V\u00e4\u00e4n\u00e4nen, J.A.: Dependence Logic - A New Approach to Independence Friendly Logic. London Mathematical Society student texts, vol. 70. Cambridge University Press (2007)","DOI":"10.1017\/CBO9780511611193"},{"key":"7_CR30","unstructured":"Galliani, P.: The Dynamics of Imperfect Information. PhD thesis, University of Amsterdam (September 2012)"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)","DOI":"10.1145\/1507244.1507246"},{"issue":"2","key":"7_CR32","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/1877714.1877716","volume":"12","author":"R Lazic","year":"2011","unstructured":"Lazic, R.: Safety alternating automata on data words. ACM Trans. Comput. Log. 12(2), 10 (2011)","journal-title":"ACM Trans. Comput. Log."},{"issue":"4","key":"7_CR33","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/1970398.1970403","volume":"12","author":"M Bojanczyk","year":"2011","unstructured":"Bojanczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Log. 12(4), 27 (2011)","journal-title":"ACM Trans. Comput. Log."},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-28332-1_30","volume-title":"Language and Automata Theory and Applications","author":"A Kara","year":"2012","unstructured":"Kara, A., Schwentick, T., Tan, T.: Feasible automata for two-variable logic with successor on data words. In: Dediu, A.-H., Mart\u00edn-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 351\u2013362. Springer, Heidelberg (2012)"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-23217-6_12","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B Bollig","year":"2011","unstructured":"Bollig, B.: An automaton over data words that captures emso logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 171\u2013186. Springer, Heidelberg (2011)"},{"key":"7_CR36","unstructured":"Kara, A., Tan, T.: Extending B\u00fcchi automata with constraints on data values. CoRR abs\/1012.5439 (2010)"},{"key":"7_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-642-13089-2_47","volume-title":"Language and Automata Theory and Applications","author":"O Grumberg","year":"2010","unstructured":"Grumberg, O., Kupferman, O., Sheinvald, S.: Variable automata over infinite alphabets. In: Dediu, A.-H., Fernau, H., Mart\u00edn-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 561\u2013572. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45917-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T18:14:28Z","timestamp":1747246468000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/10.1007\/978-3-662-45917-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662459164","9783662459171"],"references-count":37,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-662-45917-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"23 December 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}