Prace Instytutu Podstaw Informatyki PAN

Streszczenie :
Praca zawiera skrótowy opis gier ze skończoną liczbą nieskończonych populacji (typów), z których każda dysponuje skończoną liczbą strategii; wypłata pojedynczego gracza zależy od rozkładu wyborów strategii wszystkich populacji i jego własnego wyboru strategii. Podajemy konkretne przykłady zastosowań w kilku dziedzinach: alokacja przestrzenna (gatunków), modele ekonomiczne – model gospodarki drobnotowarowej i model ruchu drogowego. Dyskutujemy też krótko zagadnienia obliczeniowe i związki dużych gier, jak przedstawiono je w tym artykule, ze zwykłymi grami macierzowymi, grami z continuum graczy i z ewolucyją teorią gier.

Słowa kluczowe: duża gra, równowaga, strategia, typ gracza, alokacja przestrzenna, gospodarka drobnotowarowa, model ruchu drogowego, graf skierowany, liczby Fibonacciego

Tytuł: Statyczne duże gry ze skończoną liczbą typów graczy i strategii (praca napisana w j. angielskim)

Streszczenie :
Praca zawiera opis pewnego modelu akcji, który jest uniwersalny w tym sensie, że może służyć do reprezentowania akcji dowolnego rodzaju: dyskretnych, ciągłych, lub częściowo dyskretnych i częściowo ciągłych. Model ten opiera się na za lożeniu, że akcja jest wykonywana w pewnym środowisku obiektów. Opisuje jak możliwe wykonania akcji zmieniają sytuacje zaangażowanych obiektów. Wykorzystuje fakt, że fragmenty wykonań akcji są reprezentowane tak, że ich ograniczone segmenty mają jedynie trywialne automorfizmy. Model ma pewną strukturę algebraiczną i częściowy porządek przy którym podzbiory skierowane mają kresy górne.

Słowa kluczowe: Akcja, obiekt, instancja obiektu, wystąpienie instancji obiektu, wykonanie, segment wykonania, fragment wykonania, struktura wykonań, lposet, pomset, złożenie szeregowe, złożenie równoległe, niezależna składowa, porządek prefiksowy

Tytuł: Pewna propozycja uniwersalnego modelu akcji (praca napisana w j. angielskim)

