A Translation of Weighted LTL Formulas to Weighted Buchi Automata over omega-valuation Monoids

Eleni Mandrali;

doi:10.7561/sacs.2021.2.223

A Translation of Weighted LTL Formulas to Weighted Buchi Automata over omega-valuation Monoids

Scientific Annals of Computer Science ◽

10.7561/sacs.2021.2.223 ◽

2021 ◽

Vol 31 (2) ◽

pp. 223-292

Author(s):

Eleni Mandrali ◽

Keyword(s):

Büchi Automata ◽

Büchi Automaton ◽

Buchi Automata

In this paper we introduce a weighted LTL over product omega-valuation monoids that satisfy specific properties. We also introduce weighted generalized Buchi automata with epsilon-transitions, as well as weighted Buchi automata with epsilon-transitions over product omega-valuation monoids and prove that these two models are expressively equivalent and also equivalent to weighted Buchi automata already introduced in the literature. We prove that every formula of a syntactic fragment of our logic can be effectively translated to a weighted generalized Buchi automaton with epsilon-transitions. For generalized product omega-valuation monoids that satisfy specific properties we define a weighted LTL, weighted generalized Buchi automata with epsilon-transitions, and weighted Buchi automata with epsilon-transitions, and we prove the aforementioned results for generalized product omega-valuation monoids as well. The translation of weighted LTL formulas to weighted generalized Buchi automata with epsilon-transitions is now obtained for a restricted syntactical fragment of the logic.

Download Full-text

FACTORIZATIONS AND UNIVERSAL AUTOMATON OF OMEGA LANGUAGES

International Journal of Foundations of Computer Science ◽

10.1142/s0129054114400279 ◽

2014 ◽

Vol 25 (08) ◽

pp. 1111-1125

Author(s):

VINCENT CARNINO ◽

SYLVAIN LOMBARDY

Keyword(s):

Normal Form ◽

Büchi Automata ◽

Morphic Image ◽

Rational Language ◽

Büchi Automaton ◽

Buchi Automata

We extend the concept of factorization on finite words to ω-rational languages and show how to compute them. We define a normal form for Büchi automata and introduce a universal automaton for Büchi automata in normal form. We prove that, for every ω-rational language, this Büchi automaton, based on factorization, is canonical and that it is the smallest automaton that contains the morphic image of every equivalent Büchi automaton in normal form.

Download Full-text

THE EFFECT OF THE NUMBER OF SUCCESSFUL PATHS IN A BÜCHI TREE AUTOMATON

International Journal of Algebra and Computation ◽

10.1142/s0218196793000172 ◽

1993 ◽

Vol 03 (02) ◽

pp. 237-250

Author(s):

D. BEAUQUIER ◽

M. NIVAT ◽

D. NIWIŃSKI

Keyword(s):

Cardinal Number ◽

Tree Automaton ◽

Büchi Automata ◽

Infinite Trees ◽

Acceptance Condition ◽

Tree Languages ◽

Büchi Automaton ◽

Buchi Automata ◽

Computation Path

We modify an acceptance condition of Büchi automaton on infinite trees: rather than to require that each computation path is successful, we impose various restrictions on the number of successful paths in a run of the automaton on a tree. All these modifications alter the recognizing power of Büchi automata. We examine the classes induced by the acceptance conditions that require ≤α, ≥α, =α successful paths, where α is a cardinal number. It turns out that, except for some trivial cases, the “≤” classes are incomparable with the class Bü of Büchi acceptable tree languages, while the classes “≥” are strictly included in Bü.

Download Full-text

The Determinacy of Context-Free Games

Journal of Symbolic Logic ◽

10.2178/jsl.7804050 ◽

2013 ◽

Vol 78 (4) ◽

pp. 1115-1134 ◽

Cited By ~ 4

Author(s):

Olivier Finkel

Keyword(s):

Set Theory ◽

Winning Strategy ◽

