Pith. sign in

REVIEW 3 major objections 4 minor 99 references

Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)

T0 review · 3 major / 4 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper introduces the first statistical model checking approach for multi-objective Pareto queries, using random sampling of strategies to approximate the tradeoff frontier in Markov decision processes.

desk verdict First real SMC for equal-priority multi-objective Pareto queries; underapproximation part is sound, but the asymptotic confidence-band lemma has a genuine hole and a wrong bound — worth reviewing but needs major revision to that lemma. read the letter →

arxiv 2511.13460 v2 pith:WSOW5NH6 submitted 2025-11-17 cs.LO

Pedro R. D'Argenio , Arnd Hartmanns , Patrick Wienhöft , Mark van Wijk This is my paper · ORCID
classification cs.LO MSC 68Q6068Q87
keywords multi-objectivemodelcheckingstatisticalParetofrontMarkovdecisionprocesseslightweightstrategysamplingconfidencebandprobabilisticverificationsimulation-based
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper establishes that multi-objective Pareto queries—finding optimal tradeoffs among several probability or reward objectives in a Markov decision process—can be answered statistically without exploring the model's state space. The authors propose a scheme that samples control strategies at random via lightweight strategy sampling, evaluates each with simulation runs, and forms an under-approximation of the Pareto front from the pessimistic corners of per-strategy confidence boxes. In the long run, the scheme also yields an over-approximation, so the two enclose the true front in a statistically guaranteed band. They also offer three fixed-budget heuristics for finding a close under-approximation in finite time. A sympathetic reader would care because this brings simulation-based verification to the multi-objective setting, where exhaustive methods fail on large state spaces.

What carries the argument

The central mechanism is lightweight strategy sampling (LSS), which represents each memoryless deterministic strategy by a 32-bit integer identifier and chooses actions via a hash function of identifier and state, enabling constant-memory strategy representation. Strategy identifiers are sampled uniformly, and for each sampled strategy, simulation runs produce a d-dimensional confidence box around the sample mean. The convex hull of the boxes' pessimistic corners forms the under-approximation; the hull of optimistic corners forms the over-approximation. Simultaneous correctness of all boxes is ensured by distributing the error budget α across strategies and dimensions via the union bound (Bo

What would settle it

Construct a small MDP whose Pareto-optimal strategies form a set that the LSS hash function never generates from any 32-bit identifier, and run the incremental scheme: if the over-approximation does not converge to the true front within the claimed precision √(2d ε²), the ideal-LSS assumption fails. Alternatively, count the effective number of distinct strategies the hash function can produce; if it is less than the true strategy space, convergence cannot be guaranteed.

Watch

Extended reading notes

Core claim

For an MDP with d objectives, randomly sampling memoryless deterministic strategies and evaluating them by statistical model checking yields a statistically sound under-approximation C of the true Pareto front with confidence γ. When sampling continues indefinitely under ideal lightweight strategy sampling, the under- and over-approximations almost surely converge to a simultaneous confidence band with precision √(2d ε²), enveloping the true front. In finite time, fixed-budget heuristics that discard unpromising strategies and reallocate runs to promising ones produce close under-approximations, outperforming exhaustive methods on models whose state space grows too large for conventional pro

Load-bearing premise

The asymptotic over-approximation guarantee depends on the assumption that uniformly sampling 32-bit strategy identifiers eventually produces every memoryless deterministic strategy with probability one; in practice the finite identifier space and the hash function may never sample some Pareto-optimal strategies, so the over-approximation may never close.

Editorial extensions

If this is right

  • Multi-objective verification becomes feasible for models with state spaces too large for exhaustive probabilistic model checking, since the method is constant-memory in the state space size.
  • The incremental scheme provides, for the first time, a statistical confidence band around the true Pareto front, giving both lower and upper bounds in the limit.
  • Fixed-budget variants give statistically guaranteed lower bounds, which is useful for one-shot analyses where only a limited simulation budget is available.
  • The approach extends beyond MDPs to any model class supported by LSS, such as Markov automata and probabilistic timed automata, potentially broadening its applicability.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the confidence band claim holds in practice, engineers could certify both performance and risk simultaneously: the upper bound guards against overestimating achievable tradeoffs, while the lower bound gives a safe set of strategies.
  • The strategy-selection heuristics suggest a natural connection to multi-objective reinforcement learning; a testable extension is whether combining the incremental scheme with RL-style value approximation could reduce the number of simulation runs needed to reach a given precision.
  • The reliance on 32-bit identifiers implies that for very large strategy spaces, the theoretical convergence may be obstructed by practical hashing collisions; moving to larger identifiers or structured sampling could restore the guarantee.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents the first statistical model checking (SMC) method for multi-objective Pareto queries on Markov decision processes. It uses lightweight strategy sampling (LSS) to generate random memoryless deterministic strategies, evaluates them by SMC for all objectives simultaneously, and constructs under- and over-approximations of the true Pareto front from confidence boxes. An incremental scheme (Alg. 1) is claimed to almost surely converge to a statistically sound confidence band under ideal LSS, and three fixed-budget algorithms (WVR, FIB, FSB) with several strategy-selection heuristics are proposed to obtain close underapproximations in finite time. The methods are implemented in the Modest Toolset's modes simulator and evaluated on 34 benchmark models, including some too large for the Storm model checker.

Significance. If the main theorems are correct, the paper delivers a genuinely novel capability: SMC-based multi-objective verification with statistical guarantees and constant memory, extending earlier LSS-based single-objective tools. The underapproximation result (Lemma 1) is defensible, and the fixed-budget algorithms with a separate bias-free evaluation phase are a sound and useful engineering contribution. The experimental comparison with Storm demonstrates scalability on models beyond PMC's reach, and the implementation and benchmark set are valuable. However, the central asymptotic claim — the long-run confidence band of the incremental scheme — has flaws in Lemma 2 that need correction before the paper's advertised contribution is reliable.

