Evolutionary-Guided Synthesis of Verified Pareto-Optimal MDP Policies

Simos Gerasimou; Javier Camara Moreno; Radu Calinescu; Naif Alasmari; Faisal Alhwikem; Xinwei Fang

doi:10.1109/ASE51524.2021.9678727

Evolutionary-Guided Synthesis of Verified Pareto-Optimal MDP Policies

Simos Gerasimou, Javier Camara Moreno, Radu Calinescu, Naif Alasmari, Faisal Alhwikem, Xinwei Fang

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present a new approach for synthesising Pareto- optimal Markov decision process (MDP) policies that satisfy complex combinations of quality-of-service (QoS) software requirements. These policies correspond to optimal designs or configurations of software systems, and are obtained by translating MDP models of these systems into parametric Markov chains, and using multi-objective genetic algorithms to synthesise Pareto-optimal parameter values that define the required MDP policies. We use case studies from the service-based systems and robotic control software domains to show that our MDP policy synthesis approach can handle a wide range of QoS requirement combinations unsupported by current probabilistic model checkers. Moreover, for requirement combinations supported by these model checkers, our approach generates better Pareto-optimal policy sets according to established quality metrics.

Original language	English
Title of host publication	36th IEEE/ACM International Conference on Automated Software Engineering
Publisher	IEEE
DOIs	https://doi.org/10.1109/ASE51524.2021.9678727
Publication status	Published - 20 Jan 2022

Access to Document

10.1109/ASE51524.2021.9678727

MDPPolicySynthesis-ASE2021Accepted author manuscript, 545 KB

UKRI Trustworthy Autonomous Systems Node in Resilience
Calinescu, R., Arvind, T., Cavalcanti, A. L. C., Habli, I., Thomas, A. P. & Wilson, J. C.
EPSRC
1/11/20 → 31/10/24
Project: Research project (funded) › Research

Cite this

@inproceedings{04f051bf2b79466897321da336a23eda,

title = "Evolutionary-Guided Synthesis of Verified Pareto-Optimal MDP Policies",

abstract = "We present a new approach for synthesising Pareto- optimal Markov decision process (MDP) policies that satisfy complex combinations of quality-of-service (QoS) software requirements. These policies correspond to optimal designs or configurations of software systems, and are obtained by translating MDP models of these systems into parametric Markov chains, and using multi-objective genetic algorithms to synthesise Pareto-optimal parameter values that define the required MDP policies. We use case studies from the service-based systems and robotic control software domains to show that our MDP policy synthesis approach can handle a wide range of QoS requirement combinations unsupported by current probabilistic model checkers. Moreover, for requirement combinations supported by these model checkers, our approach generates better Pareto-optimal policy sets according to established quality metrics.",

author = "Simos Gerasimou and {Camara Moreno}, Javier and Radu Calinescu and Naif Alasmari and Faisal Alhwikem and Xinwei Fang",

year = "2022",

month = jan,

day = "20",

doi = "10.1109/ASE51524.2021.9678727",

language = "English",

booktitle = "36th IEEE/ACM International Conference on Automated Software Engineering",

publisher = "IEEE",

address = "United States",

}

TY - GEN

T1 - Evolutionary-Guided Synthesis of Verified Pareto-Optimal MDP Policies

AU - Gerasimou, Simos

AU - Camara Moreno, Javier

AU - Calinescu, Radu

AU - Alasmari, Naif

AU - Alhwikem, Faisal

AU - Fang, Xinwei

PY - 2022/1/20

Y1 - 2022/1/20

N2 - We present a new approach for synthesising Pareto- optimal Markov decision process (MDP) policies that satisfy complex combinations of quality-of-service (QoS) software requirements. These policies correspond to optimal designs or configurations of software systems, and are obtained by translating MDP models of these systems into parametric Markov chains, and using multi-objective genetic algorithms to synthesise Pareto-optimal parameter values that define the required MDP policies. We use case studies from the service-based systems and robotic control software domains to show that our MDP policy synthesis approach can handle a wide range of QoS requirement combinations unsupported by current probabilistic model checkers. Moreover, for requirement combinations supported by these model checkers, our approach generates better Pareto-optimal policy sets according to established quality metrics.

AB - We present a new approach for synthesising Pareto- optimal Markov decision process (MDP) policies that satisfy complex combinations of quality-of-service (QoS) software requirements. These policies correspond to optimal designs or configurations of software systems, and are obtained by translating MDP models of these systems into parametric Markov chains, and using multi-objective genetic algorithms to synthesise Pareto-optimal parameter values that define the required MDP policies. We use case studies from the service-based systems and robotic control software domains to show that our MDP policy synthesis approach can handle a wide range of QoS requirement combinations unsupported by current probabilistic model checkers. Moreover, for requirement combinations supported by these model checkers, our approach generates better Pareto-optimal policy sets according to established quality metrics.

U2 - 10.1109/ASE51524.2021.9678727

DO - 10.1109/ASE51524.2021.9678727

M3 - Conference contribution

BT - 36th IEEE/ACM International Conference on Automated Software Engineering

PB - IEEE

ER -

Evolutionary-Guided Synthesis of Verified Pareto-Optimal MDP Policies

Abstract

Access to Document

Projects

UKRI Trustworthy Autonomous Systems Node in Resilience

Cite this