research-article

Robust strategy synthesis for probabilistic systems applied to risk-limiting renewable-energy pricing

Authors:

Alberto Puggelli,

Alberto L. Sangiovanni-Vincentelli,

Sanjit A. SeshiaAuthors Info & Claims

EMSOFT '14: Proceedings of the 14th International Conference on Embedded Software

Article No.: 13, Pages 1 - 10

https://doi.org/10.1145/2656045.2656069

Published: 12 October 2014 Publication History

Abstract

We address the problem of synthesizing control strategies for Ellipsoidal Markov Decision Processes (EMDP), i.e., MDPs whose transition probabilities are expressed using ellipsoidal uncertainty sets. The synthesized strategy aims to maximize the total expected reward of the EMDP, constrained to a specification expressed in Probabilistic Computation Tree Logic (PCTL). We prove that the EMDP strategy synthesis problem for the fragment of PCTL disabling operators with a finite time bound is NP-complete and propose a novel sound and complete algorithm to solve it.

We apply these results to the problem of synthesizing optimal energy pricing and dispatch strategies in smart grids that integrate renewable sources of energy. We use rewards to maximize the profit of the network operator and a PCTL specification to constrain the risk of power unbalance and guarantee quality-of-service for the users. The EMDP model used to represent the decision-making scenario was trained with measured data and quantitatively captures the uncertainty in the prediction of energy generation. An experimental comparison shows the effectiveness of our method with respect to previous approaches presented in the literature.

References

[1]

Courcoubetis, C. and Yannakakis, M., "The Complexity of Probabilistic Verification," Journal of ACM, vol. 42(4), pp. 857--907, 1995.

Digital Library

[2]

H. Hansson and B. Jonsson, "A Logic for Reasoning About Time and Reliability," Formal Aspects of Computing, vol. 6(5), pp. 512--535, 1994.

Digital Library

[3]

A. Bianco and L. de Alfaro, "Model Checking of Probabilistic and Nondeterministic Systems," in Proc. of FSTTCS, ser. LNCS. Springer Berlin Heidelberg, 1995, vol. 1026, pp. 499--513.

Digital Library

[4]

M. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, 1994.

Digital Library

[5]

"International Energy Agency, World Energy Outlook 2009." {Online}: http://www.worldenergyoutlook.org/docs/weo2009/WEO2009_es_english.pdf.

[6]

A. Gore, An Inconvenient Truth. New York: Rodale, 2006.

[7]

P. Varaiya, F. Wu, and J. Bialek, "Smart Operation of Smart Grid: Risk-Limiting Dispatch," Proceedings of the IEEE, vol. 99, no. 1, pp. 40--57, 2011.

[8]

K. Porter and J. Rogers, "Survey of Variable Generation Forecasting in the West," in NREL Subcontract Report SR-5500-54457, April 2012, p. 56.

[9]

S. Koch et al., "Modeling and Control of Aggregated Heterogeneous Thermostatically Controlled Loads for Ancillary Services," Proc. of PSCC, pp. 1--7, 2011.

[10]

M. He, S. Murugesan, and J. Zhang, "Multiple Timescale Dispatch and Scheduling for Stochastic Reliability in Smart Grids with Wind Generation Integration," in Proc. of IEEE INFOCOM, 2011, pp. 461--465.

[11]

A. Puggelli et al., "Polynomial-Time Verification of PCTL properties of MDPs with Convex Uncertainties," in Proc. of CAV, ser. LNCS. Springer, 2013, vol. 8044, pp. 527--542.

Digital Library

[12]

A. Puggelli, "Formal Techniques for the Verification and Optimal Control of Probabilistic Systems in the Presence of Modeling Uncertainties," Ph.D. dissertation, University of California, Berkeley, Berkeley, CA, 2014.

[13]

C. Baier et al., "Controller Synthesis for Probabilistic Systems," in Exploring New Frontiers of Theoretical Informatics. Springer US, 2004, vol. 155, pp. 493--506.

[14]

M. Lahijanian et al., "Temporal Logic Motion Planning and Control with Probabilistic Satisfaction Guarantees," IEEE Transactions on Robotics, vol. 28, no. 2, pp. 396--409, 2012.

Digital Library

[15]

M. Kwiatkowska and D. Parker, "Automated Verification and Strategy Synthesis for Probabilistic Systems," in Proc. of ATVA, ser. LNCS, vol. 8172. Springer, 2013, pp. 5--22.

[16]

K. Sen et al., "Model-Checking Markov Chains in the Presence of Uncertainties," in Proc. of TACAS, ser. LNCS. Springer Berlin Heidelberg, 2006, vol. 3920, pp. 394--410.

Digital Library

[17]

A. Nilim and L. El Ghaoui, "Robust Control of Markov Decision Processes with Uncertain Transition Matrices," Journal of Operations Research, pp. 780--798, 2005.

Digital Library

[18]

M. Y. Vardi, "Automatic Verification of Probabilistic Concurrent Finite State Programs," in Proc. of SFCS, 1985, pp. 327--338.

Digital Library

[19]

V. Forejt et al., "Automated Verification Techniques for Probabilistic Systems," Formal Methods for Eternal Networked Software Systems, vol. 6659, pp. 53--113, 2011.

[20]

F. Bouffard and F. Galiana, "Stochastic Security for Operations Planning with Significant Wind Power Generation," in IEEE Transaction on Power Systems, 2008, vol. 23, no. 2, pp. 306--316.

[21]

