Quantitative Model Checking for a Smart Grid Pricing

A quantitative model checking technique is applied to compute a day-ahead pricing for smart grids. In a smart grid system, smart meters enable bidirectional communications between electricity providers and customers. The providers can monitor the customers’ detailed electricity usage and by posting dynamically changing prices, they can shape the energy demand. We propose a model checking based day-ahead pricing technique and demonstrate the usefulness of the technique. Specifically, we model the power demand changes of various types of loads by first order differential equations while considering expected loads and price changes as external forces. Complex requirements about the customers’ energy usage, the current system state estimate, and the expected load for the next day are described in an LTL based quantitative temporal logic, called LTLC. Day-ahead prices that can satisfy the description are computed through the LTLC model checking.