Efficient Compliance Computation in Probabilistic Declarative Specifications

In this paper, we investigate the measurement of trace satisfaction probabilities within probabilistic Declare models, where Declare constraints are associated with probabilities. Each constraint, with a probability p, is independently included in a model with probability p or excluded with probability 1 - p. This probabilistic framework creates multiple possible worlds, each corresponding to a specific selection of constraints, with the probability of each world calculated as the product of the probabilities of its included constraints. A trace can be satisfied by some of these worlds, and the probability that a trace is satisfied is the sum of the probabilities of all satisfying worlds. We develop techniques to compute this satisfaction probability by integrating a tool that determines trace satisfaction for crisp Declare models with an implementation of the inclusion-exclusion principle. Our preliminary experiments compare the performance of our prototype with and without the inclusion-exclusion principle, highlighting its impact on the efficiency and accuracy of the probability computations. The results demonstrate the potential of our approach in enhancing the analysis of probabilistic Declare models, providing a foundation for more sophisticated probabilistic reasoning in process mining.