• Novel Mapper-Based Topological Data Analysis Approach : Proposes a Mapper-based approach with expert knowledge to identify agents likely to be exposed to and influenced by information spread while minimizing false positives. • Validated on Synthetic & Empirical Data : Validates the approach using synthetic data with ground truth and empirical data with the statistical analysis using topological features of the data. • Superior Performance in Market Surveillance : Outperforms traditional anomaly detection and clustering methods in identifying information-driven trading behaviors. • Broad Applicability : Extends beyond finance to disease spreading and misinformation analysis, offering a versatile tool for contagion detection. Building on topological data analysis and expert knowledge, this study introduces a Mapper-based approach to cluster agents based on their tendency to be influenced by information spread. The context of our paper is financial markets with an aim to identify agents trading opportunistically on insider information while minimizing false positives, a critical challenge in financial market surveillance. We verify and demonstrate our methods using both synthetic and empirical data on insider networks and investor-level transactions in a stock market. Recognizing the sensitive nature of insider trading cases, we design a conservative approach to minimize false positives, ensuring that innocent agents are not wrongfully implicated. We find that the mapper-based method systematically outperforms other methods on synthetic data with ground truth. We also apply the method to empirical data and verify the results using a statistical validation method based on persistence homology. Our findings indicate that the proposed Mapper-based technique effectively identifies a subset of agents who tend to take advantage of inside information they have received. This method is highly adaptable to various applications involving the spread of information or diseases, where agents exhibit only indirect evidence of their carrier status (symptoms) through their behavior.

Loop invariant generation is a fundamental problem in program analysis and verification. In this work, we propose a new approach to automatically constructing inductive loop invariants. The key idea is to aggressively squeeze an inductive invariant based on Craig interpolants between forward and backward reachability analysis. We have evaluated our approach by a set of loop benchmarks, and experimental results show that our approach is promising.

Many algorithms for computing minimal coverability sets for Petri nets prune futures. That is, if a newmarking strictly covers an old one, then not just the old marking but also some subset of its successor markings is discarded from search. In this publication, a simpler algorithm that lacks future pruning is presented and proven correct. Its performance is compared with future pruning. It is demonstrated, using examples, that neither approach is systematically better than the other. However, the simple algorithm has some attractive features. It never needs to re-construct pruned parts of the minimal coverability set. It automatically gives most of the advantage of future pruning, if the minimal coverability set is constructed in depth-first or most tokens first order, and if so-called history merging is applied. Some implementation aspects of minimal coverability set construction are also discussed. Some measurements are given to demonstrate the effect of construction order and other implementation aspects.

Confluence reduction and partial order reduction by means of ample sets are two different techniques for state space reduction in both traditional and probabilistic model checking. This paper provides an extensive comparison between these two methods, and answers the question how they relate in terms of reduction power when preserving branching time properties. We prove that, while both preserve the same properties, confluence reduction is strictly more powerful than partial order reduction: every reduction that can be obtained with partial order reduction can also be obtained with confluence reduction, but the converse is not true. The main challenge for the comparison is that confluence reduction was defined in an action-based setting, whereas ample set reduction is often defined in a state-based setting. We therefore redefine confluence reduction in the state-based setting of Markov decision processes, and provide a nontrivial proof of its correctness. Additionally, we pinpoint precisely in what way confluence reduction is more general, and provide conditions under which the two notions coincide. The results we present also hold for non-probabilistic models, as they can just as well be applied in a context where all transitions are non-probabilistic. To discuss the practical applicability of our results, we adapt a state space generation technique based on representative states, already known in combination with confluence reduction, so that it can also be applied to ample sets.

Literature on the stubborn set and similar state space reduction methods presents numerous seemingly ad-hoc conditions for selecting the transitions that are investigated in the current state. There are good reasons to believe that the choice between

Minimal counterexamples are desirable, but expensive to compute. We propose four algorithms for computing small counterexamples that approximate the shortest case. Three of these use a new algorithm for automata-theoretic linear-time model checking, based on an early algorithm by Dijkstra for detecting strongly connected components. All four of the approximation algorithms rely on transitions shuffling; we show that the default transition ordering can behave badly. The algorithms are compared to a standard shortest counterexample algorithm on a large public data set.