Ta witryna wykorzystuje cookies. Więcej informacji można znaleźć na stronie Polityka dotycząca cookies i podobnych technologii. ZAMKNIJ Zamknij ostrzeżenie dotyczące cookies

Marek Adamek obronił pracę doktorską

Marek_Adamek_zdjecie

W dniu 19 listopada 2019 roku Marek Adamek obronił  rozprawę doktorską pt. "Rozwój aplikacji logik temporalnychw zastosowaniach informatycznych "  . Promotorem rozprawy był prof. dr hab. inż. Jan Mulawka

Abstract: Temporal logic systems are extensions of classical logic calculus, which allow to express time related dependencies where time not given explicitly. Such logics have been used in computer science over the last 40 years. One of them — which is highlighted in the dissertation is LTL (Linear-Time Temporal Logic) — which have already been deeply studied. In particular, there is a number of methods developed for LTL-based formal
inference and model checking. Some of them have high quality implementations which are used in computer science and telecommunication industry.
The main focus of the dissertation is on temporal logic LNC (Logic Next Change), which is a LTL fragment. Expressiveness of LNC is not as wide in comparison to LTL, however there still exists a significant number of problems for which LNC expressiveness is sufficient. The work provides analysis of boolean satisfiability and model checking problems in context of LNC. The conclusion is that the complexity of these problems
(NP-complete) is lower in comparison to LTL (PSPACE-complete). In addition to theoretical discussion efficient algorithms for boolean satisfiability and model checking problems has been designed and implemented.
Another interesting feature of LNC logic discussed in this dissertation is the relationship between LNC formulas and a subclass of Kripke structures. A LNC formula can be interpreted as a model under verification in model checking method. Such representation can be used for implementation of efficient and symbolic LTL model checking method based on reduction to LTL boolean satisfiability problem. To support claims stated in the thesis an experimental verification has been conducted. The tests were focused on efficiency nad correctness of proposed algorithms and methods. In great number of cases these methods present much better performance in comparison to existing tools used for LTL. These tools were selected to cover wide range of different methods for boolean satisfiability and model checking problems. The work also discusses possible practical applications of LNC logic — for example: executable specification language, planning or generation, verification and correction of binary streams — and indicates directions for further research in context of LNC and developed methods. In addition to the main part of the dissertation there are two Appendices which present implementation details of LNC in Scala and its usage for solving selected problems.

Streszczenie: Logiki temporalne są rozszerzeniem logiki klasycznej, umożliwiającym rozważanie zależności czasowych bez jawnego wprowadzania czasu. Formalizmy te są od prawie 40 lat wykorzystywane w informatyce. Jednym z nich jest logika LTL (Linear-Time Temporal Logic), która została już gruntownie przebadana, w szczególności opracowano dla niej szereg metod formalnego wnioskowania oraz metod weryfikacji modelowej.Wiele z nich ma wysokiej jakości implementacje, które są wykorzystywane w przemyśle informatycznym i telekomunikacyjnym.
Niniejsza praca poświęcona jest analizie logiki temporalnej LNC (Logic Next Change), będącej fragmentem LTL. Chociaż ogólnie ekspresywność LNC jest mniejsza niż w przypadku LTL, to jednak ciągle istnieje szerokie spektrum problemów, dla których siła wyrażania LNC jest wystarczająca. W pracy prowadzane są rozważania nad problemami badania spełnialności oraz weryfikacji modelowej w logice LNC, z których wynika, że klasy złożoności tych problemów są niższe (NP-zupełne) względem LTL (PSPACE-zupełne). Jako uzupełnienie tych rozważań zaproponowano efektywne algorytmy badania spełnialności i weryfikacji modelowej w logice LNC.
Innym zagadnieniem poruszanym w tej pracy jest związek pomiędzy formułami LNC a pewną klasą struktur Kripkego. Formuły te można interpretować jako modele poddawane weryfikacji w metodzie weryfikacji modelowej. Dla takiej reprezentacji istnieje efektywna i symboliczna metoda weryfikacji modelowej wykorzystująca redukcję do problemu badania spełnialności w LTL.
Oprócz rozważań teoretycznych praca zawiera wyniki przeprowadzonej weryfikacji eksperymentalnej pod kątem wydajności i poprawności zaproponowanych algorytmów (implementację wykonano w języku Scala). W znacznej większości przypadków opracowane metody uzyskały dużo lepsze wyniki w porównywaniu z dostępnymi obecnie
narzędziami dedykowanymi logice LTL. Wybrane narzędzia implementują różne techniki badania spełnialności i weryfikacji modelowej. Praca prezentuje również możliwe, praktyczne zastosowania logiki LNC — jak
przykładowo: język wykonywalnej specyfikacji wymagań, metoda planowania czy generacja, weryfikacja i korekcja ciągów binarnych — a także perspektywy dalszych badań w zakresie logiki LNC i opracowanych dla niej metod. Oprócz części zasadniczej, w pracy zamieszczono dwa Dodatki zawierające szczegółowy opis implementacji logiki LNC w języku Scala oraz przykłady wykorzystania tej implementacji do rozwiązania
wybranych problemów. 

Ostatnia modyfikacja: czwartek, 5 grudnia 2019, 10:51:22, Agnieszka Skalska

x x Aktualności (4) - wg daty publikacji

‹‹ Grudzień 2019 ››
Pon Wt Śr Czw Pt So N
            1
2 3 4 5 6 7 8
9 10 11 12 13 14 15
16 17 18 19 20 21 22
23 24 25 26 27 28 29
30 31