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, 9 Dec 22

[1]  arXiv:2212.03992 [pdf, ps, other]
Title: State Grammars with Stores
Comments: 21 pages
Journal-ref: Theoretical Computer Science 798, 23-39 (2019)
Subjects: Formal Languages and Automata Theory (cs.FL)

State grammars are context-free grammars where the productions have states associated with them, and a production can only be applied to a nonterminal if the current state matches the state in the production. Once states are added to grammars, it is natural to add various stores, similar to machine models. With such extensions, productions can only be applied if both the state and the value read from each store matches between the current sentential form and the production. Here, generative capacity results are presented for different derivation modes, with and without additional stores. In particular, with the standard derivation relation, it is shown that adding reversal-bounded counters does not increase the capacity, and states are enough. Also, state grammars with reversal-bounded counters that operate using leftmost derivations are shown to coincide with languages accepted by one-way machines with a pushdown and reversal-bounded counters, and these are surprisingly shown to be strictly weaker than state grammars with the standard derivation relation (and no counters). The complexity of the emptiness problem involving state grammars with reversal-bounded counters is also studied.

[2]  arXiv:2212.04218 [pdf, other]
Title: Structural Reductions and Stutter Sensitive Properties
Comments: 23 pages, extended version of FORTE'22 paper "LTL under reductions with weaker conditions than stutter invariance" arXiv:2111.03342
Subjects: Formal Languages and Automata Theory (cs.FL)

Verification of properties expressed as $\omega$-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a \emph{reduction} of a system. A reduction has the property that it can only shorten runs. Lipton's transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. We also present an approach that can reason using a partition of a property language into its stutter insensitive, shortening insensitive, lengthening insensitive and length sensitive parts to still use structural reductions even when working with arbitrary properties. An implementation and experimental evidence is provided showing most non-random properties sensitive to stutter are actually shortening or lengthening insensitive.

Replacements for Fri, 9 Dec 22

[3]  arXiv:2205.12114 (replaced) [pdf, other]
Title: Register Set Automata (Technical Report)
Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)
[4]  arXiv:2206.15319 (replaced) [pdf, other]
Title: On extended boundary sequences of morphic and Sturmian words
Comments: 32 pages, 8 figures. Short version: M. Rigo, M. Stipulanti, M. A. Whiteland, On extended boundary sequences of morphic and Sturmian words, MFCS 2022, Leibniz Int. Proc. Inform. 241 (2022), Paper 79
Subjects: Combinatorics (math.CO); Formal Languages and Automata Theory (cs.FL)
[5]  arXiv:2212.02754 (replaced) [pdf, ps, other]
Title: Automatically Transform Rust Source to Petri Nets for Checking Deadlocks
Subjects: Programming Languages (cs.PL); Formal Languages and Automata Theory (cs.FL); Software Engineering (cs.SE)
[ 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, 2212, contact, help  (Access key information)