Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 3 of 3
Full-Text Articles in Physical Sciences and Mathematics
Improving Probability Estimation Through Active Probabilistic Model Learning, Jingyi Wang, Xiaohong Chen, Jun Sun, Shengchao Qin
Improving Probability Estimation Through Active Probabilistic Model Learning, Jingyi Wang, Xiaohong Chen, Jun Sun, Shengchao Qin
Research Collection School Of Computing and Information Systems
It is often necessary to estimate the probability of certain events occurring in a system. For instance, knowing the probability of events triggering a shutdown sequence allows us to estimate the availability of the system. One approach is to run the system multiple times and then construct a probabilistic model to estimate the probability. When the probability of the event to be estimated is low, many system runs are necessary in order to generate an accurate estimation. For complex cyber-physical systems, each system run is costly and time-consuming, and thus it is important to reduce the number of system runs …
Classification-Based Parameter Synthesis For Parametric Timed Automata, Jiaying Li, Jun Sun, Bo Gao, Étienne Andre
Classification-Based Parameter Synthesis For Parametric Timed Automata, Jiaying Li, Jun Sun, Bo Gao, Étienne Andre
Research Collection School Of Computing and Information Systems
Parametric timed automata are designed to model timed systems with unknown parameters, often representing design uncertainties of external environments. In order to design a robust system, it is crucial to synthesize constraints on the parameters, which guarantee the system behaves according to certain properties. Existing approaches suffer from scalability issues. In this work, we propose to enhance existing approaches through classification-based learning. We sample multiple concrete values for parameters and model check the corresponding non-parametric models. Based on the checking results, we form conjectures on the constraint through classification techniques, which can be subsequently confirmed by existing model checkers for …
Parametric Model Checking Timed Automata Under Non-Zenoness Assumption, Étienne Andre, Hoang Gia Nguyen, Laure Petrucci, Jun Sun
Parametric Model Checking Timed Automata Under Non-Zenoness Assumption, Étienne Andre, Hoang Gia Nguyen, Laure Petrucci, Jun Sun
Research Collection School Of Computing and Information Systems
Real-time systems often involve hard timing constraints and concurrency, and are notoriously hard to design or verify. Given a model of a real-time system and a property, parametric model-checking aims at synthesizing timing valuations such that the model satisfies the property. However, the counter-example returned by such a procedure may be Zeno (an infinite number of discrete actions occurring in a finite time), which is unrealistic. We show here that synthesizing parameter valuations such that at least one counterexample run is non-Zeno is undecidable for parametric timed automata (PTAs). Still, we propose a semi-algorithm based on a transformation of PTAs …