CNAM: comment y aller
Abstract: symbolic algorithms based on binary-decision diagrams (BDDs) are routinely employed to verify complex VLSI designs with enormous state spaces. Such methods, however, have initially been applied mostly to synchronous circuits, because it has long been believed that they are not well suited to the analysis of asynchronous systems such as distributed software, Petri nets, and protocols. A few years ago, we introduced the Saturation algorithm, which not only can cope, but actually benefits from the interleaving behavior and locality of events in asynchronous systems. For such systems, Saturation has been shown in practice to have time and memory requirements that are several orders of magnitude lower than traditional breadth-first symbolic algorithms. In this talk, we give a brief survey of the current state-of-the art on the use of Saturation in different settings and applications, and of the classes of decision diagrams that can be used in such settings. Then, we discuss two specific topics in depth. The first one is a version of Saturation that uses edge-valued decision diagrams to compute distance information; this is useful to generate minimum-length witnesses in symbolic model checking, or to perform a bounded version of symbolic model checking. The second one is the use of structural information to heuristically derive a good static order for the decision diagram variables of arbitrary asynchronous systems and, in particular, of Petri nets.
Abstract: time Petri Nets (TPN) and Timed Automata (TA) are widely-used formalisms for the modeling and analysis of timed systems. A recently-developed approach for the analysis of TPNs concerns their translation to TAs, at which point efficient analysis tools for TAs can then be applied. One feature of much of this previous work has been the use of timed reachability analysis on the TPN in order to construct the TA. We present a method for the translation from TPNs to TAs which bypasses the timed reachability analysis step. Instead, our method relies on the reachability graph of the underlying untimed Petri net. We show that our approach is competitive for the translation of a wide class of TPNs to TAs in comparison with previous approaches, both with regard to the time required to perform the translation, and with regard to the number of locations and clocks of the produced TA.