Abstract
Two kinds of automata are introduced, for recognising regular and context-free nominal languages. We compare their expressive power with that of analogous proposals in the literature. Some properties of our languages are proved, in particular that emptiness of a context-free nominal language L is decidable, and that the intersection of L with a regular nominal language is still context-free. This paves the way for model-checking systems against access control properties in the nominal case, which is our main objective.
This work has been partially supported by the MIUR project Security Horizons, and by IST-FP7-FET open-IP project ASCENS.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bartoletti, M., Degano, P., Ferrari, G.L.: Planning and verifying service composition. JCS 17(5), 799–837 (2009)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Model checking usage policies. In: Kaklamanis, C., Nielson, F. (eds.) TGC 2008. LNCS, vol. 5474, pp. 19–35. Springer, Heidelberg (2009)
Benedikt, M., Ley, C., Puppis, G.: Automata vs. logics on data words. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 110–124. Springer, Heidelberg (2010)
Bojanczyk, M.: Data monoids. In: Dürr, C., Wilke, T. (eds.) STACS 2011, vol. 9, pp. 105–116. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2011)
Bojańczyk, M., Klin, B., Lasota, S.: Automata theory in nominal sets (2011), http://www.mimuw.edu.pl/~sl/PAPERS/lics11full.pdf
Bojanczyk, M., Klin, B., Lasota, S.: Automata with group actions. LICS, pp. 355–364. IEEE Computer Society, Washington, DC (2011)
Bollig, B.: An automaton over data words that captures EMSO logic. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 171–186. Springer, Heidelberg (2011)
Bollig, B., Cyriac, A., Gastin, P., Narayan Kumar, K.: Model checking languages of data words. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 391–405. Springer, Heidelberg (2012)
Cheng, E.Y.C., Kaminski, M.: Context-free languages over infinite alphabets. Acta Inf. 35(3), 245–267 (1998)
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–137. Springer, Heidelberg (2012)
Demri, S., Lazić, R., Nowak, D.: On the freeze quantifier in constraint ltl: Decidability and complexity. Information and Computation 205(1), 2–24 (2007)
Ferrari, G.L., Gnesi, S., Montanari, U., Pistore, M.: A model-checking verification environment for mobile processes. TOSEM 12(4), 440–473 (2003)
Gordon, A.D.: Notes on nominal calculi for security and mobility. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 262–330. Springer, Heidelberg (2001)
Grumberg, O., Kupferman, O., Sheinvald, S.: Variable automata over infinite alphabets. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 561–572. Springer, Heidelberg (2010)
Hazel, P.: Pcre: Perl compatible regular expressions (2005), http://www.pcre.org/pcre.txt
Kaminski, M., Francez, N.: Finite-memory automata. TCS 134(2), 329–363 (1994)
Kurz, A., Suzuki, T., Tuosto, E.: On nominal regular languages with binders. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 255–269. Springer, Heidelberg (2012)
Montanari, U., Pistore, M.: π-calculus, structured coalgebras, and minimal hd-automata. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 569–578. Springer, Heidelberg (2000)
Parys, P.: Higher-order pushdown systems with data. In: Faella, M., Murano, A. (eds.) GandALF. EPTCS, vol. 96, pp. 210–223 (2012)
Perrin, D., Pin, J.E.: Infinite words: automata, semigroups, logic and games. Pure and Applied Mathematics, vol. 141. Elsevier (2004)
Pitts, A.M.: Nominal sets names and symmetry in computer science: Names and symmetry in computer science. Cambridge Tracts in Theoretical Computer Science, vol. 57. Cambridge University Press
Pitts, A.M., Stark, I.D.B.: Observable properties of higher order functions that dynamically create local names, or what’s new? In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 122–141. Springer, Heidelberg (1993)
Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41–57. Springer, Heidelberg (2006)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332–344. IEEE Computer Society Press (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Degano, P., Ferrari, GL., Mezzetti, G. (2013). Towards Nominal Context-Free Model-Checking. In: Konstantinidis, S. (eds) Implementation and Application of Automata. CIAA 2013. Lecture Notes in Computer Science, vol 7982. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39274-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-39274-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39273-3
Online ISBN: 978-3-642-39274-0
eBook Packages: Computer ScienceComputer Science (R0)