Model checking: From tools to theory

Model checking is often cited as a success story for transitioning and engineering ideas rooted in logics and automata to practice. In this paper, we discuss how the efforts aimed at improving the scope and effectiveness of model checking tools have revived the study of logics and automata leading to unexpected theoretical advances whose impact is not limited to model checking. In particular, we describe how our efforts to add context-free specifications to software model checking led us to the model of nested words as a representation of data with both a linear ordering and a hierarchically nested matching of items. Such dual structure occurs in diverse corners of computer science ranging from executions of structured programs where there is a well-nested matching of entries to and exits from functions and procedures, to XML documents with the hierarchical structure specified by start-tags matched with end-tags. Finite-state acceptors of nested words define the class of regular languages of nested words that has all the appealing theoretical properties that the class of regular word languages enjoys. We review the emerging theory of nested words, its extension to nested trees, and its potential applications.