major comments (3)
  1. [Section 3.1, Lemma 2(2)] The overapproximation claim is not justified by the proof sketch. It argues that once all Pareto-optimal strategies are sampled and their boxes contain the true means, C̄ is an overapproximation. But C̄ is the convex hull of the optimistic corners o_i, and a true mean μ_i inside box B_i is generally not equal to o_i. The convex hull of a finite set of optimistic corners need not contain μ_i; for a single Pareto-optimal strategy, C̄={o_1} does not contain μ_1. The argument can only support that a δ-neighbourhood of C̄ is an overapproximation, with δ equal to the maximal distance between a true mean and its optimistic corner (at most 2√d ε). The lemma and the abstract's 'confidence band' statement must be revised accordingly.
  2. [Section 3.1, Lemma 2(2)] The stated precision √(2dε²) is arithmetically incorrect. Each CI has half-width ε per dimension, so the pessimistic and optimistic corners of one box differ by 2ε in each coordinate; the Euclidean distance is √(d·(2ε)²) = 2√d ε, not √(2dε²). For d=2, the paper's formula gives 2ε, whereas the correct value is 2√2 ε. This quantitative bound appears in the central convergence claim, so it must be corrected and propagated consistently through the abstract and any derived statements.
  3. [Section 3.1, Lemma 2] The phrase 'almost surely converge to an under- and overapproximation with probability γ' conflates two different probability spaces. The almost-sure part is over LSS strategy sampling under ideal LSS, while γ is the simultaneous confidence over simulation randomness. The proof sketch does not separate the two, nor does it define the mode of set convergence (e.g., Hausdorff distance). A rigorous statement is needed, especially because the 'when not interrupted' clause is an infinite-time statement while the CI correctness is per-batch and only gives probability γ. This is not merely cosmetic; it affects what the convergence claim actually guarantees.
minor comments (4)
  1. [Section 2 and Abstract] The abstract's 'almost surely converges' should be qualified with 'under ideal LSS.' Section 2 explicitly acknowledges the 32-bit identifier cap as a practical limitation, but the abstract and conclusion omit this condition, which is essential for the long-run guarantee.
  2. [Algorithms 2–5] The SMC interface is used inconsistently: Alg. 1 line 6 passes a precision ε as third argument, while Alg. 2 line 3 and Alg. 4 line 4 pass a run count n or ⌊n/|Σ|⌋. Please define the SMC parameter convention explicitly and align the pseudo-code.
  3. [Algorithm 3] Line 5 says 'select w ... between C(stat), C(stat)', which appears to be a typo for C(stat) and C̄(stat). Also, the expression 'λ σ.w·x̂^σ' in line 6 is unclear; define the dot product and the role of λ.
  4. [Experimental evaluation, Tables 2–4] The tables report counts of models where one setting 'strictly outperformed all others,' but no statistical significance measure is given, and only three seeds are used. A brief note on the variability (e.g., standard deviation or a paired test) would strengthen the comparative claims.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the Pareto-front approximations are constructed from sampled strategies' confidence boxes; no quantity is fitted to the target front, and prior-tool citations are supporting, not load-bearing.

full rationale

The derivation chain is self-contained: LSS samples strategy identifiers; SMC(σ,·) returns sample means and confidence boxes with a simultaneous-correctness requirement; C is the convex hull of pessimistic corners and C̄ the hull of optimistic corners. Lemma 1 follows directly from the CI correctness requirement plus the fact that true means are achievable points, not from assuming the conclusion. No parameter is fitted to the Pareto front, and the fixed-budget heuristics are explicitly separated from the evaluation phase to avoid bias. The incremental scheme's limit guarantee is asymptotic over sampled strategies and does not rename a fitted quantity as a prediction. The paper's reliance on lightweight strategy sampling [62] and sound confidence-interval construction [20] is citation of independently established machinery; even though some cited authors overlap with the present paper, those results are not used to assume the multi-objective conclusion and are not machine-checked in this paper, but they are parameter-free tools with stated assumptions that do not include the target result. The ideal-LSS assumption is explicitly disclosed in Section 2 as a practical limitation, and the skeptical concerns about Lemma 2's containment argument and the √(2dε²) distance bound are correctness objections, not circularity: a false or miscalculated lemma is not the same as a lemma that is true by construction. Thus no circular step is exhibited.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central guarantee rests on standard SMC soundness from prior published results and on an idealization of LSS that is acknowledged as a practical limitation. No fitted parameters are introduced; the algorithm knobs (m, n, f, α, ε) are user-chosen and the guarantees hold for any values. No new physical or formal entities are postulated.

assumptions (5)
  • domain assumption Sound SMC confidence intervals exist for the sampled quantities (from [20]).
    The whole approach inherits the soundness of the underlying SMC intervals; invoked in Section 2 (SMC background) and used in every SMC() call.
  • domain assumption Ideal LSS: uniformly sampling strategy identifiers eventually encounters every memoryless deterministic strategy with probability 1.
    Stated in Section 2 and used in Lemma 2's proof sketch to argue the overapproximation converges; it is an idealization because 32-bit identifiers cap the search space.
  • standard math The achievable set for probabilistic memoryless strategies is convex, so convex hulls of achievable points are achievable.
    Standard linearity of expectations over strategy mixtures; stated in Section 2 (multi-objective properties) and used for the underapproximation construction.
  • domain assumption MDP-reward combinations are well-formed: reachability rewards are finite with probability 1.
    Excluded in Section 2 to avoid ill-formed problems with infinite rewards; load-bearing for the expectation-based objectives.
  • standard math Simulation runs for distinct strategies are statistically independent, and dimensions share runs, so Šidák/Bonferroni corrections apply.
    Assumed in Section 3 (Multiple comparisons) to achieve simultaneous confidence γ; reasonable given separate PRNG streams for strategies.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)." pith.science (2026). https://pith.science/paper/WSOW5NH6

@misc{pith2026251113460,
  author       = {Pith},
  title        = {Pith review of: Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WSOW5NH6}},
  note         = {Machine review of arXiv:2511.13460}
}
read the original abstract

