Statistical model checking offers an alternative to traditional model checking for large stochastic systems, addressing state space explosion and approximating quantitative properties. This paper proposes machine learning approaches using decision trees to approximate zero-reachability states, offering both computational efficiency and interpretability. Statistical analysis is used as an alternative approach to establish simulation run length bounds to control computation errors. Experimental results across standard Markov models demonstrate that our decision structures maintain high correctness (99% in most cases), reduce runtime, and have minimal memory overhead. Even when some methods show limitations, alternative approaches within our framework yield effective results.
This research presents a novel hybrid portfolio optimization framework that combines the Hierarchical Risk Parity (HRP) algorithm with two Multi-Criteria Decision-Making (MCDM) methods, MEREC and WEDBA, specifically to overcome fundamental shortcomings in the standard HRP model. The central goal is to alleviate the chaining problem and resolve HRP’s difficulty in identifying the optimal number of clusters, issues known to negatively affect portfolio diversification and risk allocation. To achieve this structural improvement, the Elbow method is integrated directly into the HRP process, ensuring a robust cluster structure is defined before any weight allocation occurs. The MEREC method is then utilized to calculate objective criterion weights, while the WEDBA approach is employed to assess the financial performance of individual assets within each cluster generated by HRP. This HRP–MCDM algorithm is tested using daily closing price data for stocks on the BIST 100 Index covering the 2018–2022 period. The performance of portfolios generated across seven distinct linkage methods (Ward, single, complete, average, weighted, centroid, and median) is rigorously benchmarked against the outcomes from the traditional HRP approach. Findings demonstrate that the HRP–MCDM framework significantly boosts both return levels and risk-adjusted metrics, especially when using the single and Ward linkage method, thereby surpassing the standard HRP algorithm in the majority of test cases. By strategically blending machine-learning-based risk clustering with objective, multi-criteria evaluation, this study makes a vital methodological contribution to the portfolio optimization domain, equipping investors with a more stable, transparent, and performance-focused asset allocation instrument.
Verification in modern e-voting protocols allows voters and the general public to independently confirm the elections results. However, verification alone is insufficient to hold entities accountable for misconduct, or to protect honest participants from false accusations. This limitation is especially critical in voting protocols with multiple authorities, where the ability to identify the specific misbehaving entity is essential. We present DiReCT, the first multiparty protocol that integrates dispute resolution with individual accountability. Our protocol addresses two previously unresolved disputes: authorities blocking access to the election; and authorities denying the casting of a ballot. In addition, DiReCT improves timeliness, allowing misconducts to be proactively detected during the elections. As a result, voters can identify and recover from attacks that prevent their ballots from being recorded. Notably, DiReCT achieves these capabilities with low trust assumptions on the authorities.
Quality Function Deployment (QFD) is a technique used to collect Customer Requirements (CRs) for the product to be designed before the start of the manufacturing processes, and also used to determine whether CRs will be met with correlated or uncorrelated Design Requirements (DRs). In QFD technique, customers tend to explain their expectations from the product by using linguistic expressions instead of using exact numbers. Vagueness and impreciseness in linguistic expressions can be captured perfectly using fuzzy set theory. Pythagorean fuzzy (PF) sets as one of the extensions of ordinary fuzzy sets offer the decision maker a larger membership and non-membership assignment region than ordinary intuitionistic fuzzy sets. In this paper, customer requirements in QFD analysis are prioritized by Best-Worst Method (BWM), which has become a very popular optimization-based weighting method in recent years. In the proposed BWM and QFD methodology, interval-valued Pythagorean fuzzy (IVPF) sets are used for the first time in order to handle the uncertainties in the linguistic judgments. In the application, the two-phase IVPF methodology is proposed to a real life e-scooter design problem addressing 12 customer & 12 design requirements. The proposed PF methodology could determine the weights of customer requirements, and identify which of the design requirements is stronger, and make a competitive analysis to reveal the position of our company in the market under fuzzy environment. Besides, the sensitivity and comparative analyses have demonstrated the dominance of our company over the other competitors.