We propose a probabilistic verification framework that provides more focused information on differences among possible behaviours of the system, generalizing the ideas of quantile analysis or distribution-based semantics. We draw an analogy with database group-by queries: Instead of looking at all data points, we can aggregate the data by functions such as AVG, corresponding to the expected value, but also MIN, corresponding to the worst-case/sure-winning analysis, or other functions. Tailored aggregation of similar behaviours provides a more focused abstract view of the system, leading to better control and understanding of the system.
DFG Programme
Research Grants
