Formalization of Cost and Utility in Microeconomics

In smart grids, cost and utility modeling is used to assess the cost of energy generation from energy sources such as thermal plants and design incentives in DR programs, respectively. Cost and utility modeling, mainly, uses convex and differential theories to model the behaviors of grid actors, such as consumers. Traditionally, paper-and-pencil proof methods and computer-based tools were used to investigate the mathematical properties of cost and utility models. However, these techniques do not provide an accurate analysis due to their inability to exhaustively specify and verify the mathematical properties of the cost and utility models. Whereas accurate analysis is direly needed in mission-critical applications of smart grids such as energy generation and DR programs. To overcome the issues pertaining to the above-mentioned techniques, in this chapter, we present a theorem proving based logical framework to formally analyze and specify the mathematical properties of cost and utility modeling. The logical framework is used to formally verify the estimates of coefficients of cost function for a thermal power plant.