Autor: Zbrzezny, A. M. - Katalog OPAC zbiorów

Skocz do pozycji: 1.

Tytuł:: Comparing sat-based bounded model checking rtectl and ectl properties
Autorzy:: Zbrzezny, A. M.
Powiązania:: https://bibliotekanauki.pl/articles/297995.pdf
Data publikacji:: 2017
Wydawca:: Uniwersytet Warmińsko-Mazurski w Olsztynie
Tematy:: SAT
bounded model checking
ECTL
RTECTL
translation
Opis:: We compare two SAT-based bounded model checking algorithms for the properties expressed in the existential fragment of a soft real-time computation tree logic (RTECTL) and in the existential fragment of computation tree logic (ECTL). To this end, we use the generic pipeline paradigm (GPP) and the train controller system (TC), the classic concurrency problems, which we formalise by means of a finite transition system. We consider several properties of the problems that can be expressed in both RTECTL and ECTL, and we present the performance evaluation of the mentioned bounded model checking methods by means of the running time and the memory used.
Źródło:: Technical Sciences / University of Warmia and Mazury in Olsztyn; 2017, 20(2); 131-147
1505-4675
2083-4527
Pojawia się w:: Technical Sciences / University of Warmia and Mazury in Olsztyn
Dostawca treści:: Biblioteka Nauki

Artykuł

Skocz do pozycji: 2.

Tytuł:: Comparing SAT- and SMT- based bounded model checking for Ectl properties
Autorzy:: Zbrzezny, A. M.
Powiązania:: https://bibliotekanauki.pl/articles/121769.pdf
Data publikacji:: 2017
Wydawca:: Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie. Wydawnictwo Uczelniane
Tematy:: logika drzewa obliczeniowego
system sterowania
metoda ograniczonego modelowania
computational tree logic
control system
limited modelling method
Opis:: We compare two bounded model checking methods for properties expressed in the existential fragment of Computation Tree Logic (Ectl). To this end we use the generic pipeline paradigm (GPP) and the train controller system (TC), the classic concurrency problems, which we formalise by means of a finite transition system. We consider several properties of the problems that can be expressed in Ectl logic, and we present the performance evaluation of the mentioned bounded model checking methods by means of the running time and the memory used.
Źródło:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics; 2017, 22; 161-175
2450-9302
Pojawia się w:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
Dostawca treści:: Biblioteka Nauki

Artykuł

Skocz do pozycji: 3.

Tytuł:: A comparison of SMT-solvers for timed weighted interpreted systems
Autorzy:: Zbrzezny, A. M.
Powiązania:: https://bibliotekanauki.pl/articles/122082.pdf
Data publikacji:: 2016
Wydawca:: Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie. Wydawnictwo Uczelniane
Tematy:: SMT
model (BMC)
system wieloagentowy (MAS)
multi-agent (MAS)
Opis:: We compare four SMT-solvers for the same SMT-based bounded model checking algorithm for multi-agent systems modelled by timed weighted interpreted systems and for properties expressed in the existential fragment of epistemic weighted linear-time temporal logic (WELTLK). To this end, we use the timed weighted generic pipeline paradigm (TWGPP) and the timed weighted train controller system (TWTCS). We consider several properties of the problems that can be expressed in WELTLK, and we present the performance evaluation of the mentioned bounded model checking method using four different SMT-solvers: Z3, Yices, CVC4 and Mathsat, by means of the running time and the memory used.
Źródło:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics; 2016, 21; 189-206
2450-9302
Pojawia się w:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
Dostawca treści:: Biblioteka Nauki

Artykuł

Skocz do pozycji: 4.

Tytuł:: SMT-based reachability analysis for simply-timed systems
Autorzy:: Zbrzezny, A. M.
Zbrzezny, A.
Powiązania:: https://bibliotekanauki.pl/articles/951858.pdf
Data publikacji:: 2015
Wydawca:: Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie. Wydawnictwo Uczelniane
Tematy:: analiza osiągalności
SMT
systemy czasowe
reachability analysis
time systems
Opis:: In the paper we present Satisfiability Modulo Theory based (SMT-based) reachability analysis algorithm for Simply-Timed Systems (i.e., Kripke structures where each transition holds a duration, which is an arbitrary natural number) generated by simply-timed automata. The algorithm is based on a SMT-based encoding for Simply-Timed Systems. We have tested the algorithm in question by using the generic simply timed pipeline paradigm model as the benchmark. The performance evaluation of the algorithm is given by means of the running time and the memory used.
Źródło:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics; 2015, 20; 83-92
2450-9302
Pojawia się w:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
Dostawca treści:: Biblioteka Nauki

Artykuł

Informacja