The expressiveness of looping terms in the semantic programming (Q2306056): Difference between revisions

In the present paper, the authors study a specific kind of FO-formulas with sorts ``urelement'' and ``list'' in which one can express list structures in programming languages. In particular, they focus on the computational complexity of such constructs (e.g., bounded search terms, recursive terms, and iterative terms of sort ``list'') with the perspective on the model checking as well as the satisfiability problem. Model checking is a very central task in the area of program verification as it answers the question of whether a program fulfills a given specification. Under this point of view, the satisfiability problem asks if a given specification is consistent, that is, allows for fitting program implementation. After presenting syntax and semantics of classical formulas in Section~2, the authors introduce the new constructs (for the looping terms) in Section~3. To my personal taste, some examples in these sections would be beneficial, yet, unfortunately, the paper is lacking them. In Section~4, the complexity of model checking for formulas with bounded search terms is classified to be complete for the class \textsf{PSpace}. In the remainder of this section, the expressivity of recursive and iterative terms is analyzed, yielding a hardness result for \textsf{kExpTime} and recursive terms with respect to model checking. Subsequently, the authors show \textsf{PSpace}-hardness and containment in \textsf{ExpTime} or \textsf{2ExpTime} for flat formulas and iterative terms depending on the encoding of iterators (unary versus binary) with respect to model checking. The satisfiability problem for flat iterative terms then is proved to be \textsf{NkExpTime}-hard via a reduction from bounded domino tiling, when the number of iterations is given in unary. Similarly, as before, the complexity increases one exponential factor when this number is given in binary. The result for flat recursive terms shows \textsf{NkExpTime}-completeness. The paper is written quite technical and does neither present any graphical visualizations of proof details nor assist the reader with some further examples.