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.
Back to the Petri Nets Bibliography