Streszczenie :
Praca jest znacznym rozszerzeniem i uzupełnieniem Rozdziału 6 pracy Types and operations Prace IPI PAN Nr 1030 (również na http://arxiv.org/abs/1501.03043). Tutaj nowe pierwotne typy (odnoszące się do intuicyjnego pojęcia Continuum) są wprowadzone razem z pierwotnymi operacjami, konstruktorami oraz relacjami.

Słowa kluczowe: Continuum, teoria typów, podstawy Matematyki

Tytuł: Continuum jako typ pierwotny (praca napisana w j. angielskim)

Streszczenie :
Praca jest znacznym rozszerzeniem i uzupełnieniem Rozdziału 6 pracy Types and operations Prace IPI PAN Nr 1030 (również na http://arxiv.org/abs/1501.03043). Tutaj nowe pierwotne typy (odnoszące się do intuicyjnego pojęcia Continuum) są wprowadzone razem z pierwotnymi operacjami, konstruktorami oraz relacjami.

Słowa kluczowe: Continuum, teoria typów, podstawy Matematyki

Tytuł: Continuum jako typ pierwotny (praca napisana w j. angielskim)

Streszczenie :
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.

Słowa kluczowe: ATL, weryfikacja, aproksymacja

Tytuł: Dolna aproksymacja bezpamięciowego ATL o niepełnej informacji (praca napisana w j. angielskim)

Streszczenie :
Praca opisuje zastosowanie grafowej bazy danych do fazy planowania abstrakcyjnego w systemie automatycznej kompozycji usług sieciowych Planics. Planowanie abstrakcyjne jest pierwszą fazą procesu planowania usług, i polega na dopasowaniu typów usług i przetwarzanych przez nie obiektów, w celu wygenerowania planu abstrakcyjnego spełniającego zapytanie skierowane do systemu przez użytkownika. Rozwiązanie bardzo istotnie zwiększa efektywność istniejących metod planowania opartych na testowaniu spełnialności formuł logicznych lub bazujących na algorytmach genetycznych. Jest to szczególnie ważne w dziedzinie planowania usług sieciowych, gdzie od systemów oczekuje się bardzo krótkich czasów przetwarzania zapytań. Metoda ogranicza przeszukiwaną ontologię ze względu na zapytanie użytkownika, znacząco ułatwiając znalezienie rozwiązań.

Słowa kluczowe: automatyczna kompozycja usług sieciowych, grafowe bazy danych, planowanie abstrakcyjne

Tytuł: Ograniczone abstrakcyjne planowanie w systemie Planics wykorzystujace grafowe bazy danych (praca napisana w j. angielskim)

Streszczenie :
Zaproponowana została rewizja podstawowych pojęć typu i funkcji (nazywanej tutaj operacją). Typy, obiekty tych typów oraz operacje są konstruowane za pomocą prostej i uniwersalnej metody jako skończone struktury parametryzowane liczbami naturalnymi. Metoda ta pozwala na budowanie tzw. Uniwersum, które, w zamierzeniu, ma zawierać wszystko co jest efektywnie konstruowalne przynajmniej w sensie, jaki jest przyjęty w tej pracy. Przedstawione są argumenty, że Uniwersum nie jest jeszcze jedną formalną teorią, lecz może służyć jako ugruntowanie dla pewnych formalnych teorii.

Słowa kluczowe: typy, semantyka, podstawy

Tytuł: Typy i Operacje (praca napisana w j. angielskim)

Streszczenie :
Praca zawiera opis pewnego modelu akcji, który jest uniwersalny w tym sensie, że może służyć do reprezentowania akcji dowolnego rodzaju: dyskretnych, ciągłych, lub częściowo dyskretnych i częściowo ciągłych. Model ten opiera się na założeniu, że akcja jest wykonywana w pewnym środowisku obiektów. Opisuje jak możliwe wykonania akcji zmieniają sytuacje zaangażowanych obiektów. Wykorzystuje fakt, że wykonania akcji są reprezentowane tak, że ich ograniczone segmenty mają jedynie trywialne automor fizmy. Dzięki temu model ma pewną strukturę algebraiczną i częściowy porządek przy którym podzbiory skierowane mają kresy górne.

Słowa kluczowe: akcja, obiekt, instancja obiektu, wystąpienie instancji obiektu, wykonanie konkretne, struktura wykonań, zachowującą historie równoważność struktur wykonań, wykonanie abstrakcyjne, algebra wykonań abstrakcyjnych, częściowy porządek z kresami górnymi podzbiorów skierowanych, zredukowana struktura wykonań

Tytuł: Pewien model akcji i jego własności (praca napisana w j. angielskim)

Streszczenie :
Praca wprowadza logikę temporalną dla systemów reakcyjnych (RSTL), która jest interpretowana w modelach dla systemów reakcyjnych z ograniczeniami kontekstów. Systemy te uogólniają standardowe systemy reakcyjne przez wprowadzenie ograniczeń kontrolujących dopuszczalne konteksty. Ponadto, przedstawiono translację z systemów reakcyjnych z ograniczeniami kontekstów do formuł boolowskich, która umożliwia symboliczną weryfikację modelową dla tych systemów oraz RSTL. Wykazano również, że problem weryfikacji modelowej dla RSTL jest problemem PSPACE-zupełnym.

Słowa kluczowe: systemy reakcyjne, weryfikacja modelowa, logika temporalna

Tytuł: Weryfikacja temporalnych własności systemów reakcyjnych (praca napisana w j. angielskim)

Streszczenie :
Przedmiotem niniejszej pracy jest problem planowania abstrakcyjnego – pierwszy etap kompozycji usług sieciowych w systemie PlanICS. Prezentujemy rozwiązanie bazujące na kompaktowej reprezentacji planów abstrakcyjnych za pomocą wielozbiorów typów usług i redukcji problemu planowania do problemu spełnialności instancji SMT (Satisfiability Modulo Theories). Przedstawiamy zarówno teoretyczne aspekty planowania, jak również szczegóły symbolicznego kodowania i implementacji oraz wstępne wyniki eksperymentalne.

Słowa kluczowe: SMT, kompozycja usług sieciowych, planowanie abstrakcyjne

Tytuł: Planowanie abstrakcyjne z wykorzystaniem SMT w ontologii PlanICS (praca napisana w j. angielskim)"

Streszczenie :
Raport przedstawia nowe podejście do problemu planowania abstrakcyjnego za pomocą algorytmów genetycznych (AG). Problem planowania abstrakcyjnego polega na takiej kompozycji usług sieciowych, która spełnia zapytanie użytkownika. W raporcie pokazano sposób zastosowania AG do rozwiązania problemu planowania abstrakcyjnego oraz zaprezentowano wyniki eksperymentalne.

Słowa kluczowe: algorytmy genetyczne, kompozycja usług sieciowych, planowanie abstrakcyjne

Tytuł: Zastosowanie algorytmu genetycznego do problemu planowania abstrakcyjnego (praca napisana w j. angielskim)"

Streszczenie :
Niniejszy raport omawia zasady znakowania leksykalno-semantycznego banku drzew Składnica jednostkami leksykalnymi pochodzacymi ze Słowosieci. Ponadto prezentuje metodę przeniesienia znakowania nazw własnych z NKJP do Składnicy (wraz z ewaluacją). Wszystkie trzy wspomniane zasoby zostały pokrótce opisane. Na koniec przedstawiona została metoda aktualizacji uzyskanego znakowania do zmian zachodzących zarówno w Słowosieci, jak i w Składnicy.

Słowa kluczowe: lingwistyka komputerowa, korpusy tekstów, banki drzew, znakowanie korpusów, semantyka leksykalna, wordnet

Streszczenie :
Praca zawiera podstawy teoretyczne opisu i analizy losowych zachowań systemów współbieżnych dowolnej natury.

Słowa kluczowe: System współbieżny, stan, proces, składanie, etykietowany poset (zbiór częściowo uporządkowany), częściowo uporządkowany wielozbiór (pomset), skierowany zupełny porządek częściowy, topologia Scotta, Borelowska σ-algebra zbiorów, miara probabilistyczna.

Tytuł: Modele probabilistyczne losowych zachowań systemów współbieżnych (praca napisana w j. angielskim)

Streszczenie :
W pracy sformułowano pojęcie procesu rozumianego jako model przebiegu pewnego systemu (dyskretnego, ciągłego, lub mieszanego typu), wprowadzono operacje pozwalające wyrażać procesy złożone przez ich składowe, oraz przedstawiono ideę użycia tych środków do definiowania zachowań systemów współbieżnych.

Proces może mieć stan pocziątkowy, stan końcowy, lub oba te stany. Procesy z których jeden jest kontynuacją innego mogą być złożone szeregowo. Procesy niezależne, tzn. takie, które sobie nie przeszkadzają, mogą być złożone równolegle. Procesy mogą być prefiksami, tzn. niezależnymi składowymi segmentów początkowych innych procesów.

Procesy w pewnym uniwersum obiektów i szeregowe składanie procesów tworzą kategorię częściową zwaną częściową kategorią procesów. Procesy w pewnym uniwersum obiektów i operacje szeregowego i równoległego składania procesów tworzą algebrę częściową, zwaną algebrą procesów.

Częściowe kategorie i algebry procesów należą do aksjomatycznie definiowalnych klas algebr częściowych zwanych zachowaniowo-zorientowanymi kategoriami częściowymi i zachowaniowo-zorientowanymi algebrami. Pewne zachowaniowo-zorientowane kategorie częściowe i zachowaniowo-zorientowane algebry mogą być reprezetowane jako kategorie częściowe procesów i algebry procesów.

Kategorie częściowe i algebry procesów mogą służyć do definiowania zachowań systemów współbieżnych. Mianowicie, zachowanie systemu można definiować jako zbiór możliwych procesów tego systemu z pewną strukturą. Struktura ta odzwierciedla porządek prefiksowy procesów i czyni zbiór możliwych procesów zbiorem prefiksowo-zamkniętym i zawierającym kresy górne podzbiorów skierowanych.

Kategorie częściowe procesów i algebry procesów mogą służyć m.in. do definiowania zachowań o stanach i procesach ze specyficznymi strukturami wewnętrznymi, do defniowania operacji na zachowaniach, podobnych do operacji w znanych rachunkach zachowań, oraz do definiowania zachowań losowych.

Słowa kluczowe: Proces, stan, składanie szeregowe, składanie równoległe, kategoria, kategoria częściowa, monoid częściowy, niezależność, region, struktura, zachowanie, zachowanie losowe.

Tytuł: O pewnych algebrach dla systemów współbieżnych (praca napisana w j. angielskim)"

Streszczenie :
Niniejszy raport opisuje najbardziej znane korpusy tekstów języka naturalnego. Wpierw analizowane są zasady konstruowania korpusu, czyli doboru składających się nań tekstów w zależności od przyjetego rozmiaru oraz określenia jego struktury. Następnie prezentowane są najbardziej znane korpusy, głównie anglojęzyczne, lecz także innych języków europejskich: francuskiego, niemieckiego, rosyjskiego i czeskiego. Szczególną uwagę poświęcono dwum korpusom polskim - Korpusowi IPI PAN oraz Narodowemu Korpusowi Języka Polskiego. Oddzielny rozdział poświęcony jest bankom drzew, czyli korpusom znakowanym syntaktycznie.

Słowa kluczowe: lingwistyka komputerowa, korpusy tekstów, banki drzew, znakowanie korpusów."

Tytuł: O pewnych algebrach dla systemów współbieżnych (praca napisana w j. angielskim)"

Streszczenie :
Niniejszy raport opisuje wstępne eksperymenty dotyczące klasyfikacji syntaktyczno-semantycznej czasowników polskich. Wpierw omówione zostały istniejące prace z tej dziedziny, dotyczące głównie języka angielskiego. Następnie opisana została gradacyjna analiza odpowiedniości i skupień, która została użyta do klasyfikacji. Potem przedstawiony został semantyczno-syntaktyczny słownik walencyjny będący źródłem danych do klasyfikacji. Na koniec zaprezentowane były właściwe eksperymenty dotyczące klasyfikacji wraz z ich ewaluacją.

Słowa kluczowe: lingwistyka komputerowa, semantyka leksykalna, słowniki walencyjne, klasyfikacja czasowników, preferencje selekcyjne, wordnet.