*For the most recent entries see the
Petri Nets Newsletter.*

## Timed Verification of Asynchronous Circuits.

Møller, Jesper;
Hulgaard, Henrik;
Andersen, Henrik Reif
In:
*Concurrency and Hardware Design*, pages 274-312.
Advances in Petri Nets, Volume 2549 of Lecture Notes in Computer Science / J. Cortadella, A. Yakovlev, G. Rozenberg (Eds.) --- Springer Verlag,
November 2002.

Abstract:
We describe a methodology for analyzing timed systems symbolically. Given
a formula representing a set of timed states, we describe how to determine
a new formula that represents the set of states reachable by taking a
discrete transition or by advancing time. The symbolic representations are
given as formulae expressed in a simple first-order logic over constraints
of the form x - y <= d which can be combined with Boolean operators and
existentially quantified. The main contribution is a way of advancing time
symbolically essentially by quantifying out a special variable z which is
used to represent the current zero point in time. We describe how to model
asynchronous circuits using timed guarded commands and provide examples
that demonstrate the potential of the symbolic analysis.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*