Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning

Reynier P-A., Servais F.

Fundamenta Informaticae

2013

Vol. 122, nr 1-2

1--30

This paper presents the Monotone-Pruning algorithm (MP) for computing the minimal coverability set of Petri nets. The original Karp and Miller algorithm (K&M) unfolds the reachability graph of a Petri net and uses acceleration on branches to ensure termination. The MP algorithm improves the K&M algorithm by adding pruning between branches of the K&M tree. This idea was first introduced in the Minimal Coverability Tree algorithm (MCT), however it was recently shown to be incomplete. The MP algorithm can be viewed as the MCT algorithm with a slightly more aggressive pruning strategy which ensures completeness. Experimental results show that this algorithm is a strong improvement over the K&M algorithm as it dramatically reduces the exploration tree.

Undecidability Results for Timed Automata with Silent Transitions

Bouyer P., Haddad S., Reynier P-A.

Fundamenta Informaticae

2009

Vol. 92, nr 1-2

1-25

In this work, we study decision problems related to timed automata with silent transitions (TAε) which strictly extend the expressiveness of timed automata (TA). We first answer negatively a central question raised by the introduction of silent transitions: can we decide whether the language recognized by a TAε can be recognized by some TA? Then we establish in the framework of TAε some old open conjectures that O. Finkel has recently solved for TA. His proofs follow a generic scheme which relies on the fact that only a finite number of configurations can be reached by a TA while reading a timed word. This property does not hold for TAε , the proofs in the framework of TAε thus require more elaborated arguments. We establish undecidability of complementability, minimization of the number of clocks, and closure under shuffle. We also show these results in the framework of infinite timed languages.