Równoważność automatów Büchi i liniowego

Jest znanym faktem, że każda formuła LTL może być wyrażona przez automat Büchi . Ale najwyraźniej automaty Büchi są silniejszym i bardziej ekspresyjnym modelem. Słyszałem gdzieś, że automaty Büchi są równoważne μ- obliczeniom w czasie liniowym (to znaczy μ- obliczeniom ze zwykłymi punktami stałymi i tylko jednym operatorem czasowym: X ).$\omega$$\mu$$\mu$$\mathbf{X}$

Czy istnieje algorytm (konstruktywny dowód) tej równości?

Konstruktywna równoważność formuł stałych punktów liniowych w czasie ( niektórzy nazywają logikę TL), a automaty Buechi podano w pracy Madsa Dama z 1992 r.$\nu$

Naprawiono punkty Buchi Automata , FST i TCS 1992.

Na stronie 4 przedstawiono konstrukcję wzoru TL z automatu Buechi. Budowa automatu Buechi z formuły ν TL jest bardziej skomplikowana i zajmuje resztę papieru.$\nu$$\nu$

Pozostała część tej odpowiedzi jest krótkim argumentem, że wynik ten istniał w literaturze w znacznie mniej bezpośredniej formie. Pierre Wolper wykazał, że istnieją właściwości omega-regularne, których nie można zdefiniować LTL, i dał rozszerzenie LTL (zwane ETL), które może wyrażać właściwości omega-regularne.

Temporal Logic może być bardziej ekspresyjny , Pierre Wolper, Information and Computation, 1983.

$\nu$$\nu$$\nu$$\nu$

Logika czasowa, automaty i teorie klasyczne - wprowadzenie , Mads Dam, ESSLLI 1994.

Wykorzystanie automatów do scharakteryzowania logiki czasowej ustalonego punktu , Roope Kaivola

$\mu$

Możesz sprawdzić slajdy lub dokumenty Vardi. Zdecydowanie istnieje algorytm, ale IIRC negacje powodują ogromny wzrost czasu potrzebnego do wykonania tłumaczenia.