Hakan Younes: Probabilistic Verification of Descrete Event Systems using Acceptance Sampling

Abstract: We present a procedure for verifying properties of discrete event systems modeled as generalized semi-Markov processes. The dynamics of such systems can be very complex, which makes them hard to analyze. We resort to methods based on Monte Carlo simulation and statistical hypothesis testing. The verification is probabilistic in two senses. First, the properties, expressed as CSL formulas interpreted over generalized semi-Markov processes, can be probabilistic. Second, the result of the verification is probabilistic, and the probability of error is bounded by two parameters passed to the verification procedure.