Challenges for Logic, Transducers and Automata – DELTA

Software systems are ubiquitous, and more and more complex. The automated analysis of computer-generated data and the reliability analysis of complex programs become therefore crucial, and challenging due to the increasing size and intricacy of the objects that software systems have to face. Model-checking is a successful technique for system verification, that is now mature, and used for industrial purposes: it amounts to verifying the correctness of the system with respect to some specification. The core of this approach relies on finite-state machines: on the one hand, they provide an operational model of systems, and on the other hand, they can be considered as a low-level description of specifications. Finite-state machines processing various kinds of objects, such as words or trees, are very appealing because they capture one of the most robust concepts in computer science: the notion of regularity. This notion unifies a triangle (a Delta!) of different approaches with longstanding tradition: an operational one (automata), a descriptive one (logic), and an equational one (algebra). Logic is a powerful and precise formalism for specifying properties of systems, whereas automata offer an effective algorithmic tool, for instance for verifying and certifying properties; algebra comes naturally into play when we ask how far we can go with a specification formalism. The interplay summarized by the perfect ? of automata-logic-algebra is best understood for languages of words, where a rich theory has developed since the fundamental results of the sixties. Since then, the theory has grown in many directions, raising new and important challenges.

Current challenges. Modeling by classical finite-state machines suffices for very simple systems or programs whose variables range over bounded domains. But most realistic systems require to cope with values from unbounded domains. Let us motivate the new difficulties on three symbolic examples, where finite domains are not sufficient anymore. First, when modeling embedded software, values may represent the energy level of the system, and we may be interested in measuring maximal or average quantity of energy consumption: we need to reason about quantities. Second, looking for a text pattern in a mailbox can be solved very efficiently with finite-state machines, but what about searching for patterns where we must compare values, like time-stamps or process identifiers? We need to reason about values from an unbounded domain. A last example comes from the verification of stream-processing programs, that aims, e.g., at building on-the-fly some output flow of relevant elements out of a linear sequence of input events: the difficulty comes again from unbounded data, and requirements on the memory of the on-the-fly process of the input flow. Objectives. New theories must be devised to solve these new issues. The challenge is to retain all the advantages of the classical theory, in particular simplicity and efficiency of finite-state machines, while handling values from unbounded domains, in keeping with the needs of the aforementioned motivations. The DELTA project thus proposes a fundamental research program with motivations from automatic verification and static analysis for database systems.

Our primary objective is to extend these connections between automata, logic and algebra to richer settings that can handle values, with the two following goals in mind:

1. We first aim at developing appropriate models for the three facets of the ? (operational, descriptive, and equational), in the three extensions that we want to consider: quantitative values, documents carrying data, string-processing programs (also called transducers).

2. The second objective concerns the efficiency in processing the descriptive and operational models, like simplification of specifications and machines, or efficient translation of high-level specifications into low-level machines.