Search

Alternating timed automata (ATA) are an extension of timed automata, that are closed under complementation and hence amenable to logic-to-automata translations. Several timed logics, including Metric Temporal Logic (MTL), can be converted to equivalent 1-clock ATAs (1-ATAs). Satisfiability of an MTL formula therefore reduces to checking emptiness of a 1-ATA. Furthermore, algorithms for 1-ATA emptiness can be adapted for model-checking timed automata models against 1-ATA specifications. However, existing emptiness algorithms for 1-ATA proceed by an extended region construction, and are not suitable for implementations. In this work, we improve the existing MTL-to-1-ATA construction and develop a zone based emptiness algorithm for 1-ATAs. We first introduce a deactivation operation on the 1-ATA syntax to allow an explicit deactivation of the clock in transitions. Using the deactivation operation, we improve the existing MTL-to-1-ATA conversion and present a fragment of MTL for which the equivalent 1-ATA generate a bounded number of variables. Secondly, we develop the idea of zones for 1-ATA and present an emptiness algorithm which explores a corresponding zone graph. For termination, a special entailment check between zones is necessary. Our main technical contributions are: (1) an algorithm for the entailment check using simple zone operations and (2) an NP-hardness for the entailment check in the general case. Finally, for 1-ATA which generate a bounded number of variables, we present a modified entailment check with quadratic complexity., Comment: A shorter version appears in FoSSaCS 2025

We introduce deterministic suffix-reading automata (DSA), a new automaton model over finite words. Transitions in a DSA are labeled with words. From a state, a DSA triggers an outgoing transition on seeing a word ending with the transition's label. Therefore, rather than moving along an input word letter by letter, a DSA can jump along blocks of letters, with each block ending in a suitable suffix. This feature allows DSAs to recognize regular languages more concisely, compared to DFAs. In this work, we focus on questions around finding a "minimal" DSA for a regular language. The number of states is not a faithful measure of the size of a DSA, since the transition-labels contain strings of arbitrary length. Hence, we consider total-size (number of states + number of edges + total length of transition-labels) as the size measure of DSAs. We start by formally defining the model and providing a DSA-to-DFA conversion that allows to compare the expressiveness and succinctness of DSA with related automata models. Our main technical contribution is a method to derive DSAs from a given DFA: a DFA-to-DSA conversion. We make a surprising observation that the smallest DSA derived from the canonical DFA of a regular language L need not be a minimal DSA for L. This observation leads to a fundamental bottleneck in deriving a minimal DSA for a regular language. In fact, we prove that given a DFA and a number k, the problem of deciding if there exists an equivalent DSA of total-size at most k is NP-complete., Comment: In Proceedings GandALF 2024, arXiv:2410.21884

The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to the Myhill-Nerode theorem and a canonical automaton, which in turn, is the basis of several automata learning algorithms. A Nerode-like equivalence has been studied for various classes of timed languages. In this work, we focus on timed automata with integer resets. This class is known to have good automata-theoretic properties and is also useful for practical modeling. Our main contribution is a Nerode-style equivalence for this class that depends on a constant K. We show that the equivalence leads to a Myhill-Nerode theorem and a canonical one-clock integer-reset timed automaton with maximum constant K. Based on the canonical form, we develop an Angluin-style active learning algorithm whose query complexity is polynomial in the size of the canonical form., Comment: 25 pages, 6 figures, to be published at the 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science

The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the automata with a guess-and-check mechanism to ascertain the truth of future modalities. Guess-and-check can be naturally implemented via alternation. However, since timed automata tools do not handle alternation, existing methods perform an additional step of converting the alternating timed automata into timed automata. This de-alternation step proceeds by an intricate finite abstraction of the space of configurations of the alternating automaton. Recently, a model of generalized timed automata (GTA) has been proposed. The model comes with several powerful additional features, and yet, the best known zone-based reachability algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. We provide a new concise translation from MITL to GTA. In particular, for the timed until modality, our translation offers an exponential improvement w.r.t. the state-of-the-art. Thanks to this conversion, MITL model checking reduces to checking liveness for GTAs. However, no liveness algorithm is known for GTAs. Due to the presence of future clocks, there is no finite time-abstract bisimulation (region equivalence) for GTAs, whereas liveness algorithms for timed automata crucially rely on the presence of the finite region equivalence. As our second contribution, we provide a new zone-based algorithm for checking Buchi non-emptiness in GTAs, which circumvents this fundamental challenge.

