For a fixed regular language L, the enumeration of L-infixes is the following task: we are given an input word w = a₁ ⋯ a_n and we must enumerate the infixes of w that belong to L, i.e., the pairs i ≤ j such that a_i ⋯ a_j ∈ L. We are interested in dynamic enumeration of L-infixes, where we must additionally support letter substitution updates on w (e.g., "replace the i-th letter of w by a letter a"). Each update changes the set of infixes to enumerate, and resets the enumeration state. We study for which regular languages L we can perform dynamic enumeration of L-infixes in constant delay (i.e., the next infix is always produced in constant time) and constant additional memory throughout the enumeration, while supporting each update in constant time. We show that, for languages L with a neutral letter, if the language L belongs to the class ZG and is extensible (i.e., if u ∈ L and u is a factor of v then v ∈ L), then dynamic enumeration of L-infixes can be achieved with a simple algorithm that ensures constant-time updates and constant delay, but not constant additional memory. Our main contribution is then to show an algorithm that additionally uses only constant additional memory, and applies to a more general class of semi-extensible ZG languages for which we give several equivalent characterizations. We further discuss whether our results can be generalized to larger language classes and show some (conditional) lower bounds.

We show how to efficiently solve problems involving a quantitative measure, here called energy , as well as a qualitative acceptance condition, expressed as a Büchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. Solving the former problem and extracting the corresponding witness is our main contribution and is handled by a modified version of the Bellman-Ford algorithm interleaved with Couvreur’s algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source platforms TChecker and Spot.

In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of $\omega$-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Sch\"utzenberger 1963). As in the theory of formal grammars, these weighted context-free languages, or $\omega$-algebraic series, can be represented as solutions of mixed $\omega$-algebraic systems of equations and by weighted $\omega$-pushdown automata. In our first main result, we show that (mixed) $\omega$-algebraic systems can be transformed into Greibach normal form. We use the Greibach normal form in our second main result to prove that simple $\omega$-reset pushdown automata recognize all $\omega$-algebraic series. Simple $\omega$-reset automata do not use $\epsilon$-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted context-free languages.

Recently, weighted ω-pushdown automata have been introduced by Droste, Ésik, Kuich. This new type of automaton has access to a stack and models quantitative aspects of infinite words. Here, we consider a simple version of those automata. The simple ω-pushdown automata do not use ε-transitions and have a very restricted stack access. In previous work, we could show this automaton model to be expressively equivalent to context-free ω-languages in the unweighted case. Furthermore, semiring-weighted simple ω-pushdown automata recognize all ω-algebraic series. Here, we consider ω-valuation monoids as weight structures. As a first result, we prove that for this weight structure and for simple ω-pushdown automata, Büchi-acceptance and Muller-acceptance are expressively equivalent. In our second result, we derive a Nivat theorem for these automata stating that the behaviors of weighted ω-pushdown automata are precisely the projections of very simple ω-series restricted to ω-context-free languages. The third result is a weighted logic with the same expressive power as the new automaton model. To prove the equivalence, we use a similar result for weighted nested ω-word automata and apply our present result of expressive equivalence of Muller and Büchi acceptance.

In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Here, we investigate weighted context-free languages of infinite words, a generalization of omega-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted languages, or omega-algebraic series, can be represented as solutions of mixed omega-algebraic systems of equations and by weighted omega-pushdown automata. In our first main result, we show that mixed omega-algebraic systems can be transformed into Greibach normal form. Our second main result proves that simple omega-reset pushdown automata recognize all omega-algebraic series that are a solution of an omega-algebraic system in Greibach normal form. Simple reset automata do not use epsilon-transitions and can change the stack only by at most one symbol. These results generalize fundamental properties of context-free languages to weighted languages.

This paper explores the problem of how to improve the average-case performance of real-time locking protocols, preferably without significantly deteriorating worst-case performance. Motivated by the futex implementation in Linux, where uncontended lock operations under the Priority Inheritance Protocol (PIP) do not incur mode-switching overheads, we extend this concept to more sophisticated protocols, namely the PCP, the MPCP and the FMLP+. We identify the challenges involved in implementing futexes for these protocols and present the design and evaluation of their implementations in LITMUSRT, a real-time extension of the Linux kernel. Our evaluation shows substantial improvements in the uncontended case (e.g., A futex implementation of the PCP lowers lock acquisition and release overheads by up to 75% and 92%, respectively), at the expense of some increases in worst-case overhead on par with Linux's existing futex implementation.