Search

We introduce the notion of porous invariants for multipath affine loops over the integers. These are invariants definable in (fragments of) Presburger arithmetic and, as such, lack certain tame geometrical properties, such a convexity and connectedness. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle reachability questions for various non-trivial classes of affine loops and target sets. For the class of Z -linear invariants (those defined as conjunctions of linear equations with integer coefficients), we show that a strongest such invariant can be computed in polynomial time. For the more general class of N -semi-linear invariants (those defined as Boolean combinations of linear inequalities with integer coefficients), such a strongest invariant need not exist. Here we show that for point targets the existence of a separating invariant is undecidable in general. However we show that such separating invariants can be computed either by restricting the number of program variables or by restricting from multipath to single-path loops. Additionally, we consider porous targets, represented as Z -semi-linear sets (those defined as Boolean combinations of equations with integer coefficients). We show that an invariant can be computed providing the target spans the whole space. We present our tool porous, which computes porous invariants. [ABSTRACT FROM AUTHOR]

We study turn-based stochastic zero-sum games with lexicographic preferences over objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as controllable and adversarial non-determinism. Lexicographic order allows one to consider multiple objectives with a strict preference order. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. For a mixture of reachability and safety objectives, we show that deterministic lexicographically optimal strategies exist and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in NP ∩ coNP , matching the current known bound for single objectives; and in general the decision problem is PSPACE -hard and can be solved in NEXPTIME ∩ coNEXPTIME . We present an algorithm that computes the lexicographically optimal strategies via a reduction to the computation of optimal strategies in a sequence of single-objectives games. For omega-regular objectives, we restrict our analysis to one-player games, also known as Markov decision processes. We show that lexicographically optimal strategies exist and need either randomization or finite memory. We present an algorithm that solves the relevant decision problem in polynomial time. We have implemented our algorithms and report experimental results on various case studies. [ABSTRACT FROM AUTHOR]

We introduce a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the value of uncontrolled input. Robust reachability is better suited than standard reachability in many realistic situations related to security (e.g., criticality assessment or bug prioritization) or software engineering (e.g., replicable test suites and flakiness). We propose a formal treatment of the concept, and we revisit existing symbolic bug finding methods through this new lens. Remarkably, robust reachability allows differentiating bounded model checking from symbolic execution while they have the same deductive power in the standard case. Finally, we propose the first symbolic verifier dedicated to robust reachability: we use it for criticality assessment of 5 existing vulnerabilities, and compare it with standard symbolic execution. [ABSTRACT FROM AUTHOR]

The research examines the accessibility of museums in Istanbul for people with disabilities. The aim is to determine the suitability of museums in Istanbul for individuals with physical, visual, and hearing impairments, identify the problems they encounter in museums, identify physical limitations, and develop solution proposals. The qualitative research method was used in the research conducted in 2022-2023 covering museums in Istanbul. The research consists of two parts. In the first part, the museums to be visited were determined. Then, the checklists were submitted for approval to two expert academics. Opinions regarding the questions in the checklists were obtained by conducting a pilot study with six individuals with physical impairments, two with visual impairments, and two with hearing impairments. In the second part, the accessibility was evaluated by visiting 41 museums in Istanbul using checklists consisting of 23 questions. The findings were analyzed using the content analysis method. Considering the data of the research, none of the museums met the requirements for accessibility, museums were far from providing minimum standards for individuals with physical, visual, and hearing impairments, and individuals with physical, visual, and hearing impairments were unable to visit museums due to inadequate physical conditions rather than financial constraints. [ABSTRACT FROM AUTHOR]

This paper considers a skill learning method that does not use information about a goal set for an agent. In reinforcement learning, such methods are called intrinsic motivation methods. The proposed algorithm is based on the calculation of the mutual information between the actions of the agent and its states. This approach makes it possible to learn skills that lead to the most uniform reachability of possible states. The skills formed by the algorithm are illustrated by an example of continuous control of the agent's movement. The usefulness of these skills in solving reinforcement learning problems is analyzed. [ABSTRACT FROM AUTHOR]

