archive
Every paper Pith has read. Search by title, abstract, or pith.
213 papers in cs.FL · page 3
-
HistMSO logic expresses 39 of 42 consistency models
HistMSO: A Logic for Reasoning about Consistency Models with MONA
-
LLM agents collapse on expert network configs
NetAgentBench: A State-Centric Benchmark for Evaluating Agentic Network Configuration
-
Streaming algorithm learns PDFAs with PAC guarantees
PAC learning PDFA from data streams
-
Petri net model generates safe Rust code from API signatures
A Synthesis Method of Safe Rust Code Based on Pushdown Colored Petri Nets
-
Banach density hits 1/2 only for finite-rank language spaces in 1D
Banach density of generated languages: Dichotomies in topology and dimension
-
Supermartingales refute ε-differential privacy automatically
SuperDP: Differential Privacy Refutation via Supermartingales
-
Trajectories force CFL shuffles out of the class
Shuffles of Context-Free Languages along Regular Trajectories
-
Single RETURN statement simulates any 2-counter machine
Cypher is Turing-Complete: A Formal Proof via 2-Counter Machine Simulation
-
Product graph proves livelock freedom for all ring sizes
Practical Livelock Analysis in Parameterized Unidirectional Rings
-
Visibly recursive automata extend procedural automata
Visibly Recursive Automata
-
Finite smooth words are exactly the factors of infinite ones
The complexity of finite smooth words over binary alphabets
-
Parsing is always constrained by input while generation need not be
The Generation-Recognition Asymmetry: Six Dimensions of a Fundamental Divide in Formal Language Theory
-
HDAs drop artificial event order for interval ipomset semantics
Forgetting Event Order in Higher-Dimensional Automata
-
Memoryless strategies win reachability games with private randomness
Randomise Alone, Reach as a Team
-
IdMAT lets automata learning handle any target regular language
Automata Learning with an Incomplete but Inductive Teacher (Technical Report)
-
Translations prove automatic omega-words have decidable MSO theory
Expregular functions
-
C-RASP programs verified by translation to Lustre
Synthesis and Verification of Transformer Programs (Technical Report)
-
Monoid structure fixes space for out-of-order product
Out-of-Order Membership in Regular Languages
-
Minimal input sets explain why automata accept or reject
A Formal Framework for the Explanation of Finite Automata Decisions
-
DTMs solve SAT and Subset-Sum inside polynomial bounds
Implementation of Polynomial NP-Complete Algorithms Based on the NP Verifier Simulation Framework
-
Restriction on Büchi automata captures Eve-positional languages
Eve-positional languages: putting order into B\"uchi automata
-
Simulation relation solves control with required events
The Similarity Control Problem with Required Events
-
Posterior-deterministic POMDPs make reachability approximable
Computing the Reachability Value of Posterior-Deterministic POMDPs
-
Min-plus automata determinisation placed in fast-growing hierarchy
A Complexity Bound for Determinisation of Min-Plus Weighted Automata
-
Polynomial rules classify all commutative series products
Commutative algebras of series
-
Myhill-Nerode relation defined for one-clock timed automata
A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
-
LLM agents finish over 80% of Rust system proofs
VeruSAGE: A Study of Agent-Based Verification for Rust Systems
-
Timed reward machines add deadlines to RL rewards
About Time: Model-free Reinforcement Learning with Timed Reward Machines
-
Unambiguisability decidable for min-plus automata
Unambiguisability and Register Minimisation of Min-Plus Models
-
Bounded MSO query results on strings identified from two positions
A finer reparameterisation theorem for MSO and FO queries on strings
-
BEAVER gives sound safety bounds on LLMs with 1/10 compute
BEAVER: An Efficient Deterministic LLM Verifier
-
MSO recovers laminar trees from set systems
The role of counting quantifiers in laminar set systems
-
Positive examples alone identify relational pattern languages
Positive Characteristic Sets for Relational Pattern Languages
-
Transformers describe languages exponentially more compactly than LTL
Transformers are Inherently Succinct
-
Verified lexer makes printing the exact inverse of lexing
Formally Verified Linear-Time Invertible Lexing
-
Lazy automata order bounded by pattern fibers
On the order of lazy cellular automata
-
Past MITL translates linearly to deterministic timed automata
TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics
-
Automata decide balance of Fibonacci word rectangles
Balanced Fibonacci word rectangles, and beyond
-
Three reset classes suffice for Černý lifting
The hereditariness problem for the \v{C}ern\'y conjecture
-
Rational affine verifiers match real-valued power
Rational-Valued Affine Verifiers in Arthur--Merlin Proof Systems
-
Introspection with budget separates relativized P from NP
Psi-Turing Machines: Bounded Introspection for Complexity Barriers and Oracle Separations
-
Mobility classes follow Fibonacci fusion rules
Fusion Rules of Mobility
-
k-automatic sets split into two definability classes in Presburger arithmetic
A Dichotomy for $k$-automatic expansions of Presburger Arithmetic
-
Restricted trace-pushdown systems decide reachability theory
The theory of reachability in trace-pushdown systems
-
Byte sampler turns any BPE model into character-level generator
Sampling from Your Language Model One Byte at a Time
-
Smallest suffixient set size is O(r) in BWT runs
Smallest Suffixient Sets: Effectiveness, Resilience, and Calculation
-
Minimization during determinization shrinks NFA state spaces
Deconstructing Subset Construction -- Reducing While Determinizing
-
Deciding small DSA size is NP-complete
Deterministic Suffix-reading Automata
-
LLM framework produces LTL specs with zero safety violations
Automatic Generation of Safety-compliant Linear Temporal Logic via Large Language Model: A Self-supervised Framework
-
Conditions on substitutions make numeration systems positional
Positionality of Dumont--Thomas numeration systems for integers