PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 28

Liczba wyników na stronie
first rewind previous Strona / 2 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 2 next fast forward last
1
Content available remote 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.
2
Content available 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.
3
Content available remote Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
Woźna-Szcześniak B., Zbrzezny A.
Fundamenta Informaticae
|
2014
|
Vol. 135, nr 4
553--568
EN
We investigate a SAT-based bounded model checking (BMC) method for MTL (metric temporal logic) that is interpreted over linear discrete infinite time models generated by discrete timed automata. In particular, we translate the existential model checking problem for MTL to the existential model checking problem for a variant of linear temporal logic (called HLTL), and we provide a SAT-based BMC technique for HLTL. We show how to implement the BMC technique for HLTL and discrete timed automata, and as a case study we apply the technique in the analysis of GTPP, a Generic Timed Pipeline Paradigm modelled by a network of discrete timed automata.
4
Content available remote A Translation of the Existential Model Checking Problem from MITL to HLTL
Woźna-Szcześniak B., Zbrzezny A.
Fundamenta Informaticae
|
2013
|
Vol. 122, nr 4
401--420
EN
In the paper we propose a translation of the existential model checking problemfor timed automata and properties expressible in MITL to the existential model checking problem for HLTL. Such a translation, for example, allows to adopt LTL bounded model checking method for verification of the MITL properties
5
Content available remote Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems
Penczek W., Woźna-Szcześniak B., Zbrzezny A.
Fundamenta Informaticae
|
2012
|
Vol. 119, nr 3/4
373-392
EN
This paper makes two contributions to the verification of multi-agent systems modelled by interleaved interpreted systems. Firstly, the paper presents theoretical underpinnings of the SATbased bounded model checking (BMC) approach for LTL extended with the epistemic component (LTLK) over interleaved interpreted systems. Secondly, the BMC method has been implemented and tested on several benchmarks for MAS. The preliminary experimental results reveal advantages and disadvantages of our SAT-based BMC for LTLK and show that the method has a significant potential.
6
Content available remote Towards Automatic Composition of Web Services : SAT-Based Concretisation of Abstract Scenarios
Niewiadomski A., Penczek W., Półrola A., Szreter M., Zbrzezny A.
Fundamenta Informaticae
|
2012
|
Vol. 120, nr 2
181-203
EN
Automating the composition of web services is an object of a growing interest. In our paper [13] we proposed a method for converting the problem of the composition to the problem of building a graph of worlds consisting of formally defined objects, and presented the first phase of this composition aimed at building a graph of types of services (an abstract graph). In this work we propose a method of replacing abstract flows of this graph by sequences of concrete services able to satisfy the user’s request. The method is based on SAT-based reachability checking for (timed) automata with discrete data and parametric assignments.
7
Content available remote A New Translation from ECTL* to SAT*
Zbrzezny A.
Fundamenta Informaticae
|
2012
|
Vol. 120, nr 3/4
375-395
EN
In this paper we present a new translation from ECTL* to SAT and show that the proposed translation substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made experimental results, which demonstrate the efficiency of the method.
8
Content available Verifying RTECTL properties of a train controller systems
Woźna-Szcześniak B., Zbrzezny A., Zbrzezny Andrzej
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2011
|
Vol. 16
153--162
EN
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.
9
Content available remote PlanICS - a Web Service Composition Toolset
Doliwa D., Horzelski W., Niewiadomski A., Penczek W., Półrola A., Szreter M., Zbrzezny A.
Fundamenta Informaticae
|
2011
|
Vol. 112, nr 1
47-71
EN
The paper presents a prototype toolset to planning by automatic composition of web services. The main idea consists in arranging the composition into two main phases: abstract and concrete one, as well as to handle fully declarative user queries. The first abstract stage aims at finding all the possible sequences of the types of the services that can potentially satisfy the user request. The result, referred to as an abstract plan, is used in the concrete planning phase, which substitutes the types of the services with their concrete instances registered in the system. This is obtained by translating the problem of finding a composition of concrete services satisfying the user query into the reachability problem for (timed) automata with discrete data and parametric assignments, taking into account the concrete instances of services as well as the user query. Next, SAT-based parametric bounded model checking is used to obtaining the solutions in form of sequences of services invocations together with the example services' input values.
10
Content available SAT-based searching for k-quasi-optimal runs in weighted timed automata
Woźna-Szcześniak B., Zbrzezny A.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2010
|
Vol. 15
163--176
EN
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.
11
Content available A Boolean encoding of arithmetic operations
Zbrzezny A.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2010
|
Vol. 15
177--190
EN
In this paper we present algorithms for a Boolean encoding of four basic arithmetic operations on integer numbers: addition, subtraction, multiplication and division. Integer numbers are encoded in two's complement system as vectors of Boolean formulae, and arithmetic operations are faithfully encoded as operations on vectors of Boolean formulae.
12
Content available Model checking of java programs using networks of fadds
Woźna B., Zbrzezny A.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2009
|
Vol. 14
151-164
EN
In the paper we present the current theoretical base of the J2FADD tool, which translates a Java program to a network of finite automata with discrite data (FADDs).The reason for building the tool is that to model check a concurrent program writ-ten in Java by means of the tools like Uppaal or VerICS (the module VerICS ), an automata model of the Java program must be build first. This is because these tools verify only systems modeled as networks of automata, in particular, systems modeled as networks of FADDs. We also make an attempt to evaluate the J2FADD tool by comparison of it with the two well known Java verification tools: Bandera and Java PathFinder.
13
Content available remote A Translator of Java Programs to TADDs
Rataj A., Woźna B., Zbrzezny A.
Fundamenta Informaticae
|
2009
|
Vol. 93, nr 1-3
305-324
EN
The model checking tools Uppaal and VerICS accept a description of a network of Timed Automata with Discrete Data (TADDs) as input. Thus, to verify a concurrent programwritten in Java by means of these tools, first a TADD model of the program must be build. Therefore, we have developed the J2TADD tool that translates a Java program to a network of TADDs; the paper presents this tool. The J2TADD tool works in two stages. The first one consists in translation of a Java code to an internal assembly language (IAL). Then, the resulting assembly code is translated to a network of TADDs. We exemplify the use of the translator by means of the following well-known concurrency examples written in Java: race condition problem, dining philosophers problem, single sleeping barber problem and readers and writers problem.
14
Content available remote VerICS 2007 - a Model Checker for Knowledge and Real-Time
Kacprzak M., Nabiałek W., Niewiadomski A., Penczek W., Półrola A., Szreter M., Woźna B., Zbrzezny A.
Fundamenta Informaticae
|
2008
|
Vol. 85, nr 1-4
313-328
EN
The papers presents the current stage of the development of VerICS - a model checker for real-time and multi-agent systems. Depending on the type of a system considered, it enables to test various classes of properties - from reachability to temporal, epistemic and deontic formulas. The model checking methods used to this aim include both SAT-based and enumerative ones. In the paper we focus on new features of the verifier: SAT-based model checking for multi-agent systems and several extensions and improvements to real-time systems' verification.
15
Content available remote Towards Verification of Java Programs in VerICS
Zbrzezny A., Woźna B.
Fundamenta Informaticae
|
2008
|
Vol. 85, nr 1-4
533-548
EN
VerICS is a tool for the automated verification of timed automata and protocols written in both the Intermediate Language and the specification language Estelle. Recently, the tool has been extended to work with Timed Automata with Discrete Data and with multi-agent systems. This paper presents a prototype Timed Automata with Discrete Data model of Java programs. In addition, we show how to use the model together with the verification core of VerICS to validate the well-known alternating bit protocol written in Java. # Greedy Algorithm for Attribute Reduction
16
Content available remote Improving the Translation from ECTL to SAT
Zbrzezny A.
Fundamenta Informaticae
|
2008
|
Vol. 85, nr 1-4
513-531
EN
The objective of this paper is to offer an improvement to the translation from ECTL to SAT introduced in [14] and show that the improvement proposed substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made preliminary experimental results, which demonstrate the efficiency of the method.
17
Content available remote A Boolean Encoding of Arithmetic Operations
Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2007
|
Nr 999
1-35
EN
In this paper we present algorithms for a~Boolean encoding of four basic arithmetic operations on integer numbers: addition, subtraction, multiplication and division. Integer numbers are encoded in two's complement system as vectors of Boolean formulas and arithmetic operations are faithfully encoded as operations on vectors of Boolean formulas. In addition, we also provide an algorithm for a Boolean encoding of the operations of calculating integer square root and an algorithm for a Boolean encoding of the operation of exponentiation with nonnegative integer exponent.
PL
W pracy przedstawiamy algorytmy realizujące Boolowskie kodowanie czterech podstawowych operacji arytmetycznych: dodawania, odejmowania, mnożenia i dzielenia. Liczby całkowite są kodowane w systemie uzupełnieniowym do 2 jako wektory formuł Boolowskich a operacje arytmetyczne są zakodowane jako operacje na wektorach formuł Boolowskich. Dodatkowo przedstawiamy algorytmy realizujące Boolowskie kodowanie dla operacji obliczania całkowitego pierwiastka kwadratowego oraz dla operacji potęgowania.
18
Content available remote SAT-Based Reachability Checking for Timed Automata with Discrete Data
Zbrzezny A., Półrola A.
Fundamenta Informaticae
|
2007
|
Vol. 79, nr 3-4
579-593
19
Content available remote Bounded Model Checking for the Existential Fragment of TCTL-G and Diagonal Timed Automata
Woźna B., Zbrzezny A.
Fundamenta Informaticae
|
2007
|
Vol. 79, nr 1-2
229-256
EN
Bounded Model Checking (BMC) is one of the well known SAT based symbolic model checking techniques. It consists in searching for a counterexample of a particular length, and generating a propositional formula that is satisfiable iff such a counterexample exists. The BMC method is feasible for the various classes of temporal logic; in particular it is feasible for TECTL (the existential fragment of Time Computation Tree Logic) and Diagonal-free Timed Automata. The main contribution of the paper is to show that the concept of Bounded Model Checking can be extended to deal with TECTL-G properties of Diagonal Timed Automata. We have implemented our new BMC algorithm, and we present preliminary experimental results, which demonstrate the efficiency of the method.
20
Content available remote SAT-based Reachability Checking for Timed Automata with Diagonal Constraints
Zbrzezny A.
Fundamenta Informaticae
|
2005
|
Vol. 67, nr 1-3
303--322
EN
This paper deals with the problem of checking reachability for timed automata with diagonal constraints. Such automata are needed in many applications e.g. to model scheduling problems. We introduce a new discretization for timed automata which enables SAT based reachability analysis for timed automata for which comparisons between two clocks are allowed. In our earlier papers SAT based reachability analysis was restricted to the so called diagonal-free timed automata, where only comparisons between clocks and constants are allowed.
first rewind previous Strona / 2 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.