An official website of the United States government
A Simple Temporal Network with Uncertainty (STNU) includes real-valued variables, called time-points; binary difference constraints on those time-points; and contingent links that represent actions with uncertain durations. STNUs have been used for robot control, web-service composition, and business processes. The most important property of an STNU is called dynamic controllability (DC); and algorithms for checking this property are called DC-checking algorithms. The DC-checking algorithm for STNUs with the best worst-case time-complexity is the RUL¯ algorithm due to Cairo, Hunsberger and Rizzi. Its complexity is O(mn + k²n + kn log n), where n is the number of time-points, m is the number of constraints, and k is the number of contingent links. It is expected that this worst-case complexity cannot be improved upon. However, this paper provides a new algorithm, called RUL2021, that improves its performance in practice by an order of magnitude, as demonstrated by a thorough empirical evaluation.
more »
« less
Faster Dynamic-Consistency Checking for Conditional Simple Temporal Networks
A Conditional Simple Temporal Network (CSTN) is a structure for representing and reasoning about time in domains where temporal constraints may be conditioned on outcomes of observations made in real time. A CSTN is dynamically consistent (DC) if there is a strategy for executing its timepoints such that all relevant constraints will necessarily be satisfied no matter which outcomes happen to be observed. The literature on CSTNs contains only one sound-and-complete DC-checking algorithm that has been implemented and empirically evaluated. It is a graph-based algorithm that propagates labeled constraints/edges. A second algorithm has been proposed, but not evaluated. It aims to speed up DC checking by more efficiently dealing with so-called negative q-loops. This paper presents a new two-phase approach to DC-checking for CSTNs. The first phase focuses on identifying negative q-loops and labeling key time-points within them. The second phase focuses on computing (labeled) distances from each time-point to a single sink node. The new algorithm, which is also sound and complete for DC-checking, is then empirically evaluated against both pre-existing algorithms and shown to be much faster across not only previously published benchmark problems, but also a new set of benchmark problems. The results show that, on DC instances, the new algorithm tends to be an order of magnitude faster than both existing algorithms. On all other benchmark cases, the new algorithm performs better than or equivalently to the existing algorithms.
more »
« less
- Award ID(s):
- 1909739
- PAR ID:
- 10148943
- Date Published:
- Journal Name:
- 30th International Joint Conference on Applied Planning and Scheduling (ICAPS-2020)
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Checking query equivalence is of great significance in database systems. Prior work in automated query equivalence checking sets the first steps in formally modeling and reasoning about query optimization rules, but only supports a limited number of query features. In this paper, we present Qed, a new framework for query equivalence checking based on bag semantics. Qed uses a new formalism called Q-expressions that models queries using different normal forms for efficient equivalence checking, and models features such as integrity constraints and NULLs in a principled way unlike prior work. Our formalism also allows us to define a new query fragment that encompasses many real-world queries with a complete equivalence checking algorithm, assuming a complete first-order theory solver. Empirically, Qed can verify 299 out of 444 query pairs extracted from the Calcite framework and 979 out of 1287 query pairs extracted from CockroachDB, which is more than 2× the number of cases proven by prior state-of-the-art solver.more » « less
-
The COVID-19 pandemic has intensified the need for home-based cardiac health monitoring systems. Despite advancements in electrocardiograph (ECG) and phonocardiogram (PCG) wearable sensors, accurate heart sound segmentation algorithms remain understudied. Existing deep learning models, such as convolutional neural networks (CNN) and recurrent neural networks (RNN), struggle to segment noisy signals using only PCG data. We propose a two-step heart sound segmentation algorithm that analyzes synchronized ECG and PCG signals. The first step involves heartbeat detection using a CNN-LSTM-based model on ECG data, and the second step focuses on beat-wise heart sound segmentation with a 1D U-Net that incorporates multi-modal inputs. Our method leverages temporal correlation between ECG and PCG signals to enhance segmentation performance. To tackle the label-hungry issue in AI-supported biomedical studies, we introduce a segment-wise contrastive learning technique for signal segmentation, overcoming the limitations of traditional contrastive learning methods designed for classification tasks. We evaluated our two-step algorithm using the PhysioNet 2016 dataset and a private dataset from Bayland Scientific, obtaining a 96.43 F1 score on the former. Notably, our segment-wise contrastive learning technique demonstrated effective performance with limited labeled data. When trained on just 1% of labeled PhysioNet data, the model pre-trained on the full unlabeled dataset only dropped 2.88 in the F1 score, outperforming the SimCLR method. Overall, our proposed algorithm and learning technique present promise for improving heart sound segmentation and reducing the need for labeled data.more » « less
-
In real-world phenomena which involve mutual influence or causal effects between interconnected units, equilibrium states are typically represented with cycles in graphical models. An expressive class of graphical models, relational causal models, can represent and reason about complex dynamic systems exhibiting such cycles or feedback loops. Existing cyclic causal discovery algorithms for learning causal models from observational data assume that the data instances are independent and identically distributed which makes them unsuitable for relational causal models. At the same time, causal discovery algorithms for relational causal models assume acyclicity. In this work, we examine the necessary and sufficient conditions under which a constraint-based relational causal discovery algorithm is sound and complete for cyclic relational causal models. We introduce relational acyclification, an operation specifically designed for relational models that enables reasoning about the identifiability of cyclic relational causal models. We show that under the assumptions of relational acyclification and sigma-faithfulness, the relational causal discovery algorithm RCD is sound and complete for cyclic relational models. We present experimental results to support our claim.more » « less
-
Dependent security labels (security labels that depend on program states) in various forms have been introduced to express rich information flow policies. They are shown to be essential in the verification of real-world software and hardware systems such as conference management systems, Android Apps, a MIPS processor and a TrustZone-like architecture. However, most work assumes that all (complex) labels are provided manually, which can both be error-prone and time-consuming. In this paper, we tackle the problem of automatic label inference for static information flow analyses with dependent security labels. In particular, we propose the first general framework to facilitate the design and validation (in terms of soundness and/or completeness) of inference algorithms. The framework models label inference as constraint solving and offers guidelines for sound and/or complete constraint solving. Under the framework, we propose novel constraint solving algorithms that are both sound and complete. Evaluation result on sets of constraints generated from secure and insecure variants of a MIPS processor suggests that the novel algorithms improve the performance of an existing algorithm by orders of magnitude and offers better scalability.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
