skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Computing under-approximations of multivalued decision diagrams
Efficient manipulation of binary or multi-valueddecision diagrams (BDDs or MDDs) is critical in symbolic verification tools. Despite the applicability of MDDs to real-world tasks such as discovering the reachable states of a model, their large demands on hardware resources, especially memory, limit algorithmic scalability. In this paper, we focus on memory-constrained algorithms that employ a novel O(m log n)-time under-approximation technique for MDDs, where m and n are the number of MDD edges and nodes, respectively. The effectiveness of our approach is demonstrated experimentally by a reduction in peak memory usage for the symbolic reachability computation of a set of Petri nets.  more » « less
Award ID(s):
2212142
PAR ID:
10465240
Author(s) / Creator(s):
;
Editor(s):
Gomes, L.; Lorenz, R.
Date Published:
Journal Name:
Application and Theory of Petri Nets and Concurrency
Volume:
LNCS 13929
Page Range / eLocation ID:
243–263
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Abstract We demonstrate that the key components of cognitive architectures (declarative and procedural memory) and their key capabilities (learning, memory retrieval, probability judgment, and utility estimation) can be implemented as algebraic operations on vectors and tensors in a high‐dimensional space using a distributional semantics model. High‐dimensional vector spaces underlie the success of modern machine learning techniques based on deep learning. However, while neural networks have an impressive ability to process data to find patterns, they do not typically model high‐level cognition, and it is often unclear how they work. Symbolic cognitive architectures can capture the complexities of high‐level cognition and provide human‐readable, explainable models, but scale poorly to naturalistic, non‐symbolic, or big data. Vector‐symbolic architectures, where symbols are represented as vectors, bridge the gap between the two approaches. We posit that cognitive architectures, if implemented in a vector‐space model, represent a useful, explanatory model of the internal representations of otherwise opaque neural architectures. Our proposed model, Holographic Declarative Memory (HDM), is a vector‐space model based on distributional semantics. HDM accounts for primacy and recency effects in free recall, the fan effect in recognition, probability judgments, and human performance on an iterated decision task. HDM provides a flexible, scalable alternative to symbolic cognitive architectures at a level of description that bridges symbolic, quantum, and neural models of cognition. 
    more » « less
  2. In several emerging technologies for computer memory (main memory), the cost of reading is significantly cheaper than the cost of writing. Such asymmetry in memory costs poses a fundamentally different model from the RAM for algorithm design. In this paper we study lower and upper bounds for various problems under such asymmetric read and write costs. We consider both the case in which all but O(1) memory has asymmetric cost, and the case of a small cache of symmetric memory. We model both cases using the (M,w)-ARAM, in which there is a small (symmetric) memory of size M and a large unbounded (asymmetric) memory, both random access, and where reading from the large memory has unit cost, but writing has cost w >> 1. For FFT and sorting networks we show a lower bound cost of Omega(w*n*log_{w*M}(n)), which indicates that it is not possible to achieve asymptotic improvements with cheaper reads when w is bounded by a polynomial in M. Moreover, there is an asymptotic gap (of min(w,log(n)/log(w*M)) between the cost of sorting networks and comparison sorting in the model. This contrasts with the RAM, and most other models, in which the asymptotic costs are the same. We also show a lower bound for computations on an n*n diamond DAG of Omega(w*n^2/M) cost, which indicates no asymptotic improvement is achievable with fast reads. However, we show that for the minimum edit distance problem (and related problems), which would seem to be a diamond DAG, we can beat this lower bound with an algorithm with only O(w*n^2/(M*min(w^{1/3},M^{1/2}))) cost. To achieve this we make use of a "path sketch" technique that is forbidden in a strict DAG computation. Finally, we show several interesting upper bounds for shortest path problems, minimum spanning trees, and other problems. A common theme in many of the upper bounds is that they require redundant computation and a tradeoff between reads and writes. 
    more » « less
  3. Children bring intuitive arithmetic knowledge to the classroom before formal instruction in mathematics begins. For example, children can use their number sense to add, subtract, compare ratios, and even perform scaling operations that increase or decrease a set of dots by a factor of 2 or 4. However, it is currently unknown whether children can engage in a true division operation before formal mathematical instruction. Here we examined the ability of 6- to 9-year-old children and college students to perform symbolic and non-symbolic approximate division. Subjects were presented with non-symbolic (dot array) or symbolic (Arabic numeral) dividends ranging from 32 to 185, and non-symbolic divisors ranging from 2 to 8. Subjects compared their imagined quotient to a visible target quantity. Both children (Experiment 1 N = 89, Experiment 2 N = 42) and adults (Experiment 3 N = 87) were successful at the approximate division tasks in both dots and numeral formats. This was true even among the subset of children that could not recognize the division symbol or solve simple division equations, suggesting intuitive division ability precedes formal division instruction. For both children and adults, the ability to divide non-symbolically mediated the relation between Approximate Number System (ANS) acuity and symbolic math performance, suggesting that the ability to calculate non-symbolically may be a mechanism of the relation between ANS acuity and symbolic math. Our findings highlight the intuitive arithmetic abilities children possess before formal math instruction. 
    more » « less
  4. Analyzing multithreaded programs is notoriously hard due to the exponential number of thread interleavings. Although race detectors can help developers find and fix such bugs before the code is deployed, multithreaded code may still be buggy due to memory errors and assertion violations that are not due to race conditions. This paper presents a property directed symbolic execution of multithreaded code. Our approach, named SIFT, differs from previous work on detecting errors in multithreaded code by being property directed and by handling both memory safety and assertion checking that can be further customized by the user. SIFT can detect bugs that may or may not be due to data races, and works in an iterative way. In each step, it explores the state space using selective scheduling based on a set of interleaving points that have been inferred in the previous step. We have developed three partitioning strategies for improved effectiveness and performance. We have implemented SIFT on top of the KLEE symbolic execution engine and applied it to various real-world and academic benchmarks. SIFT could detect more vulnerabilities than a state-of-the-art memory vulnerability detector. 
    more » « less
  5. This study characterises a previously unstudied facet of a major causal model of math anxiety. The model posits that impaired “basic number abilities” can lead to math anxiety, but what constitutes a basic number ability remains underdefined. Previous work has raised the idea that our perceptual ability to represent quantities approximately without using symbols constitutes one of the basic number abilities. Indeed, several recent studies tested how participants with math anxiety estimate and compare non-symbolic quantities. However, little is known about how participants with math anxiety perform arithmetic operations (addition and subtraction) on non-symbolic quantities. This is an important question because poor arithmetic performance on symbolic numbers is one of the primary signatures of high math anxiety. To test the question, we recruited 92 participants and asked them to complete a math anxiety survey, two measures of working memory, a timed symbolic arithmetic test, and a non-symbolic “approximate arithmetic” task. We hypothesised that if impaired ability to perform operations was a potential causal factor to math anxiety, we should see relationships between math anxiety and both symbolic and approximate arithmetic. However, if math anxiety relates to precise or symbolic representation, only a relationship between math anxiety and symbolic arithmetic should appear. Our results show no relationship between math anxiety and the ability to perform operations with approximate quantities, suggesting that difficulties performing perceptually based arithmetic operations do not constitute a basic number ability linked to math anxiety. 
    more » « less