We propose Pareto optimal reachability analysis to solve multi-objective scheduling and planing problems using real-time model checking techniques. Not only the makespan of a schedule, but also other objectives involving quantities like performance, energy, risk, cost etc., can be optimized simultaneously in balance. We develop the Pareto optimal reachability algorithm for Uppaal to explore the state-space and compute the goal states on which all objectives will reach a Pareto optimum. After that diagnostic traces are generated from the initial state to the goal states, and Pareto optimal schedules are obtainable from those traces. We demonstrate the usefulness of this new feature by two case studies.
CITATION STYLE
Zhang, Z., Nielsen, B., Larsen, K. G., Nies, G., Stenger, M., & Hermanns, H. (2017). Pareto Optimal Reachability Analysis for Simple Priced Timed Automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10610 LNCS, pp. 481–495). Springer Verlag. https://doi.org/10.1007/978-3-319-68690-5_29
Mendeley helps you to discover research relevant for your work.