Formalization of Cost and Utility in Microeconomics

Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki

Research output: Chapter in Book/Report/Conference proceedingChapter


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.

Original languageEnglish
Title of host publicationSpringerBriefs in Applied Sciences and Technology
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages14
Publication statusPublished - 2022

Publication series

NameSpringerBriefs in Applied Sciences and Technology
ISSN (Print)2191-530X
ISSN (Electronic)2191-5318

ASJC Scopus subject areas

  • Biotechnology
  • General Chemical Engineering
  • General Mathematics
  • General Materials Science
  • Energy Engineering and Power Technology
  • General Engineering


Dive into the research topics of 'Formalization of Cost and Utility in Microeconomics'. Together they form a unique fingerprint.

Cite this