TY - CHAP

T1 - Formalization of Cost and Utility in Microeconomics

AU - Ahmed, Asad

AU - Hasan, Osman

AU - Awwad, Falah

AU - Bastaki, Nabil

N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85113555104&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85113555104&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-78409-6_4

DO - 10.1007/978-3-030-78409-6_4

M3 - Chapter

AN - SCOPUS:85113555104

T3 - SpringerBriefs in Applied Sciences and Technology

SP - 47

EP - 60

BT - SpringerBriefs in Applied Sciences and Technology

PB - Springer Science and Business Media Deutschland GmbH

ER -