A new Petri net based formalism for specification, design and analysis of real-time systems

Current Petri net based methods for modeling and design of real-time systems rely on formalisms that are either expressive or analyzable, but not both. Our goal is to provide a new formalism bridging the gap between these positions. We start from a well known result on timed marked graphs, extend it to more general nets, and enhance the resulting formalism expressiveness by means of a set of transition expansion rules, which also enable hierarchical net structuring. A detailed example is discussed