Wyniki wyszukiwania - BazTech

1

BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets

Męski A., Penczek W., Półrola A.

Fundamenta Informaticae

|

2011

|

Vol. 109, nr 3

305-321

EN

In the paper we present a bounded model checking for 1-safe Petri nets and properties expressed in LTL and the universal fragment of CTL, based on binary decision diagrams. The presented experimental results show that we have obtained a technique which performs better in some of the considered cases, in comparison with the existing SAT-based implementation. The results are also compared with standard BDD-based symbolic method.

2

High Accuracy Asymptotic Bounds on the BDD Size and Weight of the Hardest Functions

Lozhkin S.A., Shiganov A.E.

Fundamenta Informaticae

|

2010

|

Vol. 104, nr 3

239-253

EN

In this paper we study the representation of Boolean functions by general binary decision diagrams (BDDs). We investigate the size L(Σ) (number of inner nodes) of BDD Σ with different constraints on the number M(Σ) of its merged nodes. Furthermore, we introduce a weighted complexity measure W(Σ) = L(Σ) + ωM(Σ), where ω > 0. For the hardest Boolean function on n input variables we define the weight WBDD(n) and the size LBDD(n, t), where t limits the number of merged nodes. By using a new synthesis method and appropriate restrictions for the number t of merged nodes, we are able to prove tight upper and lower asymptotic bounds: [formula] which have a relative error of O(1/n). Our results show how weight and structural restrictions of general BDDs influence the complexity of the hardest function in terms of high accuracy asymptotic bounds.

3

Wykorzystanie binarnych diagramów decyzyjnych do syntezy wielopoziomowych układów logicznych

Opara A.

Pomiary Automatyka Kontrola

|

2006

|

R. 52, nr 7 bis

115--117

PL

W artykule przedstawiona jest koncepcja wykorzystania wielokorzeniowych binarnych diagramów decyzyjnych (BDD) do reprezentacji zbioru funkcji logicznych. Funkcje te są poddawane dekompozycji, tak by można je było zaimplementować w typowych strukturach FPGA. Większość stosowanych algorytmów opartych o BDD operuje na pojedynczych funkcjach, dając mniejsze możliwości znajdowania wspólnych zależności. W prezentowanym rozwiązaniu operowanie na wielu funkcjach pozwala na współdzielenie bloków związanych w dekompozycji Ashenhursta, a tym samym wymaga mniejszej ilości zasobów.

EN

This paper presents concept of using multi-root (shared) binary decision diagrams (SBDD) to represent a set of boolean functions. These functions are decomposed to implement them in typical FPGA devices. Most of algorithms based on BDD operates on single function, so many common relations can not be extracted. In presented approach operating on many functions gains better utilization of programmable device's resources.

4

Comparing BDD and SAT based techniques for model checking Chaum's Dining Cryptographers Protocol

Kacprzak M., Lomuscio A., Niewiadomski A., Penczek W., Raimondi F., Szreter M.

Fundamenta Informaticae

|

2006

|

Vol. 72, nr 1-3

215-234

EN

We analyse different versions of the Dining Cryptographers protocol by means of automatic verification via model checking. Specifically we model the protocol in terms of a network of communicating automata and verify that the protocol meets the anonymity requirements specified. Two different model checking techniques (ordered binary decision diagrams and SAT-based bounded model checking) are evaluated and compared to verify the protocols.

5

Kodowanie funkcji wyjściowych z obszarów diagramu BDD zespołu funkcji logicznych wyznaczonych podczas dekompozycji diagramu dla układów FPGA

Dzikowski A.

Elektronika : konstrukcje, technologie, zastosowania

|

2006

|

Vol. 47, nr 11

15-17

PL

Artykuł przedstawia wpływ kodowania funkcji wyjściowych z obszarów diagramu MTBDD, wyznaczonych różnymi metodami dekompozycji. Problem kodowania jest bardzo istotny, ponieważ od niego zależy liczba bloków CLB układu FPGA, które zostaną wykorzystane do implementacji dekomponowanego zespołu funkcji logicznych. Problem kodowania ma również pośrednio wpływ na czas propagacji uzyskanej w procesie dekompozycji struktury.

EN

The paper discusses influence of output function coding for MTBDD areas obtained as a result of decomposition on quality of synthesis dedicated for FPGA circuits. Coding constitutes a very important problem in synthesis, because it influences the number of CLB blocks utilised to implement the set of boolean functions beeing subject to decomposition. Coding can also indirectly influence propagation delays in the synthesised structure.

6

BDD-based decompositions of multiple output logic functions

Dzikowski A., Hrynkiewicz E.

Bulletin of the Polish Academy of Sciences. Technical Sciences

|

2006

|

Vol. 54, nr 4

489-498

EN

The paper presents modification of the method dedicated to a complex area decomposition of a set of logic functions whereas the altered method is dedicated to implement the considered logic circuits within FPGA structures. The authors attempted to reach solu-tions where the number of configurable logic blocks and the number of structural layer would be reasonably balanced on the basis of the minimization principle. The main ad-vantage of the procedure when the decomposition is carried out directly on the BDD diagram is the opportunity of immediate checking whether the decomposed areas of the diagram do not exceed the resources of logic blocks incorporated into the integrated circuits that are used for implementation of the logic functions involved.

7

Application of OBDD Diagrams in Verification of Tabular Rule Systems

Szwed P., Ligęza A.

Schedae Informaticae

|

2005

|

Vol. 14

75-94

EN

This paper examines the application of Ordered Binary Decision Diagrams (OBDD) to modelling and verification of quality properties of rule systems. The transformation of an intentional specification of a tabular rule system into OBDD data structures was proposed and techniąues of verification of such ąuality properties as completeness, determinism and redundancy of rules were described.

8

The BDD Space Complexity of Different Forms of Concurrency

Baldamus M., Schneider K.

Fundamenta Informaticae

|

2002

|

Vol. 50, nr 2

111-133

EN

The automated verification of concurrent systems by model checking is often confronted with the state space explosion problem. A widely adopted method to tackle this problem is to use binary decision diagrams (BDDs) for representing systems and state spaces implicitly. However, it may be that even the system representation itself is prohibitively large. It is therefore interesting to study which factors influence the size of a BDD that represents the transition relation of a system. In this article, we consider the BDD representations of synchronous, asynchronous, and interleaved processes with communication via shared variables and present upper bounds for their sizes. To this end, we introduce a general representation strategy where catastrophic exponential growth of the BDD can only be due to the specifics of communication and/or write conflict resolution; it is neither due to the number of processes nor to the concurrency discipline. Moreover, conditions on communication and write conflict resolution are presented that are sufficient for polynomial sized BDD representations.