Autor: Szczęśniak, B. - Katalog OPAC zbiorów

Skocz do pozycji: 1.

Tytuł:: SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties
Autorzy:: Woźna-Szcześniak, B.
Szcześniak, I.
Powiązania:: https://bibliotekanauki.pl/articles/951862.pdf
Data publikacji:: 2015
Wydawca:: Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie. Wydawnictwo Uczelniane
Tematy:: model czasowy
logika czasowa
drzewo obliczeń
timed models
timed logic
computation tree
Opis:: We define an SAT-based bounded model checking (BMC) method for RTECTLK (the existential fragment of the real-time computation tree logic with knowledge) that is interpreted over timed models generated by timed interpreted systems. Specifically, we translate the model checking problem for RTECTLK to the model checking problem for a variant of branching temporal logic (called EyCTLK) interpreted over an abstract model, and we redefine an SAT-based BMC technique for EyCTLK.
Źródło:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics; 2015, 20; 69-81
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: 2.

Tytuł:: On the SMT-based verification of communicative commitments
Autorzy:: Woźna-Szcześniak, B.
Szcześniak, I.
Powiązania:: https://bibliotekanauki.pl/articles/121962.pdf
Data publikacji:: 2016
Wydawca:: Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie. Wydawnictwo Uczelniane
Tematy:: zobowiązania komunikacyjne
język komunikacji
semantyka mentalna
język CCTL
communications commutments
langue of communication
CCTL language
Opis:: We propose an SMT-based bounded model checking (BMC) technique for the existential fragments of CCTL*K – an epistemic temporal logic extended to include modalities for different social commitments – and for multi-agent systems modelled by Communication Interpreted Systems (CIS). Furthermore, we exemplify the use of the technique by means of the NetBill protocol, a popular example in the MAS literature related to the modelling of business processes.
Źródło:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics; 2016, 21; 161-187
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ł:: SAT-based searching for k-quasi-optimal runs in weighted timed automata
Autorzy:: Woźna-Szcześniak, B.
Zbrzezny, A.
Powiązania:: https://bibliotekanauki.pl/articles/121744.pdf
Data publikacji:: 2010
Wydawca:: Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie. Wydawnictwo Uczelniane
Tematy:: SAT
timed automata
air traffic control problem
reachability problem
automat czasowy
problem kontroli ruchu lotniczego
problem osiągalności
Opis:: In the paper we are concerned with an optimal cost reachability problem for weighted timed automata, and we use a translation to SAT to solve the problem. In particular, we show how to find a run of length k ∈ IN that starts at the initial state and terminates at a state containing a target location, its total cost belongs to the interval [c,c+1), for some natural number c ∈ IN, and the cost of each other run of length k, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of runs is called k-quasi-optimal. We exemplify the use of our solution to the mentioned problem by means of the air traffic control problem, and we provide some preliminary experimental results.
Źródło:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics; 2010, 15; 163-176
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ł:: Verifying RTECTL properties of a train controller systems
Autorzy:: Woźna-Szcześniak, B.
Zbrzezny, A.
Zbrzezny, Andrzej
Powiązania:: https://bibliotekanauki.pl/articles/121877.pdf
Data publikacji:: 2011
Wydawca:: Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie. Wydawnictwo Uczelniane
Tematy:: RTECTL
train controller systems
BMC method
system kontrolera pociągu
metoda BMC
Opis:: In the paper we deal with a classic concurrency problem - a faulty train controller system (FTC). In particular, we formalize it by means of finite automata, and consider several properties of the problem, which can be expressed as formulae of a soft real-time branching time temporal logic, called RTECTL. Further, we verify the RTECTL properties of FTC by means of SAT-based bounded model checking (BMC) method, and present the performance evaluation of the BMC method with respect to the considered problem. The performance evaluation 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; 2011, 16; 153-162
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: 5.

Tytuł:: A GPGPU–based simulator for prism: statistical verification of results of PMC
Autorzy:: Copik, M.
Rataj, A.
Woźna-Szcześniak, B.
Powiązania:: https://bibliotekanauki.pl/articles/121899.pdf
Data publikacji:: 2017
Wydawca:: Uniwersytet Humanistyczno-Przyrodniczy im. Jana Długosza w Częstochowie. Wydawnictwo Uczelniane
Tematy:: GPGPU
symulacja Monte Carlo
pryzmat
probabilistyczny model statystyczny
Monte Carlo simulation
prism
probabilistic model checking
statistical model checking
probabilistic logics
Opis:: We describe a GPGPU–based Monte Carlo simulator integrated with Prism. It supports Markov chains with discrete or continuous time and a subset of properties expressible in PCTL, CSL and their variants extended with rewards. The simulator allows an automated statistical verification of results obtained using Prism’s formal methods.
Źródło:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics; 2017, 22; 85-97
2450-9302
Pojawia się w:: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
Dostawca treści:: Biblioteka Nauki

Artykuł

Informacja