Adding nesting structure to words

ABSTRACT

We propose the model of nested words for representation of data with both a linear ordering and a hierarchically nested matching of items. Examples of data with such dual linear-hierarchical structure include executions of structured programs, annotated linguistic data, and HTML/XML documents. Nested words generalize both words and ordered trees, and allow both word and tree operations. We define nested word automata—finite-state acceptors for nested words, and show that the resulting class of regular languages of nested words has all the appealing theoretical properties that the classical regular word languages enjoys: deterministic nested word automata are as expressive as their nondeterministic counterparts; the class is closed under union, intersection, complementation, concatenation, Kleene-*, prefixes, and language homomorphisms; membership, emptiness, language inclusion, and language equivalence are all decidable; and definability in monadic second order logic corresponds exactly to finite-state recognizability. We also consider regular languages of infinite nested words and show that the closure properties, MSO-characterization, and decidability of decision problems carry over.

The linear encodings of nested words give the class of visibly pushdown languages of words, and this class lies between balanced languages and deterministic context-free languages. We argue that for algorithmic verification of structured programs, instead of viewing the program as a context-free language over words, one should view it as a regular language of nested words (or equivalently, a visibly pushdown language), and this would allow model checking of many properties (such as stack inspection, pre-post conditions) that are not expressible in existing specification logics.

We also study the relationship between ordered trees and nested words, and the corresponding automata: while the analysis complexity of nested word automata is the same as that of classical tree automata, they combine both bottom-up and top-down traversals, and enjoy expressiveness and succinctness benefits over tree automata.

REFERENCES

