We gratefully acknowledge support from
the Simons Foundation and member institutions.

Formal Languages and Automata Theory

New submissions

[ total of 5 entries: 1-5 ]
[ showing up to 2000 entries per page: fewer | more ]

New submissions for Fri, 3 Feb 23

[1]  arXiv:2302.01009 [pdf, ps, other]
Title: String Compression in FA-Presentable Structures
Comments: 14 pages; accepted version
Journal-ref: Theoretical Computer Science, 947 (2023) 113705
Subjects: Formal Languages and Automata Theory (cs.FL)

We construct a FA-presentation $\psi: L \rightarrow \mathbb{N}$ of the structure $(\mathbb{N};\mathrm{S})$ for which a numerical characteristic $r(n)$ defined as the maximum number $\psi(w)$ for all strings $w \in L$ of length less than or equal to $n$ grows faster than any tower of exponents of a fixed height. This result leads us to a more general notion of a compressibility rate defined for FA-presentations of any FA-presentable structure. We show the existence of FA-presentations for the configuration space of a Turing machine and Cayley graphs of some groups for which it grows faster than any tower of exponents of a fixed height. For FA-presentations of the Presburger arithmetic $(\mathbb{N};+)$ we show that it is bounded from above by a linear function.

Cross-lists for Fri, 3 Feb 23

[2]  arXiv:2302.00724 (cross-list from cs.DS) [pdf, other]
Title: Order-Preserving Squares in Strings
Subjects: Data Structures and Algorithms (cs.DS); Formal Languages and Automata Theory (cs.FL)

An order-preserving square in a string is a fragment of the form $uv$ where $u\neq v$ and $u$ is order-isomorphic to $v$. We show that a string $w$ of length $n$ over an alphabet of size $\sigma$ contains $\mathcal{O}(\sigma n)$ order-preserving squares that are distinct as words. This improves the upper bound of $\mathcal{O}(\sigma^{2}n)$ by Kociumaka, Radoszewski, Rytter, and Wale\'n [TCS 2016]. Further, for every $\sigma$ and $n$ we exhibit a string with $\Omega(\sigma n)$ order-preserving squares that are distinct as words, thus establishing that our upper bound is asymptotically tight. Finally, we design an $\mathcal{O}(\sigma n)$ time algorithm that outputs all order-preserving squares that occur in a given string and are distinct as words. By our lower bound, this is optimal in the worst case.

[3]  arXiv:2302.00737 (cross-list from cs.DC) [pdf, other]
Title: A Universal Technique for Machine-Certified Proofs of Linearizable Algorithms
Comments: 31 pages
Subjects: Distributed, Parallel, and Cluster Computing (cs.DC); Data Structures and Algorithms (cs.DS); Formal Languages and Automata Theory (cs.FL)

Linearizability has been the long standing gold standard for consistency in concurrent data structures. However, proofs of linearizability can be long and intricate, hard to produce, and extremely time consuming even to verify. In this work, we address this issue by introducing simple $universal$, $sound$, and $complete$ proof methods for producing machine-verifiable proofs of linearizability and its close cousin, strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is linearizable (resp. strong linearizable); and completeness means that any linearizable (resp. strong linearizable) implementation can be proved so using our method. We demonstrate the simplicity and power of our method by producing proofs of linearizability for the Herlihy-Wing queue and Jayanti's single-scanner snapshot, as well as a proof of strong linearizability of the Jayanti-Tarjan union-find object. All three of these proofs are machine-verified by TLAPS (the Temporal Logic of Actions Proof System).

Replacements for Fri, 3 Feb 23

[4]  arXiv:2104.02876 (replaced) [pdf, other]
Title: Finite Automata Encoding Functions: A Representation Using B-splines
Comments: 24 pages; in the third version the introduction and the abstract has been rewritten; additional minor changes and improvements have been made
Subjects: Computational Geometry (cs.CG); Formal Languages and Automata Theory (cs.FL)
[5]  arXiv:2208.08609 (replaced) [pdf, other]
Title: A Scalable, Interpretable, Verifiable & Differentiable Logic Gate Convolutional Neural Network Architecture From Truth Tables
Subjects: Artificial Intelligence (cs.AI); Formal Languages and Automata Theory (cs.FL); Machine Learning (cs.LG); Symbolic Computation (cs.SC)
[ total of 5 entries: 1-5 ]
[ showing up to 2000 entries per page: fewer | more ]

Disable MathJax (What is MathJax?)

Links to: arXiv, form interface, find, cs, recent, 2302, contact, help  (Access key information)