PL
 |
EN
Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 12

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

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available A Boolean encoding of arithmetic operations
100%
Zbrzezny A.
|
|
tom 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.
2
Content available remote A Note on Some Class of Locally Boolean Algebras
100%
Zbrzezny A.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2000/2001
|
tom Vol. 8
107--114
3
Content available remote Improving the Translation from ECTL to SAT
100%
Zbrzezny A.
|
2008
|
tom 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.
4
Content available remote Natural Deduction System for Some Three-valued Propositional Logic
100%
Zbrzezny A.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
1999
|
tom Vol. 6
148--152
5
Content available remote SAT-based Reachability Checking for Timed Automata with Diagonal Constraints
100%
Zbrzezny A.
|
|
tom 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.
6
Content available Model checking of java programs using networks of fadds
63%
Woźna B. , Zbrzezny A.
|
|
tom 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.
7
Content available remote Towards Verification of Java Programs in VerICS
63%
Zbrzezny A. , Woźna B.
|
2008
|
tom 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
8
Content available remote SMT-based Searching for κ-quasi-optimal Runs in Weighted Timed Automata
51%
Woźna-Szcześniak B. , Zbrzezny A. M. , Zbrzezny A.
|
|
tom 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.
9
Content available remote SAT-Based Bounded Model Checking for the Universal Fragment of TCTL
51%
Penczek W. , Woźna B. , Zbrzezny A.
|
|
tom Nr 947
1-26
EN
Bounded Model Checking (BMC) based on SAT methods consists in searching for a counterexample of a particular length and to generate a propositional formula that is satisfiable iff such a counterexample exists. Our paper shows how the concept of bounded model checking can be extended to deal with \TACTL\ (the universal fragment of \TCTL ) properties of a network of concurrent Timed Automata.
PL
Ograniczona Weryfikacja Modelowa, bzaująca na metodach SAT, polega na poszukiwaniu kontrprzykładów o długości ograniczonej przez pewną liczbę całkowitą k > 0 oraz generowanie formuły zdaniowej, która jest spełniana wtedy i tylko wtedy, gdy taki kontrprzykład istnieje. Celem tej pracy jest przedstawienie koncepcji ograniczonej weryfikacji modelowej dla automatów czasowych reprezentowanych przez siec współbieżnych i wzajemnie komunikujących się komponentów oraz własności wyrażanych w języku logiki TACTL (uniwersalnego fragmentu TCTL).
10
Content available remote Checking Reachability Properties for Timed Automata via SAT
51%
Woźna B. , Penczek W. , Zbrzezny A.
|
|
tom Nr 949
1-19
EN
The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded to the depth k Î N and encoded as a prepositional formula. Next the desired property is translated to a prepositional formula and the satisfiability of the conjunction of the two above defined formulas is checked. The unfolding of the transition can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results. Keywords : Reachability problem, bounded model checking, translation to SAT, Timed Automata, Augmented Region Graphs, discretization.
PL
Testowanie osiągalności automatów czasowych z wykorzystaniem SAT. Praca opisuje nowe podejście do problemu osiągalności dla automatów czasowych. Główna idea polega na połączeniu znanego algorytmu przeszukującego przestrzeń stanów wszerz metodą BFS oraz metody ograniczonej weryfikacji modelowej. Aby sprawdzić, czy stan spełniający daną własność jest osiągalny w modelu dla rozważanego automatu czasowego postępujemy następująco. Rozwijamy stopniowo relację przejścia dla automatu, aż do głębokości k Î N i kodujemy ją jako formułę zdaniową. Następnie, za pomocą formuły zdaniowej kodowana jest rozważana własność i sprawdzana jest spełnialność koniunkcji obydwu zdefiniowanych formuł zdaniowych. Rozwijanie relacji przejścia może zostać zakończone jeśli poszukiwany stan został znaleziony lub wszystkie stany danego automatu czasowego zostały przeszukane.
11
Content available remote Branching Time Bounded Model Checking for Elementary Net Systems
51%
Penczek W. , Woźna B. , Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2001
|
tom Nr 940
1-16
EN
Bounded Model Checking (BMC) has been recently introduced as an efficient verification method for reactive systems. BMC based on SAT methods consists in searching for a counterexample of a particular lenght and generating a propositional formula that is satisfiable iff such a counterexample exists. This new technique has been introduced by E.Clarke et al. for model checking of the linear time temporal logic (LTL). Our paper shows how the concept of bounded model checking can be extended to ACTL (the universal fragment of CTL). The implementation of the algorithm for Elementary Net Systems is described together with the experimental results.
PL
Ograniczona weryfikacja Modelowa, bazująca na metodach SAT, została wprowadzona jako uzupełniająca technika do Symbolicznej Weryfikacji Modelowej opartej na BDD. Podstawową ideą tej metody jest poszukiwanie kontrprzykładów o długości ograniczonej przez pewne całkowite k>0 oraz generowanie formuły zadaniowej, która jest spełnialna wtedy i tylko wtedy, gdy taki kontrprzykład istnieje. Ta nowa technika została po raz pierwszy wprowadzona przez E.Clarka, A.Biera, A. Cimatti'ego i Y.Zhu i zastosowana do weryfikacji modelowej formuł liniowej logiki temporalnej. Celem tej pracy jest przedstawienie koncepcji ograniczonej weryfikacji modelowej dla formuł logiki ACTL (uniwersalnego fragmentu CTL). Ponadto prezentujemy implementację algorytmu BCM dla Sieci Elementarnych wraz z wynikami eksperymentalnymi.
12
Content available remote VerICS 2007 - a Model Checker for Knowledge and Real-Time
32%
Kacprzak M. , Nabiałek W. , Niewiadomski A. , Penczek W. , Półrola A. , Szreter M. , Woźna B. , Zbrzezny A.
|
2008
|
tom 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.
first rewind previous Strona / 1 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ć.