Peptides are essential in biological processes and therapeutics. In this study, we introduce Multi-Peptide, an innovative approach that combines transformer-based language models with Graph Neural Networks (GNNs) to predict peptide properties. We combine PeptideBERT, a transformer model tailored for peptide property prediction, with a GNN encoder to capture both sequence-based and structural features. By employing Contrastive Language-Image Pre-training (CLIP), Multi-Peptide aligns embeddings from both modalities into a shared latent space, thereby enhancing the model's predictive accuracy. Evaluations on hemolysis and nonfouling datasets demonstrate Multi-Peptide's robustness, achieving state-of-the-art 86.185% accuracy in hemolysis prediction. This study highlights the potential of multimodal learning in bioinformatics, paving the way for accurate and reliable predictions in peptide-based research and applications.

Visible light positioning(VLP) has gained prominence as a highly accurate indoor positioning technique. Few techniques consider the practical limitations of implementing VLP systems for indoor positioning. These limitations range from having a single LED in the field of view(FoV) of the image sensor to not having enough images for training deep learning techniques. Practical implementation of indoor positioning techniques needs to leverage the ubiquity of smartphones, which is the case with VLP using complementary metal oxide semiconductor(CMOS) sensors. Images for VLP can be gathered only after the lights in question have been installed making it a cumbersome process. These limitations are addressed in the proposed technique, which uses simulated data of a single LED to train machine learning models and test them on actual images captured from a similar experimental setup. Such testing produced mean three dimensional(3D) positioning error of 2.88 centimeters while training with real images achieves accuracy of less than one centimeter compared to 6.26 centimeters of the closest competitor., Comment: To be presented in IEEE Region 10 technical conference, 31 oct-3 nov 2023, Chiang Mai, Thailand

Web users are increasingly presented with multiple login options, including password-based login and common web single sign-on (SSO) login options such as "Login with Google" and "Login with Facebook". There has been little focus in previous studies on how users choose from a list of login options and how to better inform users about privacy issues in web SSO systems. In this paper, we conducted a 200-participant study to understand factors that influence participants' login decisions, and how they are affected by displaying permission differences across login options; permissions in SSO result in release of user personal information to third-party web sites through SSO identity providers. We compare and report on login decisions made by participants before and after viewing permission-related information, examine self-reported responses for reasons related to their login decisions, and report on the factors that motivated their choices. We find that usability preferences and inertia (habituation) were among the dominant factors influencing login decisions. After participants viewed permission-related information, many prioritised privacy over other factors, changing their login decisions to more privacy-friendly alternatives. Displaying permission-related information also influenced some participants to make tradeoffs between privacy and usability preferences.

Negotiations, introduced by Esparza et al., are a model for concurrent systems where computations involving a set of agents are described in terms of their interactions. In many situations, it is natural to impose timing constraints between interactions -- for instance, to limit the time available to enter the PIN after inserting a card into an ATM. To model this, we introduce a real-time aspect to negotiations. In our model of local-timed negotiations, agents have local reference times that evolve independently. Inspired by the model of networks of timed automata, each agent is equipped with a set of local clocks. Similar to timed automata, the outcomes of a negotiation contain guards and resets over the local clocks. As a new feature, we allow some interactions to force the reference clocks of the participating agents to synchronize. This synchronization constraint allows us to model interesting scenarios. Surprisingly, it also gives unlimited computing power. We show that reachability is undecidable for local-timed negotiations with a mixture of synchronized and unsynchronized interactions. We study restrictions on the use of synchronized interactions that make the problem decidable., Comment: A shorter version appears in FORMATS 2023

