- Tytuł:
-
Underapproximating ATL with Imperfect Information and Imperfect Recall
Dolna Aproksymacja Bezpamięciowego ATL o Niepełnej Informacji - Autorzy:
-
Jamroga, W.
Knapik, M. - Powiązania:
- https://bibliotekanauki.pl/articles/182675.pdf
- Data publikacji:
- 2015
- Wydawca:
- Polska Akademia Nauk. Instytut Podstaw Informatyki PAN
- Tematy:
-
ATL
model checking
approximation
weryfikacja
aproksymacja - Opis:
-
We investigate the correspondence between model checking of af-AMCi and ATLir , on the example of reachability. We identify some of the reasons for the fact that these logics are of uncomparable expressivity. These observations form the basis for a novel method for underapproximating ATLir by means of fixed-point calculations. We introduce a special version of the next-step operator, called Persistent Imperfect Next-Step Operator h_iF and show how it can be used to define a new version of reachability that carries to ATLir.
W pracy badane są związki pomiędzy weryfikacją modelową Bezpamięciowej Logiki Temporalnej Czasu Alternującego z Niepełną Informacją ATLir i Epistemicznego Alternującego Mu-Rachunku af-AMCi. Jak pokazano, naturalne uogólnienia pojęcia osiągalności z ATLir -a do af-AMCi nie przynoszą dobrych efektów: osiągalność w af-AMCi nie pociąga za sobą osiągalności w ATLir . Po zidentyfikowaniu części powodów, dla których tak się dzieje, zaproponowano nową wersję operatora następnego kroku, który pozwala na przybliżanie osiągalności w ATLir przy pomocy obliczeń stałopunktowych. - Źródło:
-
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk; 2015, 1032; 1-16
0138-0648 - Pojawia się w:
- Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
- Dostawca treści:
- Biblioteka Nauki
Artykuł