Abstract

Controller synthesis is pivotal in automating control system design from formal specifications and enhancing industrial system verification and optimization processes. This paper critically evaluates LTL-based controller synthesis, highlighting significant gaps in tool support that hinder its widespread adoption in the industry. Despite substantial theoretical progress, an apparent disparity persists between academic research outcomes and the robust, practical tools demanded by industry. Through a comprehensive evaluation, this study reveals mismatches between industrial requirements and the capabilities of current open-source tools. The findings emphasize underexplored challenges and propose future research directions and strategies for practical integration. This work aims to bridge the gap by advocating for enhanced tool support, enabling solutions that align with industrial standards and fostering the broader application of controller synthesis across various sectors.

Abstract

Graphs, including, for example, social networks, collaboration networks, and epidemiological networks, offer a way to represent relationships among entities. Graphs arising from most real-world phenomena are not static and evolve. Dealing with such dynamic graphs requires special algorithms, known as dynamic graph algorithms, that update the required graph analytic based on the change in the current graph instead of recomputing the analytic from scratch. Parallel dynamic graph algorithms are now known for various graph problems such as connectivity, spanning trees, shortest paths, centrality metrics, and community detection. Dynamic algorithms often work in settings where a batch of edge insertions/deletions affects the current graph.

Abstract

Scene text recognition has historically concentrated on English, with limited advancements in developing solutions that perform well across multiple languages. Previous efforts in multilingual scene text recognition have predominantly targeted languages with considerable syntactic and semantic differences. However, Indian languages, while diverse, share numerous common features that remain largely underutilized. This competition aims to address the often-overlooked challenge of scene text recognition within the Indian context and to advance robust word image recognition across ten Indian languages. The dataset provided for this competition is one of the most comprehensive multilingual datasets, encompassing 10 languages, each with 17,500 training samples, 2,500 validation samples and 5,000 test word-image samples. The task was to correctly recognize the word-images, for which we received forty-nine registrations and five final submissions from industrial and research communities. The winning team achieved an average Character Recognition Rate (CRR) of 92.85% and a Word Recognition Rate (WRR) of 84.01% across the ten languages. This paper details the proposed dataset and summarizes the submissions for the competition- WIRIndic-2024.

Abstract

In this work, we introduce an innovative approach to estimate the vital signs of multiple human subjects simultaneously in a non-contact way using a Frequency Modulated Continuous Wave (FMCW) radar-based system. Traditional vital sign monitoring methods often face significant limitations, including subject discomfort with wearable devices, challenges in calibration, and the risk of infection transmission through contact measurement devices. To address these issues, this research is motivated by the need for versatile, non-contact vital monitoring solutions applicable in various critical scenarios. This work also explores the challenges of extending this capability to an arbitrary number of subjects, including hardware and theoretical limitations. Supported by rigorous experimental results and discussions, the paper illustrates the system’s potential to redefine vital sign monitoring. An FPGA-based implementation is also presented as proof of concept for a hardware-based and portable solution, improving upon previous works by offering 2.7x faster execution and 18.4% less Look-Up Table (LUT) utilization, as well as providing over 7400x acceleration compared to its software counterpart.

Abstract

With advances in vehicular communications technology such as Vehicle-to-Infrastructure (V2I) and Vehicle-to-Vehicle (V2V), the computation of vehicular tasks has become distributed facilitated by computation offloading from the vehicular platform to road side units (RSUs) or the cloud infrastructure. In this work, due to communication overheads, we do not consider the cloud and only consider offloading horizontally across RSU nodes. However, the advantage of offloading depends upon how the tasks are scheduled across the RSUs. Unlike existing horizontal offloading works, this work explores the benefits of online task partitioned scheduling for computation offloading from multiple vehicles to RSUs or edge nodes. Specifically, we propose a new efficient timeslot-based online hybrid partitioned scheduling algorithm, which splits some tasks into subtasks and schedules them across RSU nodes while considering vehicle flow constraints. We compared and evaluated the effectiveness of our proposed hybrid partitioned scheduling algorithm with the fully partitioned algorithm. We also compared the performance of the aforementioned algorithms with an optimal scheduling algorithm utilizing several experiments conducted on a real-world vehicular dataset.

Abstract

