Wyniki wyszukiwania - BazTech

1

A More Efficient Time Petri Net State Space Abstraction Useful to Model Checking Timed Linear Properties

Bouchene H., Rakkay H.

Fundamenta Informaticae

|

2008

|

Vol. 88, nr 4

469-495

EN

We consider here time Petri nets (TPN model). We first propose an abstraction to its generally infinite state space which preserves linear properties of the TPN model. Comparing with TPN abstractions proposed in the literature, our abstraction produces graphs which are both smaller and faster to compute. In addition, our characterization of agglomerated states allows a significant gain in space. Afterwards, we show how to apply Yoneda's partial order reduction technique to construct directly reduced graphs useful to verify LTL_x properties of the model. Using our approach, both time and space complexities are reduced. Finally, we propose a time extension for Büchi automata which is useful to model checking timed linear properties of the model, using the abstraction proposed here.

2

Logic Synthesis for Asynchronous Circuits Based on STG Unfoldings and Incremental SAT

Khomenko V., Koutny M., Yakovlev A.

Fundamenta Informaticae

|

2006

|

Vol. 70, nr 1,2

49-73

EN

The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is deriving equations for logic gates implementing each output signal of the circuit. This is usually done using reachability graphs. In this paper, we avoid constructing the reachability graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for logic synthesis based on the Incremental Boolean Satisfiability (SAT) approach. Experimental results show that this technique leads not only to huge memory savings when compared with the methods based on reachability graphs, but also to significant speedups in many cases, without affecting the quality of the solution.

3

Detecting State Encoding Conflicts in STG Unfoldings Using SAT

Khomenko V., Koutny M., Yakovlev A.

Fundamenta Informaticae

|

2004

|

Vol. 62, nr 2

221--241

EN

The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is that of identifying whether an STG satisfies the Complete State Coding (CSC) requirement (which states that semantically different reachable states must have different binary encodings), and, if necessary, modifying the STG (by, e.g., inserting new signals helping to trace the current state) to meet this requirement. This is usually done using reachability graphs. In this paper, we avoid constructing the reachability graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for detection of CSC conflicts based on the Boolean Satisfiability (SAT) approach. Following the basic formulation of the state encoding conflict relationship, we present some problem-specific optimization rules. Experimental results show that this technique leads not only to huge memory savings when compared to the CSC conflicts detection methods based on reachability graphs, but also to significant speedups in many cases.