More Like this

1. Information Acquisition Under Resource Limitations in a Noisy Environment

   https://doi.org/10.1145/3510024  

   Soloviev, Matvey; Halpern, Joseph Y. (June 2022, Journal of the ACM)

   We introduce a theoretical model of information acquisition under resource limitations in a noisy environment. An agent must guess the truth value of a given Boolean formula \( \varphi \) after performing a bounded number of noisy tests of the truth values of variables in the formula. We observe that, in general, the problem of finding an optimal testing strategy for \( \varphi \) is hard, but we suggest a useful heuristic. The techniques we use also give insight into two apparently unrelated but well-studied problems: (1) rational inattention , that is, when it is rational to ignore pertinent information (the optimal strategy may involve hardly ever testing variables that are clearly relevant to \( \varphi \) ), and (2) what makes a formula hard to learn/remember. 

   more » « less
2. Evrostos: the rLTL verifier

   https://doi.org/10.1145/3302504.3311812  

   Anevlavis, Tzanis; Neider, Daniel; Phillipe, Matthew; Tabuada, Paulo (April 2019, HSCC '19: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control)

   null (Ed.)

   Robust Linear Temporal Logic (rLTL) was crafted to incorporate the notion of robustness into Linear-time Temporal Logic (LTL) specifications. Technically, robustness was formalized in the logic rLTL via 5 different truth values and it led to an increase in the time complexity of the associated model checking problem. In general, model checking an rLTL formula relies on constructing a generalized Büchi automaton of size 5^|φ| where |φ| denotes the length of an rLTL formula φ. It was recently shown that the size of this automaton can be reduced to 3^|φ| (and even smaller) when the formulas to be model checked come from a fragment of rLTL. In this paper, we introduce Evrostos, the first tool for model checking formulas in this fragment. We also present several empirical studies, based on models and LTL formulas reported in the literature, confirming that rLTL model checking for the aforementioned fragment incurs in a time overhead that makes the verification of rLTL practical. 

   more » « less
3. Adaptive Group Testing with Mismatched Models

   https://doi.org/10.1109/ICASSP43922.2022.9747665  

   Fan, Mingzhou; Yoon, Byung-Jun; Alexander, Francis J.; Dougherty, Edward R.; Qian, Xiaoning (May 2022, ICASSP 2022 - 2022 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP))

   Accurate detection of infected individuals is one of the critical steps in stopping any pandemic. When the underlying infection rate of the disease is low, testing people in groups, instead of testing each individual in the population, can be more efficient. In this work, we consider noisy adaptive group testing design with specific test sensitivity and specificity that select the optimal group given previous test results based on pre-selected utility function. As in prior studies on group testing, we model this problem as a sequential Bayesian Optimal Experimental Design (BOED) to adaptively design the groups for each test. We analyze the required number of group tests when using the updated posterior on the infection status and the corresponding Mutual Information (MI) as our utility function for selecting new groups. More importantly, we study how the potential bias on the ground-truth noise of group tests may affect the group testing sample complexity. 

   more » « less
4. Decentralized Asynchronous Crash-resilient Runtime Verification

   https://doi.org/10.1145/3550483  

   Bonakdarpour, Borzoo; Fraigniaud, Pierre; Rajsbaum, Sergio; Rosenblueth, David; Travers, Corentin (October 2022, Journal of the ACM)

   Runtime verificationis a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronousdistributedmonitors observing the system, only if each monitor can emit verdicts taken from alarge enoughfinite set. We revisit this impossibility result in the concrete context of linear-time logic (ltl) semantics for runtime verification, that is, when the correctness of the system is specified by anltlformula on its execution traces. First, we show that monitors synthesized based on the 4-valued semantics ofltl(rv-ltl) may result in inconsistent distributed monitoring, even for some simpleltlformulas. More generally, given anyltlformula φ, we relate the number of different verdicts required by the monitors for consistently monitoring φ, with a specific structural characteristic of φ called itsalternation number. Specifically, we show that, for everyk ≥ 0, there is anltlformula φ with alternation number kthat cannot be verified at runtime by distributed monitors emitting verdicts from a set of cardinality smaller thank+ 1. On the positive side, we define a family of logics, calleddistributedltl(abbreviated asdltl), parameterized byk≥ 0, which refinesrv-ltlby incorporating2k+ 4 truth values. Our main contribution is to show that, for everyk≥ 0, everyltlformula φ with alternation number kcan be consistently monitored by distributed monitors, each running an automaton based on a (2 ⌈k/2 ⌉ +4)-valued logic taken from thedltlfamily. 

   more » « less
5. Maximizing Truth Learning in a Social Network is NP-Hard

   Uradnik, Filip; Wang, Amanda; Gao, Jie (May 2025, Proceedings of the 24th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS))

   Sequential learning models situations where agents predict a ground truth in sequence, by using their private, noisy measurements, and the predictions of agents who came earlier in the sequence. We study sequential learning in a social network, where agents only see the actions of the previous agents in their own neighborhood. The fraction of agents who predict the ground truth correctly depends heavily on both the network topology and the ordering in which the predictions are made. A natural question is to find an ordering, with a given network, to maximize the (expected) number of agents who predict the ground truth correctly. In this paper, we show that it is in fact NP-hard to answer this question for a general network, with both the Bayesian learning model and a simple majority rule model. Finally, we show that even approximating the answer is hard. 

   more » « less