arXiv subjects

Iain Phillips

Publications and source records attributed to Iain Phillips.

13 recordsLinked to original sources

arXiv2026

On the Encodability of Reversible Process Calculi

Reversibility, allowing one to execute a program not only forwards as usual, but also backwards, has emerged as a fundamental concept in computing, with applications ranging from debugging and fault tolerance to biological and quantum systems. CCSK, a reversible extension of CCS, is a paradigmatic model of reversible concurrent computation. In this paper, we investigate the encodability of CCSK into classical forward-only concurrent models. We establish a separation theorem showing that there is no basic, success-sensitive encoding of CCSK into CCS or the {\pi}-calculus, highlighting the strong impact of reversibility on expressive power. We then present an encoding of CCSK processes with only top-level parallel composition into the internal {\pi}-calculus, correct up to strong bisimilarity. We also identify a fundamental limitation: no parallel-preserving encoding of CCSK (with arbitrary parallel composition) into the {\pi}-calculus can be correct up to strong bisimilarity. Finally, we provide a parallel-preserving encoding correct under a weaker behavioural correspondence: weak mutual simulation. Our findings extend the literature of encodability results to reversible process calculi.

cs.LO↗

arXiv2026

A Framework for Evaluating Faithfulness in Explainable AI for Machine Anomalous Sound Detection Using Frequency-Band Perturbation

Explainable AI (XAI) is commonly applied to anomalous sound detection (ASD) models to identify which time-frequency regions of an audio signal contribute to an anomaly decision. However, most audio explanations rely on qualitative inspection of saliency maps, leaving open the question of whether these attributions accurately reflect the spectral cues the model uses. In this work, we introduce a new quantitative framework for evaluating XAI faithfulness in machine-sound analysis by directly linking attribution relevance to model behaviour through systematic frequency-band removal. This approach provides an objective measure of whether an XAI method for machine ASD correctly identifies frequency regions that influence an ASD model's predictions. By using four widely adopted methods, namely Integrated Gradients, Occlusion, Grad-CAM and SmoothGrad, we show that XAI techniques differ in reliability, with Occlusion demonstrating the strongest alignment with true model sensitivity and gradient-+based methods often failing to accurately capture spectral dependencies. The proposed framework offers a reproducible way to benchmark audio explanations and enables more trustworthy interpretation of spectrogram-based ASD systems.

cs.SD↗

arXiv2024

Dependence and Independence for Reversible Process Calculi

To refine formal methods for concurrent systems, there are several ways of enriching classical operational semantics of process calculi. One can enable the auditing and undoing of past synchronisations thanks to communication keys, thus easing the study of true concurrency as a by-product. Alternatively, proof labels embed information about the origins of actions in transition labels, facilitating syntactic analysis. Enriching proof labels with keys enables a theory of the relations on transitions and on events based on their labels only. We offer for the first time separate definitions of dependence relation and independence relation, and prove their complementarity on connected transitions instead of postulating it. Leveraging the recent axiomatic approach to reversibility, we prove the canonicity of these relations and provide additional tools to study the relationships between e.g., concurrency and causality on transitions and events. Finally, we make precise the subtle relationship between bisimulations based on both forward and backward transitions, on key ordering, and on dependency preservation, providing a direct definition of History Preserving bisimulation for CCS.

cs.LO↗

arXiv2024

Know Your Neighborhood: General and Zero-Shot Capable Binary Function Search Powered by Call Graphlets

Binary code similarity detection is an important problem with applications in areas such as malware analysis, vulnerability research and license violation detection. This paper proposes a novel graph neural network architecture combined with a novel graph data representation called call graphlets. A call graphlet encodes the neighborhood around each function in a binary executable, capturing the local and global context through a series of statistical features. A specialized graph neural network model operates on this graph representation, learning to map it to a feature vector that encodes semantic binary code similarities using deep-metric learning. The proposed approach is evaluated across five distinct datasets covering different architectures, compiler tool chains, and optimization levels. Experimental results show that the combination of call graphlets and the novel graph neural network architecture achieves comparable or state-of-the-art performance compared to baseline techniques across cross-architecture, mono-architecture and zero shot tasks. In addition, our proposed approach also performs well when evaluated against an out-of-domain function inlining task. The work provides a general and effective graph neural network-based solution for conducting binary code similarity detection.

cs.CR↗

arXiv2023

FASER: Binary Code Similarity Search through the use of Intermediate Representations

Being able to identify functions of interest in cross-architecture software is useful whether you are analysing for malware, securing the software supply chain or conducting vulnerability research. Cross-Architecture Binary Code Similarity Search has been explored in numerous studies and has used a wide range of different data sources to achieve its goals. The data sources typically used draw on common structures derived from binaries such as function control flow graphs or binary level call graphs, the output of the disassembly process or the outputs of a dynamic analysis approach. One data source which has received less attention is binary intermediate representations. Binary Intermediate representations possess two interesting properties: they are cross architecture by their very nature and encode the semantics of a function explicitly to support downstream usage. Within this paper we propose Function as a String Encoded Representation (FASER) which combines long document transformers with the use of intermediate representations to create a model capable of cross architecture function search without the need for manual feature engineering, pre-training or a dynamic analysis step. We compare our approach against a series of baseline approaches for two tasks; A general function search task and a targeted vulnerability search task. Our approach demonstrates strong performance across both tasks, performing better than all baseline approaches.

