Sven Dziadek

Ω-regular energy problems

By Sven Dziadek, Uli Fahrenberg, Philipp Schlehuber-Caissier

2024-12-01

In Formal Aspects of Computing

Abstract

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.

Continue reading

Energy problems in finite and timed automata with Büchi conditions

By Sven Dziadek, Uli Fahrenberg, Philipp Schlehuber-Caissier

2022-12-08

In International symposium on formal methods (FM)

Abstract

We show how to efficiently solve energy Büchi problems in finite weighted automata and in one-clock weighted timed automata. Solving the former problem is our main contribution and is handled by a modified version of Bellman-Ford 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 tools TChecker and Spot.

Continue reading

Greibach normal form for $\omega$-algebraic systems and weighted simple $\omega$-pushdown automata

By Manfred Droste, Sven Dziadek, Werner Kuich

2022-06-30

In Information and Computation

Abstract

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 (as introduced by Cohen and Gold in 1977) and an extension of weighted context-free languages of finite words (that were already investigated by Chomsky and Schützenberger in 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.

Continue reading

Search

Tags