Large Cardinal ◽

Büchi Automata ◽

Büchi Automaton ◽

Buchi Automata ◽

Context Free

AbstractWe prove that the determinacy of Gale-Stewart games whose winning sets are accepted by realtime 1-counter Büchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. We show also that the determinacy of Wadge games between two players in charge ofω-languages accepted by 1-counter Büchi automata is equivalent to the (effective) analytic Wadge determinacy. Using some results of set theory we prove that one can effectively construct a 1-counter Büchi automatonand a Büchi automatonsuch that: (1) There exists a model of ZFC in which Player 2 has a winning strategy in the Wadge gameW(L(),L()); (2) There exists a model of ZFC in which the Wadge gameW(L(),L()) is not determined. Moreover these are the only two possibilities, i.e. there are no models of ZFC in which Player 1 has a winning strategy in the Wadge gameW(L(),L()).

Download Full-text

Equivalent Characterizations of Fuzzy Büchi Automata

Chinese Journal of Computers ◽

10.3724/sp.j.1016.2013.01235 ◽

2014 ◽

Vol 36 (6) ◽

pp. 1235-1245

Author(s):

Zhao-Wei HAN ◽

Yong-Ming LI

Keyword(s):

Büchi Automata ◽

Buchi Automata

Download Full-text

Coinductive Algorithms for Büchi Automata

Fundamenta Informaticae ◽

10.3233/fi-2021-2046 ◽

2021 ◽

Vol 180 (4) ◽

pp. 351-373

Author(s):

Denis Kuperberg ◽

Laureline Pinault ◽

Damien Pous

Keyword(s):

State Space ◽

State Of The Art ◽

The State ◽

Specific Structure ◽

Büchi Automata ◽

Deterministic Automata ◽

Buchi Automata ◽

Language Equivalence ◽

Art Techniques

We propose a new algorithm for checking language equivalence of non-deterministic Büchi automata. We start from a construction proposed by Calbrix, Nivat and Podelski, which makes it possible to reduce the problem to that of checking equivalence of automata on finite words. Although this construction generates large and highly non-deterministic automata, we show how to exploit their specific structure and apply state-of-the art techniques based on coinduction to reduce the state-space that has to be explored. Doing so, we obtain algorithms which do not require full determinisation or complementation.

Download Full-text

Synthesis with Mandatory Stop Actions

10.24963/kr.2021/23 ◽

2021 ◽

Author(s):

Giuseppe De Giacomo ◽

Antonio Di Stasio ◽

Giuseppe Perelli ◽

Shufang Zhu

Keyword(s):

Model Checking ◽

Finite State Automata ◽

Deep Impact ◽

Synthesis Technique ◽

Büchi Automata ◽

Finite State ◽

Ltl Synthesis ◽

Buchi Automata ◽

The Impact

We study the impact of the need for the agent to obligatorily instruct the action stop in her strategies. More specifically we consider synthesis (i.e., planning) for LTLf goals under LTL environment specifications in the case the agent must mandatorily stop at a certain point. We show that this obligation makes it impossible to exploit the liveness part of the LTL environment specifications to achieve her goal, effectively reducing the environment specifications to their safety part only. This has a deep impact on the efficiency of solving the synthesis, which can sidestep handling Buchi determinization associated to LTL synthesis, in favor of finite-state automata manipulation as in LTLf synthesis. Next, we add to the agent goal, expressed in LTLf, a safety goal, expressed in LTL. Safety goals must hold forever, even when the agent stops, since the environment can still continue its evolution. Hence the agent, before stopping, must ensure that her safety goal will be maintained even after she stops. To do synthesis in this case, we devise an effective approach that mixes a synthesis technique based on finite-state automata (as in the case of LTLf goals) and model-checking of nondeterministic Buchi automata. In this way, again, we sidestep Buchi automata determinization, hence getting a synthesis technique that is intrinsically simpler than standard LTL synthesis.

Download Full-text