Wyniki wyszukiwania - BazTech

1

Comparing sat-based bounded model checking rtectl and ectl properties

Zbrzezny A. M.

Technical Sciences / University of Warmia and Mazury in Olsztyn

|

2017

|

nr 20(2)

131--147

EN

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.

2

Comparing SAT- and SMT- based bounded model checking for Ectl properties

Zbrzezny A. M.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2017

|

Vol. 22

161--175

EN

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.

3

SMT-based Searching for κ-quasi-optimal Runs in Weighted Timed Automata

Woźna-Szcześniak B., Zbrzezny A. M., Zbrzezny A.

Fundamenta Informaticae

|

2017

|

Vol. 152, nr 4

411--433

EN

We investigate a quasi-optimal cost reachability problem for weighted timed automata. We use a translation to the satisfiability modulo theories (SMT) problem to solve the problem. In particular, we show how to find a run of length κ ∊ N that starts at the initial state and terminates at a state containing the 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 κ, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of run is called κ-quasi-optimal. We exemplify the use of our solution to the investigated problem by means of the weighted timed generic pipeline protocol and the weighted job shop scheduling problem, and we provide some preliminary experimental results.

4

A comparison of SMT-solvers for timed weighted interpreted systems

Zbrzezny A. M.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2016

|

Vol. 21

189--206

EN

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.

5

SMT-based reachability analysis for simply-timed systems

Zbrzezny A. M., Zbrzezny A.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2015

|

Vol. 20

83--92

EN

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.