• 1: Rajeev Alur, Marrying words and trees, Proceedings of the twenty-sixth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 11-13, 2007, Beijing, China [doi>10.1145/1265530.1265564]
• 2: Rajeev Alur , Michael Benedikt , Kousha Etessami , Patrice Godefroid , Thomas Reps , Mihalis Yannakakis, Analysis of recursive state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.4, p.786-818, July 2005 [doi>10.1145/1075382.1075387]
• 3: Alur, R., Etessami, K., and Madhusudan, P. 2004. A temporal logic of nested calls and returns. In TACAS'04: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Software. Lecture Notes in Computer Science, vol. 2988, Springer-Verlag, Berlin, Germany, 467--481.
• 4: Alur, R., Kumar, V., Madhusudan, P., and Viswanathan, M. 2005b. Congruences for visibly pushdown languages. In Automata, Languages and Programming: Proceedings of the 32nd ICALP. Lecture Notes in Computer Science, vol. 3580, Springer-Verlag, Berlin, Germany, 1102--1114.
• 5: Rajeev Alur , P. Madhusudan, Visibly pushdown languages, Proceedings of the thirty-sixth annual ACM symposium on Theory of computing, June 13-16, 2004, Chicago, IL, USA [doi>10.1145/1007352.1007390]
• 6: Alur, R. and Madhusudan, P. 2006. Adding nesting structure to words. In Developments in Language Theory. Lecture Notes in Computer Science, vol. 4036, Springer-Verlag, Berlin, Germany, 1--13.
• 7: Jean-Michel Autebert , Jean Berstel , Luc Boasson, Context-free languages and pushdown automata, Handbook of formal languages, vol. 1: word, language, grammar, Springer-Verlag New York, Inc., New York, NY, 1997
• 8: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 9: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 10: Jean Berstel , Luc Boasson, Balanced grammars and their languages, Formal and natural computing, Springer-Verlag New York, Inc., New York, NY, 2002
• 11: Steven Bird , Yi Chen , Susan B. Davidson , Haejoong Lee , Yifeng Zheng, Designing and Evaluating an XPath Dialect for Linguistic Queries, Proceedings of the 22nd International Conference on Data Engineering, p.52, April 03-07, 2006 [doi>10.1109/ICDE.2006.48]
• 12: Ahmed Bouajjani , Javier Esparza , Oded Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking, Proceedings of the 8th International Conference on Concurrency Theory, p.135-150, July 01-04, 1997
• 13: Bouquet, A., Serre, O., and Walukiewicz, I. 2003. Pushdown games with unboundedness and regular conditions. In FSTTCS 2003: Proceedings of the 23rd International Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 2914, Springer-Verlag, Berlin, Germany, 88--99.
• 14: Brüggemann-Klein, A., Murata, M., and Wood, D. 2001. Regular tree and regular hedge languages over unranked alphabets: Version 1. Tech. Rep. HKUST-TCSC-2001-0, The Hongkong University of Science and Technology.
• 15: Brüggermann-Klein, A., and Wood, D. 2004. Balanced context-free grammars, hedge grammars and pushdown caterpillar automata. In Proceedings of the Extreme Markup Languages.
• 16: Olaf Burkart , Bernhard Steffen, Model Checking for Context-Free Processes, Proceedings of the Third International Conference on Concurrency Theory, p.123-137, August 24-27, 1992
• 17: Thierry Cachat , Jacques Duparc , Wolfgang Thomas, Solving Pushdown Games with a Sigma3 Winning Condition, Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, p.322-336, September 22-25, 2002
• 18: Krishnendu Chatterjee , Di Ma , Rupak Majumdar , Tian Zhao , Thomas A. Henzinger , Jens Palsberg, Stack size analysis for interrupt-driven programs, Information and Computation, v.194 n.2, p.144-174, November 1, 2004 [doi>10.1016/j.ic.2004.06.001]
• 19: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 20: Comon, H., Dauchet, M., Gilleron, R., Lugiez, D., Tison, S., and Tommasi, M. 2002. Tree automata techniques and applications. Draft, Available at http://www.grappa.univ-lille3.fr/tata/.
• 21: Patrick Dymond, Input-driven languages are in log n depth, Information Processing Letters, v.26 n.5, p.247-250, Jan. 11, 1988 [doi>10.1016/0020-0190(88)90148-2]
• 22: Javier Esparza , Antonín Kucera , Stefan Schwoon, Model checking LTL with regular valuations for pushdown systems, Information and Computation, v.186 n.2, p.355-376, 01 November 2003 [doi>10.1016/S0890-5401(03)00139-1]
• 23: Ginsburg, S., and Harrison, M. 1967. Bracketed context-free languages. J. Comput. Syst. Sci. 1, 1--23.
• 24: Todd J. Green , Gerome Miklau , Makoto Onizuka , Dan Suciu, Processing XML Streams with Deterministic Automata, Proceedings of the 9th International Conference on Database Theory, p.173-189, January 08-10, 2003
• 25: Ashish Kumar Gupta , Dan Suciu, Stream processing of XPath queries with predicates, Proceedings of the 2003 ACM SIGMOD international conference on Management of data, June 09-12, 2003, San Diego, California [doi>10.1145/872757.872809]
• 26: David Harel , Jerzy Tiuryn , Dexter Kozen, Dynamic Logic, MIT Press, Cambridge, MA, 2000
• 27: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Grégoire Sutre , Westley Weimer, Temporal-Safety Proofs for Systems Code, Proceedings of the 14th International Conference on Computer Aided Verification, p.526-538, July 27-31, 2002
• 28: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 29: John E. Hopcroft , Rajeev Motwani , Jeffrey D. Ullman, Introduction to Automata Theory, Languages, and Computation (3rd Edition), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2006
• 30: Jensen, T., Metayer, D. L., and Thorn, T. 1999. Verification of control flow based security properties. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, 89--103.
• 31: Knuth, D. 1967. A characterization of parenthesis languages. Inf. Cont. 11, 3, 269--289.
• 32: Clemens Lautemann , Thomas Schwentick , Denis Thérien, Logics For Context-Free Languages, Selected Papers from the 8th International Workshop on Computer Science Logic, p.205-216, September 25-30, 1994
• 33: Libkin, L. 2005. Logics for unranked trees: An overview. In Proceedings of the 32nd International Colloquium in Automata, Languages and Programming. LNCS 3580, 35--50.
• 34: Löding, C., Madhusudan, P., and Serre, O. 2004. Visibly pushdown games. In FSTTCS 2004: Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 3328, Springer-Verlag, Berlin, Germany, 408--420.
• 35: Martens, W., and Niehren, J. 2005. Minimizing tree automata for unranked trees. In Proceedings of the 10th International Symposium on Database Programming Languages. 233--247.
• 36: Robert McNaughton, Parenthesis Grammars, Journal of the ACM (JACM), v.14 n.3, p.490-500, July 1967 [doi>10.1145/321406.321411]
• 37: Frank Neven, Automata, Logic, and XML, Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, p.2-26, September 22-25, 2002
• 38: Amir Pnueli, The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, p.46-57, September 30-October 31, 1977
• 39: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 40: Thomas Schwentick, Automata for XML---A survey, Journal of Computer and System Sciences, v.73 n.3, p.289-315, May, 2007 [doi>10.1016/j.jcss.2006.10.003]
• 41: Luc Segoufin , Victor Vianu, Validating streaming XML documents, Proceedings of the twenty-first ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 03-05, 2002, Madison, Wisconsin [doi>10.1145/543613.543622]
• 42: Sharir, M., and Pnueli, A. 1981. Two approaches to inter-procedural data-flow analysis. In Program flow analysis: Theory and applications. Prentice-Hall, Englewood Cliffs, NJ.
• 43: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 44: Moshe Y. Vardi , Pierre Wolper, Reasoning about infinite computations, Information and Computation, v.115 n.1, p.1-37, Nov. 15, 1994 [doi>10.1006/inco.1994.1092]
• 45: Burchard von Braunmühl , Rutger Verbeek, Input-Driven Languages are Recognized in log n Space, Proceedings of the 1983 International FCT-Conference on Fundamentals of Computation Theory, p.40-51, August 21-27, 1983

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

General Terms:
Theory, Verification

Keywords:
Pushdown automata, XML processing, software model checking, tree automata