A formal model for sustainable vehicle-to-grid management

The Vehicle-To-Grid (V2G) technology allows plug-in electric vehicles (PEVs) to act like an energy provider besides being a consumer. A PEV, being connected to the smart grid, can either charge its battery by consuming electricity from the grid or discharge the stored electricity from the battery to the grid. It can also participate in the frequency regulation service of the grid. Executing the aforementioned operations in a non-controlled fashion may come with problems on the grid functionality. For safe and sustainable functioning of the grid, controlling the operations is very crucial. In this paper, we are offering an approach for vehicle-to-grid management using constraint-based formal modeling. The approach is centered around an aggregator that collects all the involved parties' constraints and preferences. The aggregator then finds a management plan, i.e., a schedule of V2G services for the PEVs by satisfying the given constraints besides its own requirements. We apply satisfiability modulo theories (SMT) to synthesize the schedule as a satisfaction of the constraints. Our evaluation results show that the formalization can be efficiently solved for problems with thousands of PEVs.