PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 7

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available 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
Content available remote Simulation of Security Protocols based on Scenarios of Attacks
Jakubowska G., Dembiński P., Penczek W., Szreter M.
Fundamenta Informaticae
|
2009
|
Vol. 93, nr 1-3
185-203
EN
In this paper we offer a methodology allowing for simulation of security protocols, implemented in the higher-level language Estelle, using scenarios designed for external attacks. To this aim we apply a translation of specifications of security protocols from Common Syntax to Estelle and an encoding of schemes of attacks into Estelle scenarios. We show that such an intelligent simulation may efficiently serve for validating security protocols.
3
Content available remote Towards Scenarios of External Attacks upon Security Protocols
Dembiński P., Jakubowska G., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2008
|
nr 1012
1-24
EN
In this paper we consider a taxonomy of external attacks on security protocols in terms of a message origin and destination in addition to a session and step number. We use this taxonomy for designing algorithms, which for a given type of attack and parameters of the protocol return a scenario of an attack of this type. This way we can dramatically reduce the number of protocol runs to be generated in order to look for an attack upon a protocol in the process of verification or simulation. We show that our algorithms generate scenarios of attacks upon all the protocols, classified within our taxonomy, which are known to susceptible to these attacks. We exemplify the results of our algorithms for several protocols from \cite{SPORE} and \cite{CJ}.
PL
Rozważamy taksonomię zewnętrznych ataków na protokoły kryptograficzne w terminach nazwy wysyłającego i odbierającego wiadmość oraz numeru kroku i sesji. Używamy tej taksonomii do zaprojektowania algorytmów, które dla zadanego typu ataku i parametrów protokołu, zwracają scenariusze ataku tego typu. W ten sposób bardzo istotnie redukujemy liczbę przebiegów protokołu, które mają byc wygenerowane w celu poszukiwania ataku na protokół w procesie weryfikacji lub symulacji W Raporcie jest pokazane, że nasze alorytmy generują scenariusze ataków na protokoły, sklasyfikowane w naszej taksonomii, na które istnieją ataki tego typu. Wyniki zastosowania algorytmów prezentujemy na przykładzie kilku protokołów z \cite{SPORE} i \cite{CJ}.
4
Content available remote Verification of Timed Automata Based on Similarity
Dembiński P., Penczek W., Półrola A.
Fundamenta Informaticae
|
2002
|
Vol. 51, nr 1,2
59-89
EN
The paper presents a modification of the standard partitioning technique to generate abstract state spaces preserving similarity for Timed Automata. Since this relation is weaker than bisimilarity, most of the obtained models (state spaces) are smaller than bisimilar ones, but still preserve the universal fragments of branching time temporal logics. The theoretical results are exemplified for strong, delay, and observational simulation relations.
5
Content available remote A distributed algorithm for dynamic resource allocation : development and validation in Estelle
Dembiński P.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2000
|
nr 907
1-18
EN
This paper describes the development and validation of an Estelle specification of a distributed algorithm solving the dynamic resource allocation problem. This is a modified version of the algorithm originally proposed in (Winkowski 1998). The specification has been obtained and validated with Estelle Development Tools. The main steps in the construction of the specification are presented and the simulation techniques validating the obtained specification are sketched. The simulations show that the specification is free of dynamic errors and preserves such properties as mutual exlusion between tasks requiring the overlapping sets of resources and starvation freedom - the properties essential for any correct solution of the resource allocation problem. The full Estelle version of the algorithm is given in the Appendix.
PL
W pracy opisano przebieg specyfikowania w języku Estelle, a następnie symulacyjnej weryfikacji zmodyfikowanej wersji rozproszonego algorytmu (zaproponowanego w pracy (Winkowski 1998)) rozwiązującego problem dynamicznej alokacji zasobów. Zarówno konstrukcję specyfikacji, jak i jej weryfikację przeprowadzono z pomocą narzędzi Estelle Development Toolset. Pokazano główne kroki w tworzeniu specyfikacji oraz naszkicowano techniki symulacyjne użyte do jej weryfikacji. Symulacja pozwoliła na stwierdzenie braku dynamicznych błędów specyfikacji, ale przede wszystkim pokazała takie podstawowe własności dla zapewnienia poprawności każdego rozwiązania problemu dynamicznej alokacji, jak wykluczanie się zadań ubiegających się o te same zasoby i brak tzw. "zagładzania" zadań. Pełny tekst specyfikacji algorytmu w języku Estelle został zamieszczony w Dodatku.
6
Content available remote Randomized enumeration
Dembiński P.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
1998
|
nr 848
1-17
PL
W pracy zaproponowano probabilistyczną wersję rozproszonego algorytmu numeracji węzłów sieci procesów. Zaletą tego probabilistycznego podejścia jest to, że wynikowy algorytm poprawnie numeruje węzły sieci o dowolnej topologii i może być całkowicie asynchroniczny (w przypadku deterministycznych rozwiązań obie te cechy mają pewne ograniczenia). Przebadano zarówno poprawność zaproponowanego algorytmu jak i jego efektywność. Te ostatnią szacuje sie poprzez oczekiwaną liczbę 'rund', w terminach których zdefiniowano algorytm. Okazuje się, że ta oczekiwana wartość jest bliska jedynce, a to znaczy, że czas wykonania algorytmu jest w praktyce równy maksymalnemu czasowi przepływu informacji pomiędzy węzłami rozpatrywanej sieci. Algorytm został opisany w języku specyfikacji Estelle. Eksperymenty symulacyjne (wykonywane zarówno dla deterministycznych jak i probabilistycznych specyfikacji algorytmu w tym formalizmie) potwierdziły otrzymane rezultaty.
EN
The paper describes a randomized version of the distributed enumeration algorithm (protocol) in a network of processes. The advantage of the randomized approach is in that the resulting algorithm works for all network topologies and for fully asynchronous communication (which is not the case for the deterministic case). Correctness of the protocol is examined as well its efficiency. The latter is estimated in probabilistic terms by means of the expected number of 'drawing rounds' in which the algorithm is defined. The value is shown to be close to one and it means that practically the algorithm is performed in time needed to broadcast a message in the network. The algorithm is implemented in the specification language Estelle. Simulation experiments (with both deterministic and randomized Estelle specifications) confirmed the obtained results.
7
Content available remote Randomized enumeration
Dembiński P.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
1998
|
nr 848
1-17
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.