cs.CR↗

arXiv2023

An Axiomatic Theory for Reversible Computation

Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, and abstract models such as prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between various reversibility properties. In particular, we show how all properties we consider are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new properties related to causal consistent reversibility, namely causal liveness and causal safety, stating, respectively, that an action can be undone if (causal liveness) and only if (causal safety) it is independent from all the following actions. These properties come in three flavours: defined in terms of independent transitions, independent events, or via an ordering on events. Both causal liveness and causal safety are derivable from our axioms.

cs.LO↗

arXiv2020

Event structures for the reversible early internal Pi-calculus

The pi-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operational semantics of the pi-calculus have been proposed, which can be classified according to whether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics. The early version allows a process to receive names it already knows from the environment, while the late semantics and reduction semantics do not. All existing reversible versions of the pi-calculus use reduction or late semantics, despite the early semantics of the (forward-only) pi-calculus being more widely used than the late. We define piIH, the first reversible early pi-calculus, and give it a denotational semantics in terms of reversible bundle event structures. The new calculus is a reversible form of the internal pi-calculus, which is a subset of the pi-calculus where every link sent by an output is private, yielding greater symmetry between inputs and outputs.

cs.FL↗

arXiv2019

Reversible Causal Nets and Reversible Event Structures

One of the well-known results in concurrency theory concerns the relationship between event structures and occurrence nets: an occurrence net can be associated with a prime event structure, and vice versa. More generally, the relationships between various forms of event structures and suitable forms of nets have been long established. Good examples are the close relationship between inhibitor event structures and inhibitor occurrence nets, or between asymmetric event structures and asymmetric occurrence nets. Several forms of event structures suited for the modelling of reversible computation have recently been developed; also a method for reversing occurrence nets has been proposed. This paper bridges the gap between reversible event structures and reversible nets. We introduce the notion of reversible causal net, which is a generalisation of the notion of reversible unfolding. We show that reversible causal nets correspond precisely to a subclass of reversible prime event structures, the causal reversible prime event structures.

cs.LO↗

arXiv2018

A Parametric Framework for Reversible Pi-Calculi

This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in pi-calculus, which differ in the treatment of parallel extrusions of the same name. In this paper we present a uniform framework for reversible pi-calculi that is parametric with respect to a data structure that stores information about an extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We show that the (parametric) reversibility induced by our framework is causally-consistent and prove a causal correspondence between an appropriate instance of the framework and Boreale and Sangiorgi's causal semantics.

cs.FL↗

arXiv2018

A Parametric Framework for Reversible $π$-Calculi

This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in pi-calculus, which differ in the treatment of parallel extrusions of the same name. In this paper we present a uniform framework for reversible pi-calculi that is parametric with respect to a data structure that stores information about an extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We show that the (parametric) reversibility induced by our framework is causally- consistent and prove a causal correspondence between an appropriate instance of the framework and Boreale and Sangiorgi's causal semantics.

cs.LO↗

arXiv2017

Towards a Categorical Representation of Reversible Event Structures

We study categories for reversible computing, focussing on reversible forms of event structures. Event structures are a well-established model of true concurrency. There exist a number of forms of event structures, including prime event structures, asymmetric event structures, and general event structures. More recently, reversible forms of these types of event structures have been defined. We formulate corresponding categories and functors between them. We show that products and co-products exist in many cases. In most work on reversible computing, including reversible process calculi, a cause-respecting condition is posited, meaning that the cause of an event may not be reversed before the event itself. Since reversible event structures are not assumed to be cause-respecting in general, we also define cause-respecting subcategories of these event structures. Our longer-term aim is to formulate event structure semantics for reversible process calculi.

cs.LO↗

arXiv2011

A Logic with Reverse Modalities for History-preserving Bisimulations

We introduce event identifier logic (EIL) which extends Hennessy-Milner logic by the addition of (1) reverse as well as forward modalities, and (2) identifiers to keep track of events. We show that this logic corresponds to hereditary history-preserving (HH) bisimulation equivalence within a particular true-concurrency model, namely stable configuration structures. We furthermore show how natural sublogics of EIL correspond to coarser equivalences. In particular we provide logical characterisations of weak history-preserving (WH) and history-preserving (H) bisimulation. Logics corresponding to HH and H bisimulation have been given previously, but not to WH bisimulation (when autoconcurrency is allowed), as far as we are aware. We also present characteristic formulas which characterise individual structures with respect to history-preserving equivalences.

cs.LO↗

arXiv2010

Reverse Bisimulations on Stable Configuration Structures

The relationships between various equivalences on configuration structures, including interleaving bisimulation (IB), step bisimulation (SB) and hereditary history-preserving (HH) bisimulation, have been investigated by van Glabbeek and Goltz (and later Fecher). Since HH bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate forms of IB and SB where both forward and reverse transitions are allowed. We give various characterisations of reverse SB, showing that forward steps do not add extra power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as HH bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration.

cs.LO↗