Statistical model checking delivers quantitative verification results with statistical guarantees. It scales to model sizes and model types that are out of reach for exhaustive, analytical techniques. So far, it has been used to evaluate one property value at a time only. Many practical problems, however, require finding the Pareto front of optimal tradeoffs between multiple objectives. In this paper, we present the first statistical model checking approach for such multi-objective Pareto queries, based on lightweight strategy sampling. We introduce an incremental scheme that almost surely converges to a statistically sound confidence band around the true Pareto front in the long run. To obtain a close underapproximation of the true front in finite time, we propose three heuristic approaches that try to make the best of an a-priori fixed sampling budget. We implement our new techniques in the modes simulator of the Modest Toolset, and show their effectiveness on benchmarks from the literature.

Figures

Figures reproduced from arXiv: 2511.13460 by the authors.

Figure 1
Figure 1. An example MDP and the corresponding expected-reward Pareto fronts acceptance rate is 20 % here; if rejected, we can try again the next year or go to arXiv. Reward structure Rrec represents the recognition our results get, and Reff our effort. We annotate branch s ′ of δ(s, a) with (Rrec(s, a, s′ ) / Reff (s, a, s′ )), omitting (0/0)s and writing rewards that are the same for all branches on the transition instead. … view at source ↗
Figure 2
Figure 2. CI boxes and fronts vertical axis) to form C, which is an underapproximation of the true Pareto front here. The most optimistic corners are the bottom-right ones, but they do not characterise a valid overapproximation—because we appear to have sampled no strategies close to the optimal ones on the bottom left. Lemma 1. C is an underapproximation with probability γ. Proof (sketch). If a most pessimistic corner is una… view at source ↗
Figure 3
Figure 3. Sampled strategies per sampled runs in Alg. 1 for d = 2, ε = 0.01, α = 0.1 performed is a proxy for the runtime needed; completing the evaluation of more strategies (higher values on the vertical axis) with fewer runs is “better”. As expected, the combination of high f = 0.5 and low m = 100 starts fast but is overtaken by more conservative approaches in the long run. For large batch sizes, however, the influence of … view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: Statistical comparison of sampled strategies. criteria for rejection, not the full sample distributions, using the precisions of the CIs to establish “safe” distances [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]
Figure 5
Figure 5. Figure 5: Criteria for discarding unpromising strategies. from witness” excludes in situations like in Figs. 5c, 5e and 5f. None of them can exclude σ in Figs. 5a and 5b. The intersection of both rules is “far from each other”, visualised in Fig. 5e. This rule also excludes σ in…
Figure 6
Figure 6. Figure 6: Number of strategies in each iteration using the simple heuristic 0.16 0.18 0.2 0.22 0.24 0 0.2 0.4 ← minimise fuel consumed ← minimise puddle punishment Seed 1 Seed 2 Seed 3 [PITH_FULL_IMAGE:figures/full_fig_p016_6.png]
Figure 8
Figure 8. Figure 8: Incremental scheme. within a row). On these benchmarks, configuration 3 performs best in almost every case, with the exception of the conservatively-far heuristic. This heuristic requires the intervals to be smaller to discard suboptimal strategies and thus requires mo…
Figure 9
Figure 9. Figure 9: Exponential model B Additional Experimental Results We provide a few more plots to illustrate our findings. As the QComp 2023 models are small enough to be checked with PMC, running Storm on them gives us a “ground truth” of Pareto fronts to compare the results of our …
Figure 10
Figure 10. Figure 10: Configurations 0.6 0.7 0.8 0.9 0.8 0.85 0.9 0.95 maximise x → maximise y → FIB FSB WVR Pareto front [PITH_FULL_IMAGE:figures/full_fig_p028_10.png]
Figure 13
Figure 13. Figure 13: Algorithms [PITH_FULL_IMAGE:figures/full_fig_p028_13.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

99 extracted references · 25 canonical work pages

  1. [1]

    In: Salkind, N.J

    Abdi, H.: The Bonferonni and Šidák corrections for multiple comparisons. In: Salkind, N.J. (ed.) Encyclopedia of measurement and statistics. Sage Publi- cations (2007),https://personal.utdallas.edu/~herve/Abdi-Bonferroni2007- pretty.pdf

    2007

  2. [2]

    Agha,G.,Palmskog,K.:Asurveyofstatisticalmodelchecking.ACMTrans.Model. Comput. Simul.28(1), 6:1–6:39 (2018).https://doi.org/10.1145/3158668

    doi:10.1145/3158668 2018

  3. [3]

    Akraoui,B.E.,Daoui,C.,Larach,A.,Rahhali,K.:Decompositionmethodsforsolv- ing finite-horizon large MDPs. J. Math.2022(2022).https://doi.org/10.1155/ 2022/8404716

    2022

  4. [4]

    In: Beyer, D., Hartmanns, A., Kordon, F

    Andriushchenko, R., Bork, A., Budde, C.E., Češka, M., Grover, K., Hahn, E.M., Hartmanns, A., Israelsen, B., Jansen, N., Jeppson, J., Junges, S., Köhl, M.A., Könighofer, B., Křetínský, J., Meggendorfer, T., Parker, D., Pranger, S., Quat- mann, T., Ruijters, E., Taylor, L., Volk, M., Weininger, M., Zhang, Z.: Tools at the frontiers of quantitative verificat...

    2023

  5. [5]

    (eds.) 9th International Symposium on Leveraging Applications of Formal Methods (ISoLA 2020)

    Ashok, P., Daca, P., Kretínský, J., Weininger, M.: Statistical model checking: Black or white? In: Margaria, T., Steffen, B. (eds.) 9th International Symposium on Leveraging Applications of Formal Methods (ISoLA 2020). Lecture Notes in Com- puter Science, vol. 12476, pp. 331–349. Springer (2020).https://doi.org/10.1007/ 978-3-030-61362-4_19

    2020

  6. [6]

    In: Gretton, A., Robert, C.C

    Auer, P., Chiang, C.K., Ortner, R., Drugan, M.M.: Pareto front identification from stochastic bandit feedback. In: Gretton, A., Robert, C.C. (eds.) 19th Interna- tional Conference on Artificial Intelligence and Statistics (AISTATS 2016). JMLR Workshop and Conference Proceedings, vol. 51, pp. 939–947. JMLR.org (2016), http://proceedings.mlr.press/v51/auer16.html

    2016

  7. [7]

    Awadallah, M.A., Makhadmeh, S.N., Al-Betar, M.A., Dalbah, L.M., Al-Redhaei, A., Kouka, S., Enshassi, O.S.: Multi-objective ant colony optimization: Review. Arch. Comput. Methods Eng.32, 995–1037 (2025).https://doi.org/10.1007/ s11831-024-10178-4

    2025

  8. [8]

    In: Esparza, J., Grumberg, O., Sickert, S

    Baier, C.: Probabilistic model checking. In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series – D: Information and Communication Security, vol. 45, pp. 1–23. IOS Press (2016).https://doi.org/10.3233/978-1-61499-627-9-1

    work page doi:10.3233/978-1-61499-627-9-1 2016

Show all 99 references
  1. [9]

    In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R

    Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 963–999. Springer (2018).https://doi.org/10.1007/978- 3-319-10575-8_28

    2018 doi

  2. [10]

    In: Heintz, F., Milano, M., O’Sullivan, B

    Baier, C., Christakis, M., Gros, T.P., Groß, D., Gumhold, S., Hermanns, H., Hoff- mann, J., Klauck, M.: Lab conditions for research on explainable automated deci- sions. In: Heintz, F., Milano, M., O’Sullivan, B. (eds.) 1st International Workshop on Trustworthy AI – Integratin...

    2020 doi

  3. [11]

    Barto, A.G., Bradtke, S.J., Singh, S.P.: Learning to act using real-time dynamic programming. Artif. Intell.72(1-2), 81–138 (1995).https://doi.org/10.1016/ 0004-3702(94)00011-O

    1995

  4. [12]

    (eds.) 19th International Conference on Computer Aided Verification (CAV 2007)

    Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: Time for playing games! In: Damm, W., Hermanns, H. (eds.) 19th International Conference on Computer Aided Verification (CAV 2007). Lec- ture Notes in Computer Science, vol. 4590, pp. 121–12...

    2007 doi

  5. [13]

    Journal of Mathematics and Mechanics 6(5), 679–684 (1957)

    Bellman, R.: A Markovian decision process. Journal of Mathematics and Mechanics 6(5), 679–684 (1957)

    1957

  6. [14]

    In: 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1995)

    Bianco,A.,deAlfaro,L.:Modelcheckingofprobabalisticandnondeterministicsys- tems. In: 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1995). Lecture Notes in Computer Science, vol. 1026, pp. 499–513. Springer (1995).https://doi.org/...

    1995 doi

  7. [15]

    Formal Aspects Com- put.31(2), 261–285 (2019).https://doi.org/10.1007/S00165-018-0458-2

    Bisgaard, M., Gerhardt, D., Hermanns, H., Krcál, J., Nies, G., Stenger, M.: Battery-aware scheduling in low orbit: the GomX-3 case. Formal Aspects Com- put.31(2), 261–285 (2019).https://doi.org/10.1007/S00165-018-0458-2

    2019 doi

  8. [16]

    In: Tesauro, G., Touretzky, D.S., Leen, T.K

    Boyan, J.A., Moore, A.W.: Generalization in reinforcement learning: Safely ap- proximating the value function. In: Tesauro, G., Touretzky, D.S., Leen, T.K. (eds.) Advances in Neural Information Processing Systems 7 (NIPS 1994). pp. 369–376. MIT Press (1994),https://proceedings...

    1994

  9. [17]

    In: Steffen, B

    Budde, C.E., D’Argenio, P.R., Hartmanns, A.: Digging for decision trees: A case study in strategy sampling and learning. In: Steffen, B. (ed.) 2nd International Conference on Bridging the Gap Between AI and Reality (AISoLA 2024). Lecture Notes in Computer Science, vol. 15217, ...

    2024 doi

  10. [18]

    Budde, C.E., D’Argenio, P.R., Hartmanns, A., Sedwards, S.: An efficient statistical model checker for nondeterminism and rare events. Int. J. Softw. Tools Technol. Transf.22(6), 759–780 (2020).https://doi.org/10.1007/S10009-020-00563-2

    2020 doi

  11. [19]

    In: Legay, A., Margaria, T

    Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: Quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) 23rd International Conference on Tools and Algorithms for the Construction and AnalysisofSystems(TACAS2017).LectureNo...

    2017 doi

  12. [20]

    In: Gurfinkel, A., Heule, M

    Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienhöft, P.: Sound statistical model checking for probabilities and expected rewards. In: Gurfinkel, A., Heule, M. (eds.) 31st International Conference on Tools and Al- gorithms for the Construction and Analysis of ...

    2025 doi

  13. [21]

    In: 2nd International Joint Conference on Quantitative Evaluation of Sys- tems and Formal Modeling and Analysis of Timed Systems (QEST+FORMATS 2025)

    Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, M., Wienhöft, P.: Sta- tistical model checking beyond means: Quantiles, CVaR, and the DKW inequal- ity. In: 2nd International Joint Conference on Quantitative Evaluation of Sys- tems and Formal Modeling and Analysis of T...

    2025 doi

  14. [22]

    Chen, D., Wang, Y., Gao, W.: Combining a gradient-based method and an evo- lution strategy for multi-objective reinforcement learning. Appl. Intell.50(10), 3301–3317 (2020).https://doi.org/10.1007/S10489-020-01702-7

    2020 doi

  15. [23]

    In: Silva, A., Leino, K.R.M

    Christakis, M., Eniser, H.F., Hermanns, H., Hoffmann, J., Kothari, Y., Li, J., Navas, J.A., Wüstholz, V.: Automated safety verification of programs invoking neural networks. In: Silva, A., Leino, K.R.M. (eds.) 33rd International Conference on Computer Aided Verification (CAV 2...

    2021 doi

  16. [24]

    Biometrika26(4), 404–413 (1934).https://doi.org/ 10.1093/biomet/26.4.404

    Clopper, C., Pearson, E.S.: The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika26(4), 404–413 (1934).https://doi.org/ 10.1093/biomet/26.4.404

    1934 doi

  17. [25]

    In: Lee, R., Jha, S., Mavridou, A

    D’Argenio, P.R., Fraire, J.A., Hartmanns, A.: Sampling distributed schedulers for resilient space communication. In: Lee, R., Jha, S., Mavridou, A. (eds.) 12th In- ternational NASA Formal Methods Symposium (NFM 2020). Lecture Notes in Computer Science, vol. 12229, pp. 291–310....

    2020 doi

  18. [26]

    In: Baier, C., Lago, U.D

    D’Argenio, P.R., Gerhold, M., Hartmanns, A., Sedwards, S.: A hierarchy of sched- uler classes for stochastic automata. In: Baier, C., Lago, U.D. (eds.) 21st Interna- tional Conference on Foundations of Software Science and Computation Structures (FOSSACS 2018). Lecture Notes i...

    2018 doi

  19. [27]

    In: Ábrahám, E., Huisman, M.(eds.)12thInternationalConferenceonIntegratedFormalMethods(iFM2016)

    D’Argenio,P.R.,Hartmanns,A.,Legay,A.,Sedwards,S.:Statisticalapproximation of optimal schedulers for probabilistic timed automata. In: Ábrahám, E., Huisman, M.(eds.)12thInternationalConferenceonIntegratedFormalMethods(iFM2016). 20 Lecture Notes in Computer Science, vol. 9681, p...

    2016 doi

  20. [28]

    D’Argenio, P.R., Legay, A., Sedwards, S., Traonouez, L.M.: Smart sampling for lightweight verification of Markov decision processes. Int. J. Softw. Tools Technol. Transf.17(4), 469–484 (2015).https://doi.org/10.1007/S10009-015-0383-0

    2015 doi

  21. [29]

    (eds.) 12th International Symposium on Automated Technology for Verification and Analysis (ATVA 2014)

    David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., Sørensen, M.G., Taankvist, J.H.: On time with minimal expected cost! In: Cassez, F., Raskin, J.F. (eds.) 12th International Symposium on Automated Technology for Verification and Analysis (ATVA 2014). Lecture Notes in...

    2014 doi

  22. [30]

    In: Baier, C., Tinelli, C

    David, A., Jensen, P.G., Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). LectureNotesinComputerScience,vol.9035,pp...

    2015 doi

  23. [31]

    David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf.17(4), 397–415 (2015).https:// doi.org/10.1007/s10009-014-0361-y

    2015 doi

  24. [32]

    IEEE Trans

    Deb, K., Agrawal, S., Pratap, A., Meyarivan, T.: A fast and elitist multiobjective genetic algorithm: NSGA-II. IEEE Trans. Evol. Comput.6(2), 182–197 (2002). https://doi.org/10.1109/4235.996017

    2002

  25. [33]

    In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010)

    Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010). pp. 342–351. IEEE Computer Society (2010).https://doi.org/10.1109/ LICS.2010.41

    2010

  26. [34]

    Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci.4(4) (2008).https://doi.org/10.2168/LMCS-4(4:8)2008

    2008 doi

  27. [35]

    In: Oh, A., Naumann, T., Glober- son, A., Saenko, K., Hardt, M., Levine, S

    Felten, F., Alegre, L.N., Nowé, A., Bazzan, A.L.C., Talbi, E., Danoy, G., da Silva, B.C.: A toolkit for reliable benchmarking and research in multi-objective reinforcement learning. In: Oh, A., Naumann, T., Glober- son, A., Saenko, K., Hardt, M., Levine, S. (eds.) 37th Annual ...

  28. [36]

    In: 36th AAAI Conference on Artificial Intelligence (AAAI 2022)

    Fickert, M., Gu, T., Ruml, W.: New results in bounded-suboptimal search. In: 36th AAAI Conference on Artificial Intelligence (AAAI 2022). pp. 10166–10173. AAAI Press (2022).https://doi.org/10.1609/AAAI.V36I9.21256

    2022 doi

  29. [37]

    In: Bernardo, M., Issarny, V

    Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) 11th In- ternationalSchoolonFormalMethodsfortheDesignofComputer,Communication and Software Systems (SFM 2011). Lecture Notes...

    2011 doi

  30. [38]

    In: Abdulla, P.A., Leino, K.R.M

    Forejt,V.,Kwiatkowska,M.Z.,Norman,G.,Parker,D.,Qu,H.:Quantitativemulti- objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) 17th International Conference on Tools and Algorithms for the Construc- tion and Analysis of Systems (TACAS 2011). ...

    2011 doi

  31. [39]

    Lecture Notes in Computer Science, vol

    Forejt, V., Kwiatkowska, M.Z., Parker, D.: Pareto curves for probabilistic model checking.In:Chakraborty,S.,Mukund,M.(eds.) 10th InternationalSymposiumon Automated Technology for Verification and Analysis (ATVA 2012). Lecture Notes in Computer Science, vol. 7561, pp. 317–332. ...

    2012 doi

  32. [40]

    In: Finkbeiner, B., Wies, T

    Fu, C., Hahn, E.M., Li, Y., Schewe, S., Sun, M., Turrini, A., Zhang, L.: EPMC gets knowledge in multi-agent systems. In: Finkbeiner, B., Wies, T. (eds.) 23rd International Conference on Verification, Model Checking, and Abstract Interpre- tation (VMCAI 2022). Lecture Notes in ...

    2022 doi

  33. [41]

    Gardner, M.: Mathematical games. Sci. Am.228(1), 118 (1973).https:// doi.org/10.1038/scientificamerican0173-108

    1973 doi

  34. [42]

    Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Steinmetz, M.: Analyzing neural network behavior through deep statistical model checking. Int. J. Softw. Tools Technol. Transf.25(3), 407–426 (2023).https://doi.org/10.1007/S10009- 022-00685-9

    2023 doi

  35. [43]

    In: Huis- man, M., Pasareanu, C.S., Zhan, N

    Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Model- free reinforcement learning for lexicographic omega-regular objectives. In: Huis- man, M., Pasareanu, C.S., Zhan, N. (eds.) 24th International Formal Methods Symposium (FM 2021). Lecture Notes in...

    2021

  36. [44]

    In: Ábrahám, E., Havelund, K

    Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). Lecture...

    2014 doi

  37. [45]

    In: Sankaranarayanan, S., Sharygina, N

    Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner’s guide to MDP model checking algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) 29th International Conference on Tools and Algorithms for the Construction and AnalysisofSystems(TACAS2023).LectureNo...

    2023 doi

  38. [46]

    In: Vojnar, T., Zhang, L

    Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantita- tive verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and Analysis of Sys- tems (TACAS 2019). Lecture Notes i...

    2019 doi

  39. [47]

    In: 2017 Winter Simulation Conference (WSC 2017)

    Hartmanns, A., Sedwards, S., D’Argenio, P.R.: Efficient simulation-based verifica- tion of probabilistic timed automata. In: 2017 Winter Simulation Conference (WSC 2017). pp. 1419–1430. IEEE (2017).https://doi.org/10.1109/WSC.2017.8247885

    2017

  40. [48]

    Hasan, M.M., Lwin, K.T., Imani, M., Shabut, A.M., Bittencourt, L.F., Hossain, M.A.: Dynamic multi-objective optimisation using deep reinforcement learning: benchmark, algorithm and an application to identify vulnerable zones based on wa- terquality.Eng.Appl.Artif.Intell.86,107...

    2019

  41. [49]

    Hasrat, I.R., Jensen, P.G., Larsen, K.G., Srba, J.: A toolchain for domestic heat- pump control using Uppaal Stratego. Sci. Comput. Program.230, 102987 (2023). https://doi.org/10.1016/J.SCICO.2023.102987

    2023

  42. [50]

    Hayes, C.F., Rădulescu, R., Bargiacchi, E., Källström, J., Macfarlane, M., Rey- mond, M., Verstraeten, T., Zintgraf, L.M., Dazeley, R., Heintz, F., Howley, E., Irissappane, A.A., Mannion, P., Nowé, A., Ramos, G., Restelli, M., Vamplew, P., 22 Roijers,D.M.:Apracticalguidetomult...

    2022

  43. [51]

    Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf.24(4), 589–610 (2022). https://doi.org/10.1007/S10009-021-00633-Z

    2022 doi

  44. [52]

    MIT Press (1960)

    Howard, R.A.: Dynamic Programming and Markov Processes. MIT Press (1960)

    1960

  45. [53]

    In: 2003 IEEE International Symposium on Computational Intelligence in Robotics and Au- tomation (CIRA 2003)

    Ito, K., Gofuku, A., Imoto, Y., Takeshita, M.: A study of reinforcement learn- ing with knowledge sharing for distributed autonomous system. In: 2003 IEEE International Symposium on Computational Intelligence in Robotics and Au- tomation (CIRA 2003). pp. 1120–1125. IEEE (2003)...

    2003 arXiv

  46. [54]

    Jain,A.,Khetarpal,K.,Precup,D.:Safeoption-critic:learningsafetyintheoption- critic architecture. Knowl. Eng. Rev.36, e4 (2021).https://doi.org/10.1017/ S0269888921000035

    2021

  47. [55]

    In: Grohe, M., Koski- nen, E., Shankar, N

    Katoen, J.P.: The probabilistic model checking landscape. In: Grohe, M., Koski- nen, E., Shankar, N. (eds.) 31st Annual ACM/IEEE Symposium on Logic in Com- puter Science (LICS 2016). pp. 31–45. ACM (2016).https://doi.org/10.1145/ 2933575.2934574

    2016

  48. [56]

    In: Italiano, G.F., Pighizzini, G., Sannella, D

    Krähmann, D., Schubert, J., Baier, C., Dubslaff, C.: Ratio and weight quantiles. In: Italiano, G.F., Pighizzini, G., Sannella, D. (eds.) 40th International Symposium on Mathematical Foundations of Computer Science (MFCS 2015). Lecture Notes in Computer Science, vol. 9234, pp. ...

    2015 doi

  49. [57]

    In: Dawar, A., Grädel, E

    Kretínský, J., Meggendorfer, T.: Conditional value-at-risk for reachability and mean payoff in Markov decision processes. In: Dawar, A., Grädel, E. (eds.) 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018). pp. 609–618. ACM (2018).https://doi.org/10.1145/3...

    2018

  50. [58]

    In: Gopalakrishnan, G., Qadeer, S

    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilis- tic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) 23rd International Conference on Computer Aided Verification (CAV 2011). Lecture Notes in Com- puter Science, vol. 6806, pp. 585–591...

    2011

  51. [59]

    Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101–150 (2002).https://doi.org/10.1016/S0304-3975(01)00046-9

    2002 doi

  52. [62]

    In: Canal, C., Idani, A

    Legay, A., Sedwards, S., Traonouez, L.M.: Scalable verification of Markov decision processes. In: Canal, C., Idani, A. (eds.) 4th Workshop on Formal Methods in the Development of Software (WS-FMDS 2014). Lecture Notes in Computer Science, vol. 8938, pp. 350–362. Springer (2014...

    2014 doi

  53. [63]

    In: Shen, W., Abel, M., Matta, N., Barthès, J.A., Luo, J., Zhang, J., Zhu, H., Peng, K

    Li,L.,Li,G.,Cai,G.:AlocalParetofrontestimationframeworkformulti-objective optimization. In: Shen, W., Abel, M., Matta, N., Barthès, J.A., Luo, J., Zhang, J., Zhu, H., Peng, K. (eds.) 28th International Conference on Computer Supported Cooperative Work in Design (CSCWD 2025). p...

    2025

  54. [64]

    IEEE Trans

    Li, Z., Tang, J., Zhao, H., Chen, C., Xie, S.: Dictionary learning-structured rein- forcement learning with adaptive-sparsity regularizer. IEEE Trans. Aerosp. Elec- tron. Syst.60(2),1753–1769 (2024).https://doi.org/10.1109/TAES.2023.3342794

    2024

  55. [65]

    Springer (1966).https:// doi.org/10.1007/978-1-4613-8122-8

    Miller, R.G.: Simultaneous Statistical Inference. Springer (1966).https:// doi.org/10.1007/978-1-4613-8122-8

    1966 doi

  56. [66]

    Moffaert, K.V., Drugan, M.M., Nowé, A.: Scalarized multi-objective reinforcement learning:Noveldesigntechniques.In:2013IEEESymposiumonAdaptiveDynamic Programming and Reinforcement Learning (ADPRL 2013). pp. 191–199. IEEE (2013).https://doi.org/10.1109/ADPRL.2013.6615007

    2013

  57. [67]

    Nguyen, A.T., Reiter, S., Rigo, P.: A review on simulation-based optimization methods applied to building performance analysis. Appl. Energy113, 1043–1058 (2014).https://doi.org/10.1016/j.apenergy.2013.08.061

    2014 doi

  58. [68]

    Nguyen, T.T., Nguyen, N.D., Vamplew, P., Nahavandi, S., Dazeley, R., Lim, C.P.: A multi-objective deep reinforcement learning framework. Eng. Appl. Artif. Intell. 96, 103915 (2020).https://doi.org/10.1016/J.ENGAPPAI.2020.103915

    2020

  59. [69]

    In: Silva, S., Paquete, L

    Okumura, N., Takagi, T., Ohta, Y., Sato, H.: Pareto front upconvert on multi- objective building facility control optimization. In: Silva, S., Paquete, L. (eds.) Genetic and Evolutionary Computation Conference (GECCO 2023). pp. 1963–

    2023

  60. [70]

    In: Lamont, G.B., Haddad, H., Papadopoulos, G.A., Panda, B

    Parsopoulos, K.E., Vrahatis, M.N.: Particle swarm optimization method in multi- objective problems. In: Lamont, G.B., Haddad, H., Papadopoulos, G.A., Panda, B. (eds.) 2002 ACM Symposium on Applied Computing (SAC 2002). pp. 603–607. ACM (2002).https://doi.org/10.1145/508791.508907

    2002

  61. [71]

    In: 18th Annual Symposium on Foun- dations of Computer Science (FOCS 1977)

    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foun- dations of Computer Science (FOCS 1977). pp. 46–57. IEEE Computer Society (1977),https://doi.org/10.1109/SFCS.1977.32

    1977 doi

  62. [72]

    Wiley Series in Probability and Statistics, Wiley (1994).https:// doi.org/10.1002/9780470316887

    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Pro- gramming. Wiley Series in Probability and Statistics, Wiley (1994).https:// doi.org/10.1002/9780470316887

    1994 doi

  63. [73]

    Quatmann,T.:Verificationofmulti-objectiveMarkovmodels.Ph.D.thesis,RWTH Aachen University (2023).https://doi.org/10.18154/RWTH-2023-09669

    2023 doi

  64. [74]

    Quiroz, E.A.P., Apolinário, H.C.F., Villacorta, K.D.V., Oliveira, P.R.: A linear scalarization proximal point method for quasiconvex multiobjective minimization. J. Optim. Theory Appl.183(3), 1028–1052 (2019).https://doi.org/10.1007/ S10957-019-01582-Z

    2019

  65. [75]

    Formal Methods Syst

    Randour, M., Raskin, J.F., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. Formal Methods Syst. Des.50(2-3), 207–248 (2017). https://doi.org/10.1007/S10703-016-0262-7

    2017 doi

  66. [76]

    Sarker, R.A., Liang, K.H., Newton, C.S.: A new multiobjective evolutionary algo- rithm. Eur. J. Oper. Res.140(1), 12–23 (2002).https://doi.org/10.1016/S0377- 2217(01)00190-4

    2002 doi

  67. [77]

    Šidák, Z.: Rectangular confidence regions for the means of multivariate normal distributions. J. Am. Stat. Assoc.62(318), 626–633 (1967).https://doi.org/ 10.1080/01621459.1967.10482935 24

    1967

  68. [78]

    Singh, C.: Optimality conditions in multiobjective differentiable programming. J. Optim. Theory Appl.53(1), 115–123 (1987).https://doi.org/10.1007/ BF00938820

    1987

  69. [79]

    Future Gener

    Song, F., Xing, H., Wang, X., Luo, S., Dai, P., Li, K.: Offloading dependent tasks in multi-access edge computing: A multi-objective reinforcement learning approach. Future Gener. Comput. Syst.128, 333–348 (2022).https://doi.org/10.1016/ J.FUTURE.2021.10.013

    2022

  70. [80]

    Suman, B., Kumar, P.: A survey of simulated annealing as a tool for single and multiobjective optimization. J. Oper. Res. Soc.57(10), 1143–1160 (2006).https: //doi.org/10.1057/PALGRAVE.JORS.2602068

    2006 doi

  71. [81]

    In: Touretzky, D.S., Mozer, M., Hasselmo, M.E

    Sutton, R.S.: Generalization in reinforcement learning: Successful examples using sparse coarse coding. In: Touretzky, D.S., Mozer, M., Hasselmo, M.E. (eds.) Ad- vances in Neural Information Processing Systems 8 (NIPS 1995). pp. 1038–1044. MIT Press (1995),http://papers.nips.c...

    1995

  72. [82]

    MIT Press (2018)

    Sutton, R.S., Barto, A.G.: Reinforcement learning - an introduction, 2nd Edition. MIT Press (2018)

    2018

  73. [83]

    In: Pfen- ning, F

    Ummels, M., Baier, C.: Computing quantiles in Markov reward models. In: Pfen- ning, F. (ed.) 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2013). Lecture Notes in Computer Sci- ence, vol. 7794, pp. 353–368. Springer (2013)...

    2013 doi

  74. [84]

    Vamplew, P., Dazeley, R., Berry, A., Issabekov, R., Dekker, E.: Empirical evalua- tion methods for multiobjective reinforcement learning algorithms. Mach. Learn. 84(1-2), 51–80 (2011).https://doi.org/10.1007/S10994-010-5232-5

    2011 doi

  75. [85]

    Vargas, D.V., Murata, J., Takano, H., Delbem, A.C.B.: General subpopulation framework and taming the conflict inside populations. Evol. Comput.23(1), 1–36 (2015).https://doi.org/10.1162/EVCO_A_00118

    2015 doi

  76. [86]

    Wan, C., Chen, X., Liu, D.: A multi-objective-driven placement technique for dig- ital microfluidic biochips. J. Circuits Syst. Comput.28(5), 1950076:1–1950076:15 (2019).https://doi.org/10.1142/S0218126619500762

    2019 doi

  77. [87]

    IEEE Trans

    Wang, C., Hou, Y., Qiu, F., Lei, S., Liu, K.: Resilience enhancement with sequen- tially proactive operation strategies. IEEE Trans. Power Syst.32(4), 2847–2857 (2019).https://doi.org/10.1109/TPWRS.2016.2622858

    2019

  78. [88]

    Wang, W., Sebag, M.: Hypervolume indicator and dominance reward based multi- objective monte-carlo tree search. Mach. Learn.92(2-3), 403–429 (2013).https: //doi.org/10.1007/S10994-013-5369-0

    2013 doi

  79. [89]

    In: Coelho, H., Studer, R., Wooldridge, M.J

    Warnquist, H., Kvarnström, J., Doherty, P.: Iterative bounding LAO. In: Coelho, H., Studer, R., Wooldridge, M.J. (eds.) 19th European Conference on Artificial Intelligence (ECAI 2010). Frontiers in Artificial Intelligence and Applications, vol. 215, pp. 341–346. IOS Press (201...

    2010 doi

  80. [90]

    In: 2014 IEEE Symposium on Adaptive Dynamic Pro- gramming and Reinforcement Learning (ADPRL 2014)

    Wiering, M.A., Withagen, M., Drugan, M.M.: Model-based multi-objective re- inforcement learning. In: 2014 IEEE Symposium on Adaptive Dynamic Pro- gramming and Reinforcement Learning (ADPRL 2014). pp. 1–6. IEEE (2014). https://doi.org/10.1109/ADPRL.2014.7010622

    2014

  81. [91]

    In: Bonet, B., Koenig, S

    Wray, K.H., Zilberstein, S., Mouaddib, A.I.: Multi-objective MDPs with condi- tional lexicographic reward preferences. In: Bonet, B., Koenig, S. (eds.) 29th AAAI Conference on Artificial Intelligence (AAAI 2015). pp. 3418–3424. AAAI Press (2015).https://doi.org/10.1609/AAAI.V2...

    2015 doi

  82. [92]

    In: Yamamoto, S., Mori, H

    Yamaguchi, T., Nagahama, S., Ichikawa, Y., Takadama, K.: Model-based multi- objective reinforcement learning with unknown weights. In: Yamamoto, S., Mori, H. (eds.) Thematic Area on Human Interface and the Management of Information (HIMI 2019), part of the 21st International C...

    2019 doi

  83. [93]

    In: Brinksma, E., Larsen, K.G

    Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event sys- tems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) 14th In- ternational Conference on Computer Aided Verification (CAV 2022). Lecture Notes in Computer Science, vol. 2404, pp. 2...

    2022 doi

  84. [94]

    IEEE Trans

    Zhang, X., Tian, Y., Jin, Y.: A knee point-driven evolutionary algorithm for many- objective optimization. IEEE Trans. Evol. Comput.19(6), 761–776 (2015).https: //doi.org/10.1109/TEVC.2014.2378512

    2015

  85. [95]

    EURASIP J

    Zhu, Y., Liang, S., Xue, G., Yang, R., Wu, X.: An efficient multi-objective opti- mization approach for sensor management via multi-Bernoulli filtering. EURASIP J. Adv. Signal Process.2022(1), 62 (2022).https://doi.org/10.1186/S13634- 022-00881-4

    2022 doi

  86. [96]

    In: Branke, J., Deb, K., Miettinen, K., Slowinski, R

    Zitzler, E., Knowles, J.D., Thiele, L.: Quality assessment of Pareto set approxima- tions. In: Branke, J., Deb, K., Miettinen, K., Slowinski, R. (eds.) Outcome of the Dagstuhl seminar on Multiobjective Optimization, Interactive and Evolutionary Approaches. Lecture Notes in Com...

    2008 doi

  87. [97]

    In: Eiben, A.E., Bäck, T., Schoenauer, M., Schwefel, H.P

    Zitzler, E., Thiele, L.: Multiobjective optimization using evolutionary algorithms – a comparative case study. In: Eiben, A.E., Bäck, T., Schoenauer, M., Schwefel, H.P. (eds.) 5th International Conference on Parallel Problem Solving from Nature (PPSN 1998). Lecture Notes in Co...

    1998 doi

  88. [98]

    ground truth

    Zitzler, E., Thiele, L., Laumanns, M., Fonseca, C.M., da Fonseca, V.G.: Per- formance assessment of multiobjective optimizers: an analysis and review. IEEE Trans. Evol. Comput.7(2), 117–132 (2003).https://doi.org/10.1109/ TEVC.2003.810758 26 A Added Benchmark Models We provide...

    2003

  89. [159]

    Springer (2021).https://doi.org/10.1007/978-3-030-90870-6_8

    2021 doi

  90. [1971]

    ACM (2023).https://doi.org/10.1145/3583133.3596339

    2023

  91. [2023]

    (2023),http://papers.nips.cc/paper_files/paper/2023/hash/ 4aa8891583f07ae200ba07843954caeb-Abstract-Datasets_and_Benchmarks.html

    2023

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.