A. Kučera and O. Stražovský, "On the Controller Synthesis for Finite-State Markov Decision Processes," in Proc. of FSTTCS, ser. LNCS. Springer Berlin Heidelberg, 2005, vol. 3821, pp. 541--552.

Digital Library

[22]

K. Draeger et al., "Permissive Controller Synthesis for Probabilistic Systems," in Proc. of TACAS, ser. LNCS. Springer, 2014, pp. 531--546.

[23]

T. Brazdil et al., "Stochastic Games with Branching-Time Winning Objectives," in Proc. of IEEE SLCS, Aug. 2006, pp. 349--358.

Digital Library

[24]

C. Hang et al., "Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints," in Proc. of CAV. Berlin, Heidelberg: Springer-Verlag, 2011, pp. 441--456.

Digital Library

[25]

P. Nuzzo et al., "CalCS: SMT Solving for Non-linear Convex Constraints," in Proc. of FMCAD, 2010, pp. 71--80.

Digital Library

[26]

S. Boyd and L. Vandenberghe, "Convex Optimization," Cambridge University Press, 2004.

Digital Library

[27]

"Gurobi Optimizer." {Online}: http://www.gurobi.com/.

[28]

S. Stoft, Power System Economics: Designing Markets for Electricity. NewYork: Wiley, 2002.

[29]

Y. Wan, "Long-term Wind Power Variability," NREL Technical Report TP-5500-53637. {Online}: http://www.nrel.gov/docs/fy12osti/53637.pdf, January 2012.

[30]

E. Ela et al., "Operating Reserves and Variable Generation," NREL Technical Report. {Online}: http://www.nrel.gov/docs/fy11osti/51978.pdf, August 2011.

[31]

M. Kwiatkowska et al., "PRISM 4.0: Verification of Probabilistic Real-Time Systems," Proc. of CAV, pp. 585--591, 2011.

Digital Library

Cited By

Yin XGao BYu X(2024)Formal synthesis of controllers for safety-critical autonomous systems: Developments and challengesAnnual Reviews in Control10.1016/j.arcontrol.2024.10094057(100940)Online publication date: 2024
https://doi.org/10.1016/j.arcontrol.2024.100940
Elfar MWang YPajic M(2020)Context-Aware Temporal Logic for Probabilistic SystemsAutomated Technology for Verification and Analysis10.1007/978-3-030-59152-6_12(215-232)Online publication date: 12-Oct-2020
https://doi.org/10.1007/978-3-030-59152-6_12
Qin ZCai XHou Y(2017)Improving wind power utilisation under stormy weather condition by risk‐limiting unit commitmentThe Journal of Engineering10.1049/joe.2017.06352017:13(1765-1770)Online publication date: 14-Dec-2017
https://doi.org/10.1049/joe.2017.0635
Show More Cited By

Index Terms

Robust strategy synthesis for probabilistic systems applied to risk-limiting renewable-energy pricing

Recommendations

Distributionally Robust Strategy Synthesis for Switched Stochastic Systems
HSCC '23: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control

We present a novel framework for formal control of uncertain discrete-time switched stochastic systems against probabilistic reach-avoid specifications. In particular, we consider stochastic systems with additive noise, whose distribution lies in an ...
Limiting Discounted-Cost Control of Partially Observable Stochastic Systems

This paper presents two main results on partially observable (PO) stochastic systems. In the first one, we consider a general PO system $$ x_{t+1}= F (x_t, a_t, xi_t), , y_t= G(x_t, eta_t) (t=0,1,ldots) hspace{1in} (*) $$ on Borel spaces, with possibly ...
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs

We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained determinized program satisfies a given quantitative ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

EMSOFT '14: Proceedings of the 14th International Conference on Embedded Software

October 2014

301 pages

ISBN:9781450330527

DOI:10.1145/2656045

Program Chairs:
Tulika Mitra
National University of Singapore, Singapore
,
Jan Reineke
Saarland University, Germany

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems
SIGDA: ACM Special Interest Group on Design Automation
IEEE CAS
IEEE Council on Electronic Design Automation (CEDA)
SIGMICRO: ACM Special Interest Group on Microarchitectural Research and Processing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 October 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Funding Sources

Conference

ESWEEK'14

Sponsor:

ESWEEK'14: TENTH EMBEDDED SYSTEM WEEK

October 12 - 17, 2014

New Delhi, India

Acceptance Rates

Overall Acceptance Rate 60 of 203 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
120
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)2

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yin XGao BYu X(2024)Formal synthesis of controllers for safety-critical autonomous systems: Developments and challengesAnnual Reviews in Control10.1016/j.arcontrol.2024.10094057(100940)Online publication date: 2024
https://doi.org/10.1016/j.arcontrol.2024.100940
Elfar MWang YPajic M(2020)Context-Aware Temporal Logic for Probabilistic SystemsAutomated Technology for Verification and Analysis10.1007/978-3-030-59152-6_12(215-232)Online publication date: 12-Oct-2020
https://doi.org/10.1007/978-3-030-59152-6_12
Qin ZCai XHou Y(2017)Improving wind power utilisation under stormy weather condition by risk‐limiting unit commitmentThe Journal of Engineering10.1049/joe.2017.06352017:13(1765-1770)Online publication date: 14-Dec-2017
https://doi.org/10.1049/joe.2017.0635
Seshia S(2015)Combining Induction, Deduction, and Structure for Verification and SynthesisProceedings of the IEEE10.1109/JPROC.2015.2471838103:11(2036-2051)Online publication date: Nov-2015
https://doi.org/10.1109/JPROC.2015.2471838

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents