Temporal logic model checking involves checking the state-space of a model of a system to determine whether errors can occur in the system. Often this involves checking symmetrically equivalent areas of the state-space. The use of symmetry reduction to increase the efficiency of model checking has inspired a wealth of activity in the area of model checking research. We provide a survey of the associated literature.

Tandem mass spectrometry (LC-MS/MS) is widely used to identify unknown ions in untargeted metabolomics. Data-dependent acquisition (DDA) chooses which ions to fragment based upon intensities observed in MS1 survey scans and typically only fragments a small subset of the ions present. Despite this inefficiency, relatively little work has addressed the development of new DDA methods, partly due to the high overhead associated with running the many extracts necessary to optimize approaches in busy MS facilities. In this work, we first provide theoretical results that show how much improvement is possible over current DDA strategies. We then describe an in silico framework for fast and cost-efficient development of new DDA strategies using a previously developed virtual metabolomics mass spectrometer (ViMMS). Additional functionality is added to ViMMS to allow methods to be used both in simulation and on real samples via an Instrument Application Programming Interface (IAPI). We demonstrate this framework through the development and optimization of two new DDA methods that introduce new advanced ion prioritization strategies. Upon application of these developed methods to two complex metabolite mixtures, our results show that they are able to fragment more unique ions than standard DDA strategies.

Many complex combinatorial problems arising from a range of scientific applications (such as computer networks, mathematical chemistry and bioinformatics) involve searching for an undirected graph satisfying a given property. Since for any possible solution there can be a large number of isomorphic representations, these problems can quickly become intractable. One way to mitigate this problem is to eliminate as many isomorphic copies as possible by breaking symmetry during search - i.e. by introducing constraints that ensure that at least one representative graph is generated for each equivalence class, but not the entire class. The goal is to generate as few members of each class as possible - ideally exactly one: the symmetry break is said to be complete in this case. In this paper we introduce novel, effective and compact, symmetry breaking constraints for undirected graph search. While incomplete, these prove highly beneficial in pruning the search for a graph. We illustrate the application of symmetry breaking in graph representation to resolve several open instances in extremal graph theory. We also illustrate the application of our approach to graph edge coloring problems which exhibit additional symmetries due to the fact that the colors of the edges in any solution can be permuted.

Generic representatives have been proposed for the effective combination of symmetry reduction and symbolic representation with BDDs in non-probabilistic model checking. This approach involves the translation of a symmetric source program into a reduced program, in which counters are used to generically represent states of the original model. Symmetric properties of the original program can also be translated, and checked directly over the reduced program. We extend this approach to apply to probabilistic systems with Markov decision process or discrete time Markov chain semantics, represented as MTBDDs. We have implemented a prototype tool, GRIP, which converts a symmetric PRISM program and PCTL property into reduced form. Model checking results for the original program can then be inferred by applying PRISM, unchanged, to the smaller model underlying the reduced program. We present encouraging experimental results for two case studies.