text: Motivated by the successful application of the theory of regular languages to formal verification of finite-state systems, there is a renewed interest in developing a theory of analyzable functions from strings to numerical values that can provide a foundation for analyzing quantitative properties of finitestate systems. In this paper, we propose a deterministic model for associating costs with strings that is parameterized by operations of interest (such as addition, scaling, and min), a notion of regularity that provides a yardstick to measure expressiveness, and study decision problems and theoretical properties of resulting classes of cost functions. Our definition of regularity relies on the theory of string-to-tree transducers, and allows associating costs with events that are conditional upon regular properties of future events. Our model of cost register automata allows computation of regular functions using multiple “write-only” registers whose values can be combined using the allowed set of operations. We show that classical shortest-path algorithms as well as algorithms designed for computing discounted costs, can be adopted for solving the min-cost problems for the more general classes of functions specified in our model. Cost register automata with min and increment give a deterministic model that is equivalent to weighted automata, an extensively studied nondeterministic model, and this connection results in new insights and new open problems.
  @cite_0: Several optimizations of programs can be performed when in certain regions of a program equality relationships hold between a linear combination of the variables of the program and a constant. This paper presents a practical approach to detecting these relationships by considering the problem from the viewpoint of linear algebra. Key to the practicality of this approach is an algorithm for the calculation of the "sum" of linear subspaces.
  @cite_21: We give a simple formulation of Karr’s algorithm for computing all affine relationships in affine programs. This simplified algorithm runs in time ( O (nk^ 3 ) ) where n is the program size and k is the number of program variables assuming unit cost for arithmetic operations. This improves upon the original formulation by a factor of k. Moreover, our re-formulation avoids exponential growth of the lengths of intermediately occurring numbers (in binary representation) and uses less complicated elementary operations. We also describe a generalization that determines all polynomial relations up to degree d in time ( O (nk^ 3d ) ).
  @cite_22: 
summary: In @cite_0 , and more recently in @cite_21 @cite_22 , the authors present the problem of deriving affine relations among variables of a program. An affine relation is a property of the form @math , where @math are program variables that range over a field such as the rationals or reals and @math are constants over the same domain. An affine program is a program with nondeterministic branching where each edge of the program is labeled with an assignment statement of the form @math , , where the RHS is an affine expression. We could define a over the cost model @math , with the cost grammar @math . An affine program is then simply obtained by ignoring the input labels of the transitions in such a . While the cost functions defined by such do not have interesting regularity properties, we remark that the equivalence of such can be checked in polynomial time by using ideas similar to the ones in @cite_21 .