Wyniki wyszukiwania - BazTech

Ograniczanie wyników

3 Fundamenta Informaticae

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: Büchi automata

Sortuj według:

Ogranicz wyniki do:

Coinductive Algorithms for Büchi Automata

Kuperberg Denis, Pinault Laureline, Pous Damien

Fundamenta Informaticae

2021

Vol. 180, nr 4

351--373

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.

Nested Emptiness Search for Generalized Büchi Automata

Tauriainen H.

Fundamenta Informaticae

2006

Vol. 70, nr 1,2

127-154

We generalize the classic explicit-state emptiness checking algorithm for Büchi word automata (the nested depth-first search) into Büchi automata with multiple acceptance conditions. Avoiding a degeneralization step improves the algorithm's worst-case memory requirements and reduces the worst-case number of state visits during the search. We give experimental results and discuss changes needed to make the generalized algorithm compatible with well-known probabilistic explicit-state model checking techniques.

Markov Decision Processes and Deterministic Büchi Automata

Beauquier D.

Fundamenta Informaticae

2002

Vol. 50, nr 1

1-13

We prove that given a Markov Decision Process (MDP) and a fixed subset of its states F, there is a Markov policy which maximizes everywhere the probability to reach F infinitely often. Moreover such a maximum policy is computable in polytime in the size of the MDP. This result can be applied in order to control a system with randomized or uncertain behavior with respect to a given property to optimize.