Abstract
Nested-word automata (NWAs) are a language formalism that helps bridge the gap between finite-state automata and pushdown automata. NWAs can express some context-free properties, such as parenthesis matching, yet retain all the desirable closure characteristics of finite-state automata.
This paper describes OpenNWA, a C++ library for working with NWAs. The library provides the expected automata-theoretic operations, such as intersection, determinization, and complementation. It is packaged with WALi—the Weighted Automaton Library—and interoperates closely with the weighted pushdown system portions of WALi.
Supported by NSF under grants CCF-{0540955, 0810053, 0904371}; by ONR under grants N00014-{09-1-0510, 10-M-0251}; by ARL under grant W911NF-09-1-0413; and by AFRL under grants FA9550-09-1-0279 and FA8650-10-C-7088. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the sponsoring agencies.
Chapter PDF
References
Alur, R.: Nested words (2011), http://www.cis.upenn.edu/~alur/nw.html
Alur, R., Madhusudan, P.: Adding Nesting Structure to Words. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 1–13. Springer, Heidelberg (2006)
Alur, R., Madhusudan, P.: Adding nesting structure to words. JACM 56(3) (May 2009)
Driscoll, E., Burton, A., Reps, T.: Checking conformance of a producer and a consumer. In: FSE (2011)
Driscoll, E., Thakur, A., Burton, A., Reps, T.: WALi: Nested-word automata. TR-1675R, Comp. Sci. Dept., Univ. of Wisconsin, Madison, WI (September 2011)
Fredrikson, M., Joiner, R., Jha, S., Reps, T., Porras, P., Saïdi, H., Yegneswaran, V.: Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 548–563. Springer, Heidelberg (2012)
Kidd, N., Lal, A., Reps, T.: WALi: The Weighted Automaton Library (2007), http://www.cs.wisc.edu/wpis/wpds/download.php
Madhusudan, P.: Visibly pushdown automata – automata on nested words (2009), http://www.cs.uiuc.edu/~madhu/vpa/
Nguyen, H.: Visibly pushdown automata library (2006), http://www.emn.fr/z-info/hnguyen/vpa/
Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. SCP 58(1-2) (October 2005)
Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., Reps, T.: Directed proof generation for machine code. TR 1669, UW-Madison (April 2010); Abridged version published in CAV 2010
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Driscoll, E., Thakur, A., Reps, T. (2012). OpenNWA: A Nested-Word Automaton Library. In: Madhusudan, P., Seshia, S.A. (eds) Computer Aided Verification. CAV 2012. Lecture Notes in Computer Science, vol 7358. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31424-7_47
Download citation
DOI: https://doi.org/10.1007/978-3-642-31424-7_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31423-0
Online ISBN: 978-3-642-31424-7
eBook Packages: Computer ScienceComputer Science (R0)