Tytuł pozycji:
Towards partial order reductions for fragments of alternating-time temporal logic
A general semantics of strategic abilities of agents in asynchronous
systems with and without perfect information is proposed, and
some general complexity results for verification of strategic abilities
in asynchronous systems are presented. A methodology for
partial order reduction (POR) in verification of agents with imperfect
information is developed, based on the notion of traces
introduced by Mazurkiewicz. Two semantics of ATL∗
−X are considered
and it is shown that for memoryless imperfect information
(|=ir) contrary to memoryless perfect information (|=Ir), one can
apply techniques known for LTL−X.
Raport definiuje ogólną semantykę dla strategicznych umiejętności agentów w systemach asynchronicznych z pełną i częściową informacją, oraz prezentuje ogólne wyniki dotyczące złożoności weryfikacji strategicznych możliwości w systemach asynchronicznych. Metoda redukcji częścio-porządkowych, wykorzystująca ślady Mazurkiewicza, została zastosowana do weryfikacji agentów z niepełną informacją. Dla rozważanych dwóch semantyk logiki ATL*_x zostało pokazane, że dla bezpamięciowej niepełnej informacji (|=ir) w przeciwieństwie do bezpamięciowej pełnej informacji (|=Ir), można zastosować metody znane dla LTL_x.