Wyniki wyszukiwania - BazTech

1

Towards partial order reductions for fragments of alternating-time temporal logic

Dembiński P., Jamroga W., Mazurkiewicz A., Penczek W.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2016

|

Nr 1036

1--32

EN

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.

PL

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.

2

Underapproximating ATL with Imperfect Information and Imperfect Recall

Jamroga W., Knapik M.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2015

|

Nr 1032

1--16

EN

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.

PL

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.

3

What Agents Can Probably Enforce

Bulling N., Jamroga W.

Fundamenta Informaticae

|

2009

|

Vol. 93, nr 1-3

81-96

EN

Alternating-time Temporal Logic (ATL) is probably themost influential logic of strategic ability that has emerged in recent years. The idea of ATL is centered around cooperation modalities: ((A))ϒ is satisfied if the group A of agents has a collective strategy to enforce temporal property ϒ against the worst possible response from the other agents. So, the semantics of ATL shares the 'all-or-nothing' attitude of many logical approaches to computation. Such an assumption seems appropriate in some application areas (life-critical systems, security protocols, expensive ventures like space missions). In many cases, however, one might be satisfied if the goal is achieved with reasonable likelihood. In this paper, we try to soften the rigorous notion of success that underpins ATL.

4

Expressing and Verifying Temporal and Structural Properties of Mobile Agents

Bednarczyk M.A., Jamroga W., Pawłowski W.

Fundamenta Informaticae

|

2006

|

Vol. 72, nr 1-3

51-63

EN

Logics for expressing properties of Petri hypernets, a visual formalism for modelling mobile agents, are proposed. Two classes of properties are of interest-the temporal evolution of agents and their structural correlation. In particular, we investigate how the classes can be combined into a logic capable of expressing the dynamic evolution of the structural correlation. The problem of model checking properties of a class of the logic on Petri hypernets is shown to be pspace-complete.

5

Agents that Know How to Play

Jamroga W., Van der Hoek W.

Fundamenta Informaticae

|

2004

|

Vol. 63, nr 2,3

185--219

EN

We look at ways to enrich Alternating-time Temporal Logic (ATL) - a logic for specification and verification of multi-agent systems - with a notion of knowledge. Starting point of our study is a recent proposal for a system called Alternating-time Temporal Epistemic Logic (ATEL). We show that, assuming that agents act under uncertainty in some states of the system, the notion of allowable strategy should be defined with some caution. Moreover, we demonstrate a subtle difference between an agent knowing that he has a suitable strategy and knowing the strategy itself. We also point out that the agents should be assumed similar epistemic capabilities in the semantics of both strategic and epistemic operators. Trying to implement these ideas, we propose two different modifications of ATEL. The first one, dubbed Alternating-time Temporal Observational Logic (ATOL), is a logic for agents with bounded recall of the past. With the second, ATEL-R*, we present a framework to reason about both perfect and imperfect recall, in which we also incorporate operators for reasoning about the past. We identify some feasible subsystems of this expressive system.

6

Changing and using beliefs under incomplete information

Jamroga W.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2001

|

Nr 928

31-36

EN

The concept being proposed here is to use prototype semantics to represent an agent's belief state. Prototype semantics is a linguistic theory that emerged in the 1980s - the key idea is to describe the meaning of an utterance, or a notion, by defining the prototype (the most typical example to which the notion refers) and the extension rules describing 'family resemblances' between various entities and, in consequence, allowing to derive less typical instances from more typical ones. The intuition behind this paper is that in situations of incomplete information such a representation of the agent's knowledge may be easier to deal with than a straightforward probabilistic representation - especially when belief changes are not necessarily monotonic, and informations being acquired by the agent may be vague themselves. Moreover, when an exhaustive search through all the possibilities is impossible the agent may benefit from analyzing the typical situations instead of random ones. This property was tested for a family of games with incomplete information on binary trees.