Finding a set of empirical criteria fulfilled by any theory that satisfies the generalized notion of noncontextuality is a challenging task of both operational and foundational importance. The conventional approach of deriving facet inequalities from the relevant noncontextual polytope is computationally demanding. Specifically, the noncontextual polytope is a product of two polytopes, one for preparations and the other for measurements, and the dimension of the former typically increases polynomially with the number of measurements. This work presents an alternative methodology for constructing a polytope that encompasses the actual noncontextual polytope while ensuring that the dimension of the polytope associated with the preparations remains constant regardless of the number of measurements and their outcome size. In particular, the facet inequalities of this polytope serve as necessary conditions for noncontextuality. To demonstrate the efficacy of our methodology, we apply it to nine distinct contextuality scenarios involving four to nine preparations and two to three measurements to obtain the respective sets of facet inequalities. Additionally, we retrieve the maximum quantum violations of these inequalities. Our investigation uncovers many novel non-trivial noncontextuality inequalities and reveals intriguing aspects and applications of quantum contextual correlations.

Abstract

Walking is one of the most natural ways to explore an environment. While Virtual Reality (VR) facilities simulation of infinite spaces, its limited by the physical space available. To address this limitation, several techniques have been proposed, such as redirected walking, walking in place, and teleportation. While some of these techniques, such as teleportation and walking in place, disrupt the natural immersion, others like redirected walking limit the walkable area within the virtual space. The concept of overlapping architecture tackles this challenge by compressing large virtual environments into smaller spaces. This is achieved by generating portions of an environment that might be physically impossible as a whole. In this paper, we propose a system for creating maze-based virtual environments with multi-path capabilities. This system allows for infinite natural walking experiences while maintaining architectural consistency. Specifically, our system can generate distinct, customizable, and scalable virtual mazes for physical areas exceeding 4x4 meters. The combination of multi-path capabilities and architectural consistency can enhance the overall maze traversal experience for end users.

Abstract

Funicular geometries, which are compression governing structural systems, are a significant part of our architectural heritage. To ensure the safety and serviceability of these historical infrastructures, where arches, vaults and domes are integral components, it is essential to have a comprehensive understanding of the structural behaviour of these geometries. Unlike conventional structural systems, the failure of funicular geometries is governed by the system equilibrium and geometric instability rather than strength exceedance. Further, the collapse behaviour of these structures is usually quantified either using simplified two dimensional analytical approaches, which might not be representative, or using complex numerical models, which might be computationally expensive. To address this, a novel analytical approach is proposed, leveraging structural geometry and system equilibrium to quantify the collapse behaviour of funicular structures.

Abstract

Addressing blockchain's insufficient throughput and scalability is imperative for practical viability. Off-chain approaches, such as state channels (including Hash Time Lock Contract (HTLC), virtual channels), demonstrate enhanced throughput by enabling parallel transaction processing. While virtual channels introduce execution complexity, HTLC suffers from high update delays. Moreover, existing methods face network attacks. We present Sharding-based Hybrid State Channel (SharHSC) to address these issues. Firstly, we introduce a novel off-chain sharding architecture, which partitions proxy nodes into multiple shards. Thus, when the off-chain node count increases, adding shards enhances system throughput. Secondly, each shard establishes a supervisory committee to record latest channel statuses to ensure accurate fund distribution upon channel closure. Thirdly, we combine the strengths of HTLC and virtual channels. In particular, SharHSC constructs a single virtual channel across all the nodes involved in the payment by treating the nodes between payer and payee as an intermediate entity, which utilizes HTLC for fund routing. This realizes both low latency and streamlined complexity. Finally, our work is substantiated by security analysis and experiments. As the node number varies, compared with HTLC and virtual channels, the latency is reduced by 49.32% and 31.82%, and the throughput is increased by 8.93 and 1.89 times.

Abstract

With an increasing number of vehicles on the road every day, intelligent traffic monitoring and control is essential. This entails development of cost-effective, scalable, and easy-to-install monitoring systems. In this letter, a versatile piezoresistance-based cost-effective on-road sensor system is presented to estimate vehicle speed and vehicle wheelbase length. The system consists of a velostat thin film sensing element placed on the road, with read out circuits and control electronics located at the sidewalk. The system measures the speed of a vehicle with 90.4% accuracy, and the length of the wheelbase with 94.3% accuracy. The wheelbase length can be used to classify the vehicle type. Our experiments show that the system is reliable, as the sensor output returns to the initial values after each vehicle passes. The utilization of flexible piezoresistive sensors makes this system convenient to deploy in different applications where basic traffic activity monitoring is required with speed, count, and classification estimation of vehicles.