Bipartite graphs are naturally used to model relationships between two types of entities, such as people-location, user-post, and investor-stock. When modeling real-world applications like disease outbreaks, edges are often enriched with temporal information, leading to temporal bipartite graphs. While reachability has been extensively studied on (temporal) unipartite graphs, it remains largely unexplored on temporal bipartite graphs. To fill this research gap, we study the reachability problem on temporal bipartite graphs in this paper. Specifically, a vertex u reaches a vertex w in a temporal bipartite graph G if u and w are connected through a series of consecutive wedges with time constraints. To efficiently answer if a vertex can reach the other vertex, we propose an index-based method by adapting the idea of 2-hop labeling. Effective optimization strategies and parallelization techniques are devised to accelerate the index construction process. To better support real-life scenarios, we further show how the index is leveraged to efficiently answer other types of queries, e.g., single-source reachability and earliest-arrival path queries. In addition, we propose an efficient method to handle incremental maintenance of the index structure. Extensive experiments on 16 real-world graphs demonstrate the effectiveness and efficiency of our proposed techniques. [ABSTRACT FROM AUTHOR]

In the allocation of indivisible goods, a prominent fairness notion is envy-freeness up to one good (EF1). We initiate the study of reachability problems in fair division by investigating the problem of whether one EF1 allocation can be reached from another EF1 allocation via a sequence of exchanges such that every intermediate allocation is also EF1. We show that two EF1 allocations may not be reachable from each other even in the case of two agents, and deciding their reachability is PSPACE-complete in general. On the other hand, we prove that reachability is guaranteed for two agents with identical or binary utilities as well as for any number of agents with identical binary utilities. We also examine the complexity of deciding whether there is an EF1 exchange sequence that is optimal in the number of exchanges required. [ABSTRACT FROM AUTHOR]

