Abstract
Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic formalism for modelling and analysing such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability for reachability checks. The distinctive feature of our machines is their use of unbounded memory sets (histories) where input symbols can be selectively stored and compared with symbols to follow. In addition, stored symbols can be consumed or deleted by reset. We show that the combination of consumption and reset capabilities renders the automata powerful enough to imitate counter machines (Petri nets with reset arcs), and yields closure under all regular operations apart from complementation. We moreover examine weaker notions of HRAs which strike different balances between expressiveness and effectiveness.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S., Ghica, D.R., Murawski, A.S., Ong, C.-H.L., Stark, I.D.B.: Nominal games and full abstraction for the nu-calculus. In: LICS, pp. 150–159 (2004)
Araki, T., Kasami, T.: Some decision problems related to the reachability problem for Petri nets. Theor. Comput. Sci. 3(1), 85–104 (1977)
Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Meth. Comput. Sci. 7(4) (2011)
Benton, N., Leperchey, B.: Relational Reasoning in a Nominal Semantics for Storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 86–101. Springer, Heidelberg (2005)
Björklund, H., Schwentick, T.: On notions of regularity for data languages. TCS 411 (2010)
Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: LICS, pp. 7–16 (2006)
Bouajjani, A., Fratani, S., Qadeer, S.: Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 207–220. Springer, Heidelberg (2007)
Ciardo, G.: Petri Nets with Marking-Dependent Arc Cardinality. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 179–198. Springer, Heidelberg (1994)
Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. TOCL 10(3) (2009)
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset Nets Between Decidability and Undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)
Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson’s lemma. In: LICS, pp. 269–278 (2011)
Finkel, A., Sangnier, A.: Mixing Coverability and Reachability to Analyze VASS with One Zero-Test. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol. 5901, pp. 394–406. Springer, Heidelberg (2010)
Gabbay, M., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Asp. Comput. 13(3-5), 341–363 (2002)
Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: TACAS (to appear 2013)
Jancar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci. 148(2), 281–301 (1995)
Jeffrey, A., Rathke, J.: Towards a theory of bisimulation for local names. In: LICS (1999)
Kaiser, A., Kroening, D., Wahl, T.: Efficient Coverability Analysis by Proof Minimization. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 500–515. Springer, Heidelberg (2012), http://www.cprover.org/bfc/
Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2) (1994)
Laird, J.: A Fully Abstract Trace Semantics for General References. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 667–679. Springer, Heidelberg (2007)
Lazic, R., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Inform. 88(3), 251–274 (2008)
Lipton, R.: The reachability problem requires exponential space. Tech. Rep. 62, Yale (1976)
Manuel, A., Ramanujam, R.: Class counting automata on datawords. Int. J. Found. Comput. Sci. 22(4), 863–882 (2011)
Montanari, U., Pistore, M.: An introduction to History Dependent Automata. Electr. Notes Theor. Comput. Sci. 10 (1997)
Murawski, A.S., Tzevelekos, N.: Algorithmic Nominal Game Semantics. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 419–438. Springer, Heidelberg (2011)
Murawski, A.S., Tzevelekos, N.: Algorithmic Games for Full Ground References. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 312–324. Springer, Heidelberg (2012)
Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic 5(3), 403–435 (2004)
Pitts, A.M., Stark, I.: 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)
Rackoff, C.: The covering and boundedness problems for vector addition systems. TCS (1978)
Rosier, L.E., Yen, H.-C.: A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci. 32(1), 105–135 (1986)
Schnoebelen, P.: Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)
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)
Stark, I.: Names and higher-order functions. PhD thesis, University of Cambridge (1994)
Tzevelekos, N.: Fresh-register automata. In: POPL, pp. 295–306 (2011)
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
Tzevelekos, N., Grigore, R. (2013). History-Register Automata. In: Pfenning, F. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2013. Lecture Notes in Computer Science, vol 7794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37075-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-37075-5_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37074-8
Online ISBN: 978-3-642-37075-5
eBook Packages: Computer ScienceComputer Science (R0)