2026 Iowa State REU Project
2026 Iowa State REU Project
Project mentor: Kristin Yvonne Rozier
A temporal logic is a formal system of syntax rules and semantics that allows us to represent and reason about propositions qualified in terms of time. One of the most widely used and well-known temporal logics is Linear-time Temporal Logic (LTL), for which time is conceived as a linear, discrete succession of time instances. LTL extends the classical propositional language by adding temporal operators G, X, and U, with intended meaning as follows:
- Gp: "It will always be the case that p;"
- Xp: "Next time will be the case that p;"
- pUq: "p will be the case until a time when q is the case."
This logic expresses properties that describe the specifications of a system, that is, the behaviors the system should exhibit. For example, the specification “Every request is followed by a grant” can be formalized in LTL as G(request→¬G¬grant). LTL formulas are interpreted over the set of natural numbers with its usual order, where each number represents a time instance, with zero representing the current one, plus an interpretation function (aka a trace) V that assigns to each proposition p a set of time instances V(p)⊆AP on which it holds.
On the other hand, Mission-Time Temporal Logic (MLTL) follows the syntax of LTL while adding finite, discrete, closed-interval bounds on the temporal operators. For example, the formula "G[2,5]p" captures that "p must hold between 2 and 5 time steps from now." MLTL has been used as the specification logic for NASA’s Robonaut2 verification project, as well as for both design-time and runtime verification of the NASA Lunar Gateway Vehicle System Manager. MLTL formulas are interpreted over finite traces, that is, over an initial segment of the set of natural numbers (instead of infinite traces), which may or may not be long enough to cover all the intervals in the formula.
A natural question to ask about any logical formula is to determine whether or not it is satisfiable (i.e., that is true in some interpretation), as well as determining if a given formula is a tautology (i.e., is it always true regardless of its interpretation). In the case of LTL, multiple solutions to these questions have been developed using Büchi Automata, which are essentially finite directed graphs with labeled vertices and edges. However, for MLTL, there is no known good solution, other than encoding each formula into another logic, such as LTL, at an exponential cost, then using algorithms developed for that logic. This project will investigate algorithmic methods to produce automata-based encodings for MLTL formulas that avoid encoding them into LTL first and evaluating their complexity and performance against the best algorithms known for LTL.
Prerequisites: Basic programming skills, some background in discrete mathematics (introductory undergraduate level), and mathematical maturity. Familiarity with concepts from mathematical logic (satisfiability, soundness, completeness, compactness, etc.) is desirable.
Project mentor: Eric Weber and Enrique Alvarado
In this REU, we will mainly be interested in investigating the asymptotic properties of the ternary hypercube, defined as the set of all vectors in n dimensional Euclidean space whose entries are either -1, 0, or 1. For example, the ternary hypercube in 2 dimensions consists of the nine integer coordinate vectors contained within the square of base length 2 centered at the origin, and whose sides are perpendicular to the coordinate axes. We are particularly interested in sparse representations of the vectors in high dimensional ternary hypercubes.
Technically speaking, a sparse representation of a (non-zero) vector in n dimensions (or in any vector space, really) only makes sense whenever you are also given a dictionary D, a set of n dimensional vectors that spans n dimensional Euclidean space. Recalling our definitions from Linear Algebra, D is said to span our vector space if every vector in the space can be written as a linear combination of the vectors in D. When the dictionary D contains more vectors than the dimension of the vector space, there may be multiple ways that a linear combination of the vectors in D can give us a vector v.
For example, if the dictionary D consists of the 4 vectors [1, 0], [0, 1], [1, 1], and [1, -1], we can represent the vector v = [3, 3] in two different ways: either as v = 3[1, 0] + 3[0, 1] + 0[1, 1] + 0[1, -1], or as v = 0[1, 0] + 0[0, 1] + 3[1, 1] + 0[1, -1]. The second representation of [3, 3] is said to be sparser than the first representation because there is only one non-zero coefficient used within the sum, whereas the first one uses two non-zero coefficients. Given a dictionary, the sparsity of a vector v is defined as the smallest number of non-zero coefficients needed to represent v. In the example above, the sparsity of [3, 3] with respect to the dictionary D was 1. The way we constructed the dictionary was by taking the union of the standard Euclidean basis with the Hadamard basis.
In this project, our goal will be to conjecture and prove statements related to the sparsity of vectors in the n dimensional ternary hypercube in the case that n is a large power of 2, and when our dictionary is equal to the union of the n dimensional Euclidean basis, and the n dimensional Hadamard basis. The motivation of this problem comes from the area of Topological Data Analysis, an active area of applied mathematics, widely and successfully used to study the “shape” of data found within scientific domains such as medicine, materials science, computational chemistry, neuroscience, and more.
Prerequisites: The prerequisites for this project is mainly some standard first-course knowledge of Linear Algebra. It will also be helpful to have familiarity with coding in Python, however, enthusiasm to learn how to code in Python is sufficient.