Parametric timed automata (PTA) have been introduced by Alur, Henzinger, and Vardi as an extension of timed automata in which clocks can be compared against parameters. The reachability problem asks for the existence of an assignment of the parameters to the non-negative integers such that reachability holds in the underlying timed automaton. The reachability problem for PTA is long known to be undecidable, already over three parametric clocks. A few years ago, Bundala and Ouaknine proved that for PTA over two parametric clocks and one parameter the reachability problem is decidable and also showed a lower bound for the complexity class PSPACENEXP. Our main result is that the reachability problem for two-parametric timed automata with one parameter is EXPSPACE-complete. Our contribution is two-fold. For the EXPSPACE lower bound, inspired by [13-14], we make use of deep results from complexity theory, namely a serializability characterization of EXPSPACE (in turn based on Barrington's Theorem) and a logspace translation of numbers in Chinese remainder representation to binary representation due to Chiu, Davida, and Litow. It is shown that with small PTA over two parametric clocks and one parameter one can simulate serializability computations. For the EXPSPACE upper bound, we first give a careful exponential time reduction from PTA over two parametric clocks and one parameter to a (slight subclass of) parametric one-counter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. For solving the reachability problem for parametric one-counter automata with one parameter, we provide a series of techniques to partition a fictitious run into several carefully chosen subruns that allow us to prove that it is sufficient to consider a parameter value of exponential magnitude only. This allows us to show a doubly-exponential upper bound on the value of the only parameter of a PTA over two parametric clocks and one parameter. We hope that extensions of our techniques lead to finally establishing decidability of the long-standing open problem of reachability in parametric timed automata with two parametric clocks (and arbitrarily many parameters) and, if decidability holds, determinining its precise computational complexity. [ABSTRACT FROM AUTHOR]

Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for checking non-emptiness of event-clock automata. As ECAs contain special prophecy clocks that guess and maintain the time to the next occurrence of specific events, they cannot be seen as a syntactic subclass of TA. Therefore, implementations for TA cannot be directly used for ECAs, and moreover the translation of an ECA to a semantically equivalent TA is expensive. Another reason for the lack of ECA implementations is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied by Geeraerts et al. in 2011, where the authors proposed a zone enumeration procedure that uses zone extrapolations for finiteness. In this article, we propose a different zone-based algorithm to solve the reachability problem for event-clock automata, using simulations for finiteness. A surprising consequence of our result is that for event-predicting automata, the subclass of event-clock automata that only use prophecy clocks, we obtain finiteness even without any simulations. For general event-clock automata, our new algorithm exploits the G-simulation framework, which is the coarsest known simulation relation in timed automata literature, and has been recently used for advances in other extensions of timed automata. [ABSTRACT FROM AUTHOR]

The reachable set of controlled dynamical systems is the set of all reachable states from an initial condition over a certain time horizon, subject to operational constraints and exogenous disturbances. In astrodynamics, rapid approximation of reachable sets is invaluable for trajectory planning, collision avoidance, and ensuring safe and optimal performance in complex dynamics. Leveraging the connection between minimum-time trajectories and the boundary of reachable sets, we propose a sampling-based method for rapid and efficient approximation of reachable sets for finite- and low-thrust spacecraft. The proposed method combines a minimum-time multi-stage indirect formulation with the celebrated primer vector theory. Reachable sets are generated under two-body and circular restricted three-body (CR3B) dynamics. For the two-body dynamics, reachable sets are generated for (1) the heliocentric phase of a benchmark Earth-to-Mars problem, (2) two scenarios with uncertainties in the initial position and velocity of the spacecraft at the time of departure from Earth, and (3) a scenario with a bounded single impulse at the time of departure from Earth. For the CR3B dynamics, several cislunar applications are considered, including L1 Halo orbit, L2 Halo orbit, and Lunar Gateway 9:2 NRHO. The results indicate that low-thrust spacecraft reachable sets coincide with invariant manifolds existing in multi-body dynamical environments. The proposed method serves as a valuable tool for qualitatively analyzing the evolution of reachable sets under complex dynamics, which would otherwise be either incoherent with existing grid-based reachability approaches or computationally intractable with a complete Hamilton–Jacobi–Bellman method. [ABSTRACT FROM AUTHOR]

The behavior of discrete-event systems, in which the individual components move from event to event rather than varying continuously through time, is often described by systems of linear equations in max-min algebra, in which classical addition and multiplication are replaced by ⊕ and ⊗, representing maximum and minimum, respectively. Max-min equations have found a broad area of applications in causal models, which emphasize relationships between input and output variables. Many practical situations can be described using max-min systems of linear equations. We shall deal with a two-sided max-min system of linear equations with unknown column vector x of the form A⊗x⊕c=B⊗x⊕d, where A, B are given square matrices, c, d are column vectors and operations ⊕ and ⊗ are extended to matrices and vectors in the same way as in the classical algebra. We give an equivalent condition for its solvability. For a given max-min objective function f, we consider optimization problem of type f⊤⊗x→max or min constraint to A⊗x⊕c=B⊗x⊕d. We solve the equation in the form f(x)=v on the set of solutions of the equation A⊗x⊕c=B⊗x⊕d and extend the problem to the case of an interval function f and an interval value v. We define several types of the reachability of the interval value v by the interval function f and provide equivalent conditions for them. [ABSTRACT FROM AUTHOR]

AbstractOne-handed interactions on smartphone interfaces offer a prominent feature of highly mobile inputs. Thus, the design factor of user reachability is essential to realizing the incentive. However, the sole consideration of physical characteristics, such as hand size and thumb length, does not fully reflect the users’ perceived choices of hand poses and the corresponding inertia. We first conducted a 6-week questionnaire-based study of UI rating tasks and collected 62,156 responses reflecting user preferences for 3000 clustered UIs. Our analysis of the responses shows that user perceptions of smartphone UI components are divergent from their physical ability of thumb reaches; e.g. they can reach an icon with a thumb reach, but they prefer alternative hand poses. Accordingly, we propose a machine learning model, i.e. XGBoost (XGB), to predict the user’s choices of hand poses, with a reasonable prediction accuracy of 64% that can be regarded as a practical preliminary evaluation tool. With illustrative examples, our model can offer auxiliary information in the assessment of perceived user reachability with one-handed interaction on smartphone interfaces, which paves a path toward a computational understanding of UI designs, and such findings can be further extended to 2D UIs in 3D worlds. [ABSTRACT FROM AUTHOR]

We abstract and study reachability preservers, a graph-theoretic primitive that has been implicit in prior work on network design. Given a directed graph G=(V,E) and a set of demand pairs P⊆VxV, a reachability preserver is a sparse subgraph H that preserves reachability between all demand pairs. Our first contribution is a series of extremal bounds on the size of reachability preservers. Our main result states that, for an n-node graph and demand pairs of the form P⊆SxV for a small node subset S, there is always a reachability preserver on O(n+√n/P//S/) edges. We additionally give a lower bound construction demonstrating that this upper bound characterizes the settings in which O(n) size reachability preservers are generally possible, in a large range of parameters. The second contribution of this paper is a new connection between extremal graph sparsification results and classical Steiner Network Design problems. Surprisingly, prior to this work, the osmosis of techniques between these two fields had been superficial. This allows us to improve the state of the art approximation algorithms for the most basic Steiner-type problem in directed graphs from the O(n0.6+ε) of Chlamatac, et al. [Approximating spanners and directed steiner forest: Upper and lower bounds, in Proceedings of the Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, Philadelphia, 2017, pp. 534-443] (n4/7+ε). [ABSTRACT FROM AUTHOR]

Software in autonomous systems like autonomous cars, robots or drones is often implemented on resource-constrained embedded systems with heterogeneous architectures. At the heart of such software are multiple feedback control loops, whose dynamics not only depend on the control strategy being used, but also on the timing behavior the control software experiences. But performing timing analysis for safety critical control software tasks, particularly on heterogeneous computing platforms, is challenging. Consequently, a number of recent papers have addressed the problem of stability analysis of feedback control loops in the presence of timing uncertainties (cf., deadline misses). In this paper, we address a different class of safety properties, viz., whether the system trajectory with timing uncertainties deviates too much from the nominal trajectory. Verifying such quantitative safety properties involves performing a reachability analysis that is computationally intractable, or is too conservative. To alleviate these problems we propose to provide statistical guarantees over the behavior of control systems with timing uncertainties. More specifically, we present a Bayesian hypothesis testing method that estimates deviations from a nominal or ideal behavior. We show that our analysis can provide, with high confidence, tighter estimates of the deviation from nominal behavior than using known reachability analysis methods. We also illustrate the scalability of our techniques by obtaining bounds in cases where reachability analysis fails, thereby establishing the practicality of our proposed method. [ABSTRACT FROM AUTHOR]

The behavior of discrete-event systems, in which the individual components move from event to event rather than varying continuously through time, is often described by systems of linear equations in max-min algebra, in which classical addition and multiplication are replaced by $ \oplus $ and $ {\otimes} $, representing maximum and minimum, respectively. Max-min equations have found a broad area of applications in causal models, which emphasize relationships between input and output variables. Many practical situations can be described using max-min systems of linear equations. We shall deal with a two-sided max-min system of linear equations with unknown column vector $ x $ of the form $ A{\otimes} x{\oplus} c = B{\otimes} x{\oplus} d $, where $ A $, $ B $ are given square matrices, $ c $, $ d $ are column vectors and operations $ \oplus $ and $ {\otimes} $ are extended to matrices and vectors in the same way as in the classical algebra. We give an equivalent condition for its solvability. For a given max-min objective function $ f $, we consider optimization problem of type $ f^\top{\otimes} x\rightarrow \max\text{ or } \min $ constraint to $ A{\otimes} x{\oplus} c = B{\otimes} x{\oplus} d $. We solve the equation in the form $ f(x) = v $ on the set of solutions of the equation $ A{\otimes} x{\oplus} c = B{\otimes} x{\oplus} d $ and extend the problem to the case of an interval function $ {{\boldsymbol{f}}} $ and an interval value $ {{\boldsymbol{v}}} $. We define several types of the reachability of the interval value $ {{\boldsymbol{v}}} $ by the interval function $ {{\boldsymbol{f}}} $ and provide equivalent conditions for them.

It is challenging in the e-healthcare system to monitor patients using wearables or embedded sensors that can gather real-time physiological data, analyze lab test results, conduct medical examinations, and recommend treatments because all the associated sensitive information transmission is through a hostile environment; it is always possible for an unauthorized person to access them. To improve the security of the telemedicine system in such a situation, it is imperative to develop a real-time data transmission system that can effectively handle the tasks carried out by devices in the telemedicine system. This allows administrators to assess the correctness of the various users’ work and remotely monitor the real-time data gathered by the smart sensing devices. However, as stated, the real-time data is shared across a public channel—and is private and sensitive; an attacker accesses the sensitive information about the telemedicine system and makes it public to disturb user privacy and violate its security. A robust and lightweight key agreement scheme must be designed for the telemedicine system to create a secret session key between a chosen wearable or smart sensing device and the telemedicine server—a trustworthy entity installed in the telehealthcare environment. Otherwise, security for such sensitive information cannot be guaranteed. Therefore, this article presents the design of a robust and lightweight authentication protocol named RLKAS-TMS that can effectively alleviate the security and privacy concerns of sensitive medical information over a public network channel.

The Internet of Drones (IoD) presents a crucial framework for managing drones in a decentralized manner, facilitating control, navigation, and access through the Internet. Given its importance in future generations, ensuring secure communication within this infrastructure is paramount. While existing authentication schemes have been proposed, they often suffer from design flaws or performance limitations, necessitating the development of more robust solutions. In response to these challenges, this article introduces a novel authentication scheme based on asymmetric cryptography tailored for the IoD environment. The scheme aims to address vulnerabilities in communication channels by providing strong authentication and cross-verification mechanisms. Formal scrutiny through GNY logic and ProVerif and informal validation through proposition demonstrate the security of the proposed scheme. Moreover, the scheme’s performance is rigorously analyzed regarding computation, communication, and storage overheads. The comparative analysis highlights the scheme’s ability to balance security and performance, positioning it as a viable solution for real-world implementation in IoD environments. Overall, this proposed authentication scheme represents a significant advancement in securing communication within the Internet of Drones, offering robust security and efficient performance for future applications.

During the decommissioning of the 101 reactor hot cell, there are some problems, such as high radiation level, small space, complex environment, etc. In order to complete the recovery of radioactive waste, decommissioning robot system was designed. The experimental verification of waste recovery was carried out on the platform of simulated hot cell. The results show that the robot is driven by hydraulic pressure and has 6 degrees of freedom. The load capacity of the robot is up to 30 kg under the condition of maximum arm span. In the bench examination, the decommissioning robot has high reachability, which can realize the recovery of the waste from the storage well and the ground of the hot cell. The decommission robot design is reasonable and the function can meet the requirements of the hot cell decommissioning. The results can provide technical support for the actual implementation of the project.

Copyright of Journal of Isotopes is the property of Journal of Isotopes Editorial Office and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

We consider a control system describing the interaction of water waves with a partially immersed rigid body constraint to move only in the vertical direction. The fluid is modeled by the shallow water equations. The control signal is a vertical force acting on the floating body. We first derive the full governing equations of the fluid-body system in a water tank and reformulate them as an initial boundary value problem of a first-order evolution system. We then linearize the equations around the equilibrium state and we study its well-posedness. Finally we focus on the reachability and stabilizability of the linear system. Our main result asserts that, provided that the floating body is situated in the middle of the tank, any symmetric waves with appropriate regularity can be obtained from the equilibrium state by an appropriate control force. This implies, in particular, that we can project this system on the subspace of states with appropriate symmetry properties to obtain a reduced system which is approximately controllable and strongly stabilizable. Note that, in general, this system is not controllable (even approximately). [ABSTRACT FROM AUTHOR]

Reachable and controllable sets for electric propulsion spacecraft are important to many problems including: dynamic replanning, robust mission design, space situational awareness, assessing advanced concepts, and threat assessments. Current methods result in a two-point boundary value problem or are limited in their application. The reachable and controllable problem is solved using an multistage indirect approach. The paper demonstrates our formulation enables rapid, reliable, and autonomous estimates of the reachable and controllable sets. Numerical examples show that the algorithms work in strong multibody environments (i.e., flybys) and incorporates uncertainty in initial conditions. These conditions make the algorithm suitable for space situational awareness and cislunar applications. [ABSTRACT FROM AUTHOR]

We prove that the reachability problem for two-dimensional vector addition systems with states is NL-complete or PSPACE-complete, depending on whether the numbers in the input are encoded in unary or binary. As a key underlying technical result, we show that, if a configuration is reachable, then there exists a witnessing path whose sequence of transitions is contained in a bounded language defined by a regular expression of pseudo-polynomially bounded length. This, in turn, enables us to prove that the lengths of minimal reachability witnesses are pseudo-polynomially bounded. [ABSTRACT FROM AUTHOR]

Vehicular ad-hoc network (VANET) is a technique that uses cars moved in cities or highways as nodes in wireless networks. Each car in these networks works as a router and allows cars in the range to communicate with each other. As a result of this movement, some cars will become out of range, but these networks can connect to the internet and the cars in these networks can connect to each other. This research proposes a unique clustering strategy to improve the performance of these networks by making their clusters more stable. One of the biggest problems these networks face is traffic data, which consumes network resources. Agent based modeling (ABM) evaluates better networks. The evaluation showed that the proposed strategy surpasses earlier techniques in reachability and throughput, but ad hoc on-demand distance vector (AODV) (on-demand/reactive) outperforms it in total traffic received since our hybrid approach needs more traffic than AODV. [ABSTRACT FROM AUTHOR]

This work outlines and assesses several methods for the detection of manoeuvres in Low Earth Orbit (LEO) from surveillance radar data. To be able to detect manoeuvres, the main starting assumption is that the object under analysis has an orbit known with a sufficient degree of precision. Based on the precise (a posteriori) orbit and radar data, several manoeuvre detection methods are presented; one is based on unscented Kalman filtering, whereas two others algorithms are based on reachability analysis of the state, which correlates its prediction set with the next track from the radar. The filtering algorithm can be extended for several radar tracks, whereas the reachability-based methods are more precise in detecting manoeuvres. Then, to inherit the best properties of both classes of algorithms, a manoeuvre detection filter that combines both concepts is finally presented. Manoeuvre detection results are analysed first for simulated scenarios—for validation and calibration purposes—and later for real data. Radar information comes from the Spanish Space Surveillance Radar (S3TSR), with real manoeuvre information and high-quality ephemerides. The results show promise, taking into account that a single surveillance radar is the only source of data, obtaining manoeuvre detection rates of more than 50% and false positive rates of less than 10%. [ABSTRACT FROM AUTHOR]

Neural networks are widely used in systems of artificial intelligence, but due to their black box nature, they have so far evaded formal analysis to certify that they satisfy desirable properties, mainly when they perform critical tasks. In this work, we introduce methods for the formal analysis of reachability and robustness of neural networks that are modeled as rational McNaughton functions by, first, stating such properties in the language of Łukasiewicz infinitely-valued logic and, then, using the reasoning techniques of such logical system. We also present a case study where we employ the proposed techniques in an actual neural network that we trained to predict whether it will rain tomorrow in Australia. [ABSTRACT FROM AUTHOR]