In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with timers. Our main contribution is a new simulation-based zone algorithm for checking reachability in this unified model. While such algorithms are known to exist for timed automata, and have recently been shown for event-clock automata without diagonal constraints, this is the first result that can handle event-clock automata with diagonal constraints and automata with timers. We also provide a prototype implementation for our model and show experimental results on several benchmarks. To the best of our knowledge, this is the first effective implementation not just for our unified model, but even just for automata with timers or for event-clock automata (with predicting clocks) without going through a costly translation via timed automata. Last but not least, beyond being interesting in their own right, generalized timed automata can be used for model-checking event-clock specifications over timed automata models., Comment: arXiv admin note: text overlap with arXiv:2207.02633

In many modern data sets, High dimension low sample size (HDLSS) data is prevalent in many fields of studies. There has been an increased focus recently on using machine learning and statistical methods to mine valuable information out of these data sets. Thus, there has been an increased interest in efficient learning in high dimensions. Naturally, as the dimension of the input data increases, the learning task will become more difficult, due to increasing computational and statistical complexities. This makes it crucial to overcome the curse of dimensionality in a given dataset, within a reasonable time frame, in a bid to obtain the insights required to keep a competitive edge. To solve HDLSS problems, classical methods such as support vector machines can be utilised to alleviate data piling at the margin. However, when we question geometric domains and their assumptions on input data, we are naturally lead to convex optimisation problems and this gives rise to the development of solutions like distance weighted discrimination (DWD), which can be modelled as a second-order cone programming problem and solved by interior-point methods when sample size and feature dimensions of the data is moderate. In this paper, our focus is on designing an even more scalable and robust algorithm for solving large-scale generalized DWD problems., Comment: 34 pages. arXiv admin note: substantial text overlap with arXiv:1604.05473

The number of login options on web sites has increased since the introduction of web single sign-on (SSO) protocols. Web SSO services allow users to grant web sites or relying parties (RPs) access to their personal profile information from identity provider (IdP) accounts. Many RP sites fail to provide sufficient privacy-related information to allow users to make informed login decisions. Moreover, privacy differences in permission requests across login options are largely hidden from users and are time-consuming to manually extract and compare. In this paper, we present an empirical analysis of popular RP implementations supporting three major IdP login options (Facebook, Google, and Apple) and categorize RPs in the top 500 sites into four client-side code patterns. Informed by these RP patterns, we design and implement SSOPrivateEye (SPEye), a browser extension prototype that extracts and displays to users permission request information from SSO login options in RPs covering the three IdPs.

Timed automata have been introduced by Rajeev Alur and David Dill in the early 90's. In the last decades, timed automata have become the de facto model for the verification of real-time systems. Algorithms for timed automata are based on the traversal of their state-space using zones as a symbolic representation. Since the state-space is infinite, termination relies on finite abstractions that yield a finite representation of the reachable states. The first solution to get finite abstractions was based on extrapolations of zones, and has been implemented in the industry-strength tool Uppaal. A different approach based on simulations between zones has emerged in the last ten years, and has been implemented in the fully open source tool TChecker. The simulation-based approach has led to new efficient algorithms for reachability and liveness in timed automata, and has also been extended to richer models like weighted timed automata, and timed automata with diagonal constraints and updates. In this article, we survey the extrapolation and simulation techniques, and discuss some open challenges for the future., Comment: Invited contribution at FORMATS'22

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.

Two-factor authentication (2FA) offers several security benefits that security-conscious users might expect from high-value services such as online banks. In this work, we present our preliminary study to develop a scoring scheme to automatically recognize when bank sites mention support for two-factor authentication. We extract information related to security features (primarily 2FA) offered by 379 bank domains from 93 countries. We use a subset of these sites to refine our scoring scheme to include several heuristics for identifying whether sites offer 2FA. For each bank domain in our dataset, we use our algorithm based on text-analysis to calculate whether the domain offers 2FA to the users of the domain's online banking platform. Our preliminary findings suggest that 2FA is yet to be widely adopted by banking domains.

