9607 research outputs found
Sort by
A Sound and Complete Projection for Global Types.
No full textMultiparty session types is a typing discipline used to write specifications, known as global types, for branching and recursive message-passing systems. A necessary operation on global types is projection to abstractions of local behaviour, called local types. Typically, this is a computable partial function that given a global type and a role erases all details irrelevant to this role. Computable projection functions in the literature are either unsound or too restrictive when dealing with recursion and branching. Recent work has taken a more general approach to projection defining it as a coinductive, but not computable, relation. Our work defines a new computable projection function that is sound and complete with respect to its coinductive counterpart and, hence, equally expressive. All results have been mechanised in the Coq proof assistant
Soft Manipulation Surface With Reduced Actuator Density For Heterogeneous Object Manipulation.
No full textObject manipulation in robotics faces challenges due to diverse object shapes, sizes, and fragility. Gripper-based methods offer precision and low degrees of freedom (DOF) but the gripper limits the kind of objects to grasp. On the otherhand, surface-based approaches provide flexibility for handling fragile and heterogeneous objects but require numerous actuators, increasing complexity. Wepropose new manipulation hardware that utilizes equally spaced linear actuators placed vertically and connected by a soft surface. In this setup, objectmanipulation occurs on the soft surface through coordinated movements of the surrounding actuators. This approach requires fewer actuators to cover a largemanipulation area, offering a cost-effective solution with a lower DOF compared to dense actuator arrays. It also effectively handles heterogeneous objects of varying shapes and weights, even when they are significantly smaller than the distance between actuators. This method is particularly suitable for managing highly fragile objects in the food industry
Proceedings of the 6th Workshop on Computational Approaches to Discourse, Context and Document-Level Inferences (CODI 2025)
No full textThermal Cards: From Classical Chinese Poetry to Designerly Lenses on Thermal-Affective Technology
No full textA "warm" smile? A "cold" rage? Thermal and emotional experiences are often tightly connected. In recent years HCI has investigated opportunities for thermal technologies to enrich user experience. However, our vocabulary for these experiences has remained limited and inexpressive: "hot", "cold", "warm", "cool". This limits our ability to describe and conceptualise experience, and impedes the exploration of design features for thermal and affective interaction. Our pictorial offers resources to enrich language and clarify the design space for thermal and affective technologies. We expand a recently developed theoretical framework based on Chinese classical poetry to present six lenses on thermal and affective experience. The pictorial also functions as a deck of design cards with a design exemplar. Together these resources can help researchers and designers conceptualise thermal experience, explore parameters for experiential design, and design technologies for rich thermal and affective experience
Approximate Single-Linkage Clustering Using Graph-Based Indexes: MST-Based Approaches and Incremental Searchers.
Get PDFCurrent exact single-linkage clustering algorithms have asymptotically quadratic complexity. We present algorithms for approximate single-linkage clustering with empirically near-linear scalability. We explore both graph index-based incremental nearest neighbor search and an iterative exploration scheme on the graph index approximating the MST of the reachability graph similar to Kruskal. As graph index, we use both the bottom layer and a combination of all layers of an HNSW as a stand-in for connected search graphs. We provide experiments comparing the clusterings to baselines such as exact single linkage implementation and an algorithm using metric tree-based searchers. We explore the impact of the HNSW hyperparameters on the performance in terms of running time and clustering quality and evaluate the empirical asymptotic complexity
Model Checking Reachability Properties for Quantum Markov Chains
Get PDFWe propose a discrete time quantum Markov chain (QMC) related to previous proposals but yet with a different semantics. A probability measure is defined similar to as for DTMCs in contrast to e.g.\ the super operator valued measure. Our work is based on a simple imperative quantum pseudo programming language and its denotational semantics which naturally leads to a definition of a QMC. As a novelty we demonstrate how reachability events of a QMC expressed in a simple temporal logic like notation may be checked similar to as for DTMCs as transient state probabilities and how probability intervals of such events may be computed by smallest fixed-point solutions to linear equations
From Theory to Practice: Engineering Approximation Algorithms for Dynamic Orientation.
No full textDynamic graph algorithms have seen significant theoretical advancements, but practical evaluations often lag behind. This work bridges the gap between theory and practice by engineering and empirically evaluating recently developed approximation algorithms for dynamically maintaining graph orientations. We comprehensively describe the underlying data structures, including efficient bucketing techniques and round-robin updates. Our implementation has a natural parameter λ, which allows for a trade-off between algorithmic efficiency and the quality of the solution. In the extensive experimental evaluation, we demonstrate that our implementation offers a considerable speedup. Using different quality metrics, we show that our implementations are very competitive and can outperform previous methods. Overall, our approach solves more instances than other methods while being up to 112 times faster on instances that are solvable by all methods compared
Macro-types in multi-scale feedback systems: a conceptual framework
Get PDFLarge Complex Adaptive Systems (CAS) operate at multiple scales - processing various information flows, encoded at different granularities, over different substrates. Often, system scales are interconnected by feedback cycles, with micro-scales generating macro-scales, in turn influencing the micro-scales, and so on. E.g. foraging ants (micro) contribute to a pheromone trail (macro), which in turn guides their movement (micro) and updates the trail (macro). As these processes take widely different forms when occurring in different environments and accomplishing different functions, they may be difficult to detect, compare and transfer across CAS domains. We previously generalised such diverse processes, defining them explicitly as a Multi-Scale Feedback Systems (MSFS) design pattern. In this paper, we propose a conceptual framework for categorising macroprocesses in MSFS. This helps identify and analyse micro-macro feedback cycles across CAS domains; and engineer new CAS with specific constraints. We illustrate these concepts via CAS examples that fit the MSFS pattern via different variants. This contribution extends the theoretical basis of MSFS for dealing with the increasing complexity of modern environments
1st Workshop on Data Craft as Boundary AI Practice
No full textData is central to AI performance, yet its curation remains an invisible and labour-intensive process, often leading to biases and reliability issues. While HCI has explored methods to improve data work, a growing body of research embraces data imperfections in an artistic vein to provoke reflection on human-AI relations. This workshop examines "Data Craft"- practices that creatively manipulate data to challenge conventional AI narratives and lower barriers to public engagement. By framing data craft as a boundary practice, we explore its potential to foster dialogue on AI capabilities, limitations, and societal impact. The workshop will investigate how data craft can be systematically integrated into participatory AI efforts, moving beyond artistic spaces to inform public debate. Through hands-on exploration, we aim to uncover strategies for leveraging data craft to engage diverse communities in shaping AI discourse
Detecting bias in algorithms used to disseminate information in social networks and mitigating it using multiobjective optimization
No full textSocial connections are conduits through which individuals communicate, information propagates, and diseases spread. Identifying individuals who are more likely to adopt ideas and spread them is essential in order to develop effective information campaigns, maximize the reach of resources, and fight epidemics. Consequently, a lot of work has focused on identifying influencers in social networks with various influence maximization algorithms being proposed. Based on extensive computer simulations on synthetic and 10 diverse real-world social networks we show that seeding information in social networks using state-of-the-art influence maximization methods creates information gaps. Our results show that these algorithms select influencers who do not disseminate information equitably, threatening to create an increasingly unequal society. To overcome this issue, we devise a multiobjective algorithm which both maximizes influence and information equity. Our results demonstrate it is possible to reduce vulnerability at a relatively low trade-off with respect to spread. This highlights that in our search for maximizing the spread of information we do not need to compromise on information equality