{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T02:51:16Z","timestamp":1648867876786},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,2,23]],"date-time":"2016-02-23T00:00:00Z","timestamp":1456185600000},"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":["Acta Informatica"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s00236-016-0261-6","type":"journal-article","created":{"date-parts":[[2016,2,23]],"date-time":"2016-02-23T06:16:10Z","timestamp":1456208170000},"page":"399-433","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Regular and context-free nominal traces"],"prefix":"10.1007","volume":"54","author":[{"given":"Pierpaolo","family":"Degano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gian-Luigi","family":"Ferrari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianluca","family":"Mezzetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,2,23]]},"reference":[{"issue":"1","key":"261_CR1","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M Abadi","year":"1996","unstructured":"Abadi, M., Needham, R.M.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1), 6\u201315 (1996). doi: 10.1109\/32.481513","journal-title":"IEEE Trans. Softw. Eng."},{"key":"261_CR2","unstructured":"Amarilli, A., Jeanmougin, M.: A proof of the pumping lemma for context-free languages through pushdown automata (2012). arXiv:1207.2819"},{"issue":"4","key":"261_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.5381\/jot.2009.8.4.a1","volume":"8","author":"M Bartoletti","year":"2009","unstructured":"Bartoletti, M., Costa, G., Degano, P., Martinelli, F., Zunino, R.: Securing Java with local policies. JOT 8(4), 5\u201332 (2009)","journal-title":"JOT"},{"issue":"5","key":"261_CR4","doi-asserted-by":"publisher","first-page":"799","DOI":"10.3233\/JCS-2009-0357","volume":"17","author":"M Bartoletti","year":"2009","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: Planning and verifying service composition. JCS 17(5), 799\u2013837 (2009)","journal-title":"JCS"},{"issue":"1","key":"261_CR5","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/TSE.2007.70740","volume":"34","author":"M Bartoletti","year":"2008","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Semantics-based design for secure web services. IEEE Trans. Softw. Eng. 34(1), 33\u201349 (2008)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"261_CR6","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/1552309.1552313","volume":"31","author":"M Bartoletti","year":"2009","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Local policies for resource usage analysis. ACM Trans. Program. Lang. Syst. 31(6), 23 (2009)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"261_CR7","doi-asserted-by":"publisher","first-page":"710","DOI":"10.1017\/S096012951200093X","volume":"25","author":"M Bartoletti","year":"2015","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Model checking usage policies. Math. Struct. Comput. Sci. 25(3), 710\u2013763 (2015)","journal-title":"Math. Struct. Comput. Sci."},{"key":"261_CR8","unstructured":"Bartoletti, M., Zunino, R.: LocUsT: a tool for checking usage policies. Tech. Rep. TR08-07, University of Pisa (2008)"},{"key":"261_CR9","unstructured":"Belkhir, W., Chevalier, Y., Rusinowitch, M.: Guarded variable automata over infinite alphabets (2013). arXiv:1304.6297"},{"key":"261_CR10","unstructured":"Belkhir, W., Rossi, G., Rusinowitch, M.: A parametrized propositional dynamic logic with application to service synthesis. In: Advances in Modal Logic 10, invited and Contributed Papers from the Tenth Conference on \u201cAdvances in Modal Logic, Groningen, The Netherlands, 5\u20138 August 2014, pp. 34\u201353 (2014). http:\/\/www.aiml.net\/volumes\/volume10\/Belkhir-Rossi-Rusinowitch.pdf"},{"key":"261_CR11","doi-asserted-by":"publisher","unstructured":"Benedikt, M., Ley, C., Puppis, G.: Automata vs. logics on data words. In: Dawar, A., Veith, H. (eds.) CSL, LNCS, vol. 6247, pp. 110\u2013124. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-15205-4_12"},{"key":"261_CR12","unstructured":"Boja\u0144czyk, M., Klin, B., Lasota, S.: Automata theory in nominal sets (2011). http:\/\/www.mimuw.edu.pl\/sl\/PAPERS\/lics11full.pdf"},{"key":"261_CR13","doi-asserted-by":"publisher","unstructured":"Bojanczyk, M., Klin, B., Lasota, S.: Automata with group actions. In: LICS, pp. 355\u2013364. IEEE Computer Society, Washington, DC, USA (2011). doi: 10.1109\/LICS.2011.48","DOI":"10.1109\/LICS.2011.48"},{"key":"261_CR14","doi-asserted-by":"publisher","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, Berlin (2011)","DOI":"10.1007\/978-3-642-23217-6_12"},{"key":"261_CR15","doi-asserted-by":"publisher","unstructured":"Bollig, B., Cyriac, A., Gastin, P., Kumar, K.N.: Model checking languages of data words. In: Birkedal, L. (ed.) FOSSACS 2012, LNCS, vol. 7213, pp. 391\u2013405. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28729-9_26"},{"key":"261_CR16","doi-asserted-by":"publisher","unstructured":"Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking message-passing programs. In: Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16\u201318, 2002, pp. 45\u201357 (2002)","DOI":"10.1145\/503272.503278"},{"issue":"3","key":"261_CR17","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s002360050120","volume":"35","author":"EYC Cheng","year":"1998","unstructured":"Cheng, E.Y.C., Kaminski, M.: Context-free languages over infinite alphabets. Acta Inf. 35(3), 245\u2013267 (1998)","journal-title":"Acta Inf."},{"key":"261_CR18","unstructured":"Ciancia, V., Tuosto, E.: A novel class of automata for languages on infinite alphabets. Tech. rep., CS-09-003, University of Leicester, UK (2009)"},{"key":"261_CR19","doi-asserted-by":"publisher","unstructured":"Degano, P., Ferrari, G.L., Mezzetti, G.: Nominal automata for resource usage control. In: Moreira, N., Reis, R. (eds.) CIAA 2012, LNCS, vol. 7381, pp. 125\u2013137. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31606-7_11"},{"key":"261_CR20","unstructured":"Dierks, T., Rescorla, E.: RFC 5246: The Transport Layer Security (TLS) Protocol Version 1.2 (2008). http:\/\/tools.ietf.org\/html\/rfc5246"},{"issue":"6","key":"261_CR21","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/777313.777335","volume":"46","author":"C Ferris","year":"2003","unstructured":"Ferris, C., Farrell, J.: What are web services? Commun. ACM 46(6), 31 (2003). doi: 10.1145\/777313.777335","journal-title":"Commun. ACM"},{"issue":"3","key":"261_CR22","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M Gabbay","year":"2002","unstructured":"Gabbay, M., Pitts, A.: A new approach to abstract syntax with variable binding. Form. Asp. Comput. 13(3), 341\u2013363 (2002)","journal-title":"Form. Asp. Comput."},{"issue":"4","key":"261_CR23","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1038\/scientificamerican1004-76","volume":"291","author":"N Gershenfeld","year":"2004","unstructured":"Gershenfeld, N., Krikorian, R., Cohen, D.: The internet of things. Sci. Am. 291(4), 76 (2004)","journal-title":"Sci. Am."},{"key":"261_CR24","doi-asserted-by":"publisher","unstructured":"Gong, Z., Gu, X., Wilkes, J.: PRESS: predictive elastic resource scaling for cloud systems. In: Proceedings of the 6th International Conference on Network and Service Management, CNSM 2010, Niagara Falls, Canada, October 25\u201329, 2010, pp. 9\u201316 (2010). doi: 10.1109\/CNSM.2010.5691343","DOI":"10.1109\/CNSM.2010.5691343"},{"key":"261_CR25","doi-asserted-by":"publisher","unstructured":"Gordon, A.D.: Notes on nominal calculi for security and mobility. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000, LNCS, vol. 2171, pp. 262\u2013330. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45608-2_5"},{"key":"261_CR26","doi-asserted-by":"publisher","unstructured":"Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: Tools and Algorithms for the Construction and Analysis of Systems\u201419th International Conference, TACAS 2013, Lecture Notes in Computer Science, vol. 7795, pp. 260\u2013276. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-36742-7_19"},{"key":"261_CR27","doi-asserted-by":"publisher","unstructured":"Grumberg, O., Kupferman, O., Sheinvald, S.: Variable automata over infinite alphabets. In: Dediu, A.H., Fernau, H., Mart\u00edn-Vide, C. (eds.) LATA, LNCS, vol. 6031, pp. 561\u2013572. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-13089-2_47"},{"key":"261_CR28","doi-asserted-by":"publisher","unstructured":"Jensen, T.P., M\u00e9tayer, D.L., Thorn, T.: Verification of control flow based security properties. In: 1999 IEEE Symposium on Security and Privacy, Oakland, California, USA, May 9\u201312, 1999, pp. 89\u2013103 (1999)","DOI":"10.1109\/SECPRI.1999.766902"},{"issue":"2","key":"261_CR29","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. TCS 134(2), 329\u2013363 (1994)","journal-title":"TCS"},{"issue":"5","key":"261_CR30","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1142\/S0129054110007532","volume":"21","author":"M Kaminski","year":"2010","unstructured":"Kaminski, M., Zeitlin, D.: Finite-memory automata with non-deterministic reassignment. Int. J. Found. Comput. Sci. 21(5), 741\u2013760 (2010)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"261_CR31","doi-asserted-by":"publisher","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, Berlin (2012)","DOI":"10.1007\/978-3-642-28729-9_17"},{"key":"261_CR32","unstructured":"Kurz, A., Suzuki, T., Tuosto, E.: Nominal regular expressions for languages over infinite alphabets. Extended abstract (2013). arXiv:1310.7093"},{"key":"261_CR33","doi-asserted-by":"publisher","unstructured":"Manuel, A., Muscholl, A., Puppis, G.: Walking on data words. In: Mogens, N., Branislav, R. (eds.) Computer Science-Theory and Applications, pp. 64\u201375. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38536-0_6"},{"key":"261_CR34","unstructured":"Mezzetti, G.: Nominal context-free behaviour. Ph.D. thesis, University of Pisa (2014)"},{"key":"261_CR35","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs, NJ (1967)"},{"key":"261_CR36","doi-asserted-by":"crossref","unstructured":"Montanari, U., Pistore, M.: $$\\pi $$ \u03c0 -calculus, structured coalgebras, and minimal hd-automata. In: Mogens, N., Branislav, R. (eds.) MFCS 2000, LNCS, vol. 1893, pp. 569\u2013578. Springer, Berlin (2000)","DOI":"10.1007\/3-540-44612-5_52"},{"key":"261_CR37","doi-asserted-by":"publisher","unstructured":"Murawski, A.S., Ramsay, S.J., Tzevelekos, N.: Reachability in pushdown register automata. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25\u201329, 2014. Proceedings, Part I, Lecture Notes in Computer Science, vol. 8634, pp. 464\u2013473. Springer, Berlin (2014). doi: 10.1007\/978-3-662-44522-8_39","DOI":"10.1007\/978-3-662-44522-8_39"},{"key":"261_CR38","first-page":"560","volume":"2001","author":"F Neven","year":"2001","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Towards regular languages over infinite alphabets. Math. Found. Comput. Sci. 2001, 560\u2013572 (2001)","journal-title":"Math. Found. Comput. Sci."},{"issue":"3","key":"261_CR39","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F Neven","year":"2004","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log. (TOCL) 5(3), 403\u2013435 (2004)","journal-title":"ACM Trans. Comput. Log. (TOCL)"},{"key":"261_CR40","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, 1st ed. 1999. corr. 2nd printing, 1999 edn. Springer, Berlin (2005)","DOI":"10.1007\/978-3-662-03811-6_1"},{"key":"261_CR41","unstructured":"Papazoglou, M.P.: Web Services\u2014Principles and Technology. Prentice Hall, Englewood Cliffs (2008). http:\/\/vig.pearsoned.com\/store\/product\/1%2C1207%2Cstore-12521_isbn-0321155556%2C00.html"},{"key":"261_CR42","doi-asserted-by":"publisher","unstructured":"Parys, P.: Higher-order pushdown systems with data. In: Faella, M., Murano, A. (eds.) GandALF, EPTCS, vol. 96, pp. 210\u2013223 (2012)","DOI":"10.4204\/EPTCS.96.16"},{"key":"261_CR43","unstructured":"Perrin, D., Pin, J.: Infinite words: automata, semigroups, logic and games. Pure Appl. Math. 141 (2004)"},{"key":"261_CR44","doi-asserted-by":"publisher","unstructured":"Pitts, A.M., Stark, I.D.B.: Observable properties of higher order functions that dynamically create local names, or what\u2019s new? In: Andrzej, M.B., Stefan, S. (eds.) MFCS 1993, LNCS, vol. 711, pp. 122\u2013141. Springer, Berlin (1993)","DOI":"10.1007\/3-540-57182-5_8"},{"issue":"1","key":"261_CR45","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. (TISSEC) 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"issue":"2","key":"261_CR46","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1017\/S0956796807006466","volume":"18","author":"C Skalka","year":"2008","unstructured":"Skalka, C., Smith, S.F., Horn, D.V.: Types and trace effects of higher order programs. J. Funct. Program. 18(2), 179\u2013249 (2008)","journal-title":"J. Funct. Program."},{"issue":"1","key":"261_CR47","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1145\/1925844.1926420","volume":"46","author":"N Tzevelekos","year":"2011","unstructured":"Tzevelekos, N.: Fresh-register automata. ACM SIGPLAN Not. 46(1), 295\u2013306 (2011)","journal-title":"ACM SIGPLAN Not."},{"key":"261_CR48","doi-asserted-by":"publisher","unstructured":"Tzevelekos, N., Grigore, R.: History-register automata. In: Pfenning, F. (ed.) Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16\u201324, 2013. Proceedings, vol. 7794, pp. 17\u201333. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-37075-5_2"},{"key":"261_CR49","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332\u2013344. IEEE Computer Society (1986)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0261-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0261-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0261-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0261-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,4]],"date-time":"2019-09-04T21:58:15Z","timestamp":1567634295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0261-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,23]]},"references-count":49,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["261"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0261-6","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,23]]}}}