An information cascade is a circumstance where agents make decisions in a sequential fashion by following other agents. Bikhchandani et al., predict that once a cascade starts it continues, even if it is wrong, until agents receive an external input such as public information. In an information cascade, even if an agent has its own personal choice, it is always overridden by observation of previous agents' actions. This could mean agents end up in a situation where they may act without valuing their own information. As information cascades can have serious social consequences, it is important to have a good understanding of what causes them. We present a detailed Bayesian model of the information gained by agents when observing the choices of other agents and their own private information. Compared to prior work, we remove the high impact of the first observed agent's action by incorporating a prior probability distribution over the information of unobserved agents and investigate an alternative model of choice to that considered in prior work: weighted random choice. Our results show that, in contrast to Bikhchandani's results, cascades will not necessarily occur and adding prior agents' information will delay the effects of cascades., Comment: 13 pages, 37 figures, Paper accepted for presentation A Bayesian model of information cascade in International Workshop on Coordination, Organizations, Institutions, Norms and Ethics for Governance of Multi-Agent Systems (COINE), co-located with AAMAS 2021

Single sign-on authentication systems such as OAuth 2.0 are widely used in web services. They allow users to use accounts registered with major identity providers such as Google and Facebook to login on multiple services (relying parties). These services can both identify users and access a subset of the user's data stored with the provider. We empirically investigate the end-user privacy implications of OAuth 2.0 implementations in relying parties most visited around the world. We collect data on the use of OAuth-based logins in the Alexa Top 500 sites per country for five countries. We categorize user data made available by four identity providers (Google, Facebook, Apple and LinkedIn) and evaluate popular services accessing user data from the SSO platforms of these providers. Many services allow users to choose from multiple login options (with different identity providers). Our results reveal that services request different categories and amounts of personal data from different providers, with at least one choice undeniably more privacy-intrusive. These privacy choices (and their privacy implications) are highly invisible to users. Based on our analysis, we also identify areas which could improve user privacy and help users make informed decisions.

The gas-phase reaction of CCl+ with acetonitrile (CH3CN) is studied using a linear Paul ion trap coupled to a time-of-flight mass spectrometer. This work builds on a previous study of the reaction of CCl+ with acetylene and further explores the reactivity of CCl+ with organic neutral molecules. Both of the reactant species are relevant in observations and models of chemistry in the interstellar medium (ISM). Nitriles, in particular, are noted for their relevance in prebiotic chemistry, such as is found in the atmosphere of Titan, one of Saturn's moons. This work represents one of the first studied reactions of a halogenated carbocation with a nitrile, and the first exploration of CCl+ with a nitrile. Reactant isotopologues are used to unambiguously assign ionic primary products from this reaction: HNCCl+ and C2H3+. Branching ratios are measured and both primary products are determined to be equally probable. Quantum chemical and statistical reaction rate theory calculations illuminate pertinent information for interpreting the reaction data, including: reaction thermodynamics, a potential energy surface for the reaction, as well as rate constants and branching ratios for the observed products. In particular, the reaction products and potential energy surface stimulate questions regarding the strength and role of the nitrile functional group, which can be further explored with more reactions of this class.

Updatable timed automata (UTA) are extensions of classic timed automata that allow special updates to clock variables, like x:= x - 1, x := y + 2, etc., on transitions. Reachability for UTA is undecidable in general. Various subclasses with decidable reachability have been studied. A generic approach to UTA reachability consists of two phases: first, a static analysis of the automaton is performed to compute a set of clock constraints at each state; in the second phase, reachable sets of configurations, called zones, are enumerated. In this work, we improve the algorithm for the static analysis. Compared to the existing algorithm, our method computes smaller sets of constraints and guarantees termination for more UTA, making reachability faster and more effective. As the main application, we get an alternate proof of decidability and a more efficient algorithm for timed automata with bounded subtraction, a class of UTA widely used for modelling scheduling problems. We have implemented our procedure in the tool TChecker and conducted experiments that validate the benefits of our approach., Comment: Shorter version of this article is accepted at FSTTCS 2020