Where

Laboratoire Spécification et Vérification
École Normale Supérieure de Cachan
61, avenue du Président Wilson
94235 Cachan CEDEX
France
http://www.lsv.ens-cachan.fr

Title: Accelerated Paths in Petri Nets

Keywords: Petri nets, acceleration, logics.

Description

Although the exact complexity of accessibility in Petri nets is still unsettled, covering and boundedness were proven ExpSpace-complete by [CLM76,Rac78]. Rackoff’s technique was later generalized by [Yen92] to a logical language on paths in Petri nets, with the same ExpSpace bound.

However, it turns out that Yen’s algorithm only works for a fragment of the original logic, called increasing path formulæ [AH09]. Although many properties can still be expressed in this fragment, the properties that rely on accelerations (i.e. introduction of ω values in a Karp and Miller covering tree contruction) do not fit in this restricted fragment. In particular, the complexity of the regularity problem—whether the set of traces of a Petri net is a regular language [VVN81]—is currently in balance. Another instance is that of T-boundedness—whether the set of traces is a bounded language [CFS09].

The aim of this internship is to initiate research on path logics for Petri nets that allow to express accelerations but remain verifiable in exponential space. A first step is to examine how to adapt Rackoff’s algorithm to check T-boundedness and regularity in exponential space. A second step is to generalize these insights and propose a sensible language for accelerated paths in Petri nets.

Contact

Références

[AH09]

Mohamed-Faouzi Atig and Peter Habermehl. On Yen’s path logic for Petri nets. In Olivier Bournez and Igor Potapov, editors, RP’09, volume 5797 of Lecture Notes in Computer Science, pages 51–63. Springer, 2009.

[CFS09]

Pierre Chambart, Alain Finkel, and Sylvain Schmitz. Liveness for T-bounded well-structured transition systems. 2009.

[CLM76]

E. Cardoza, Richard J. Lipton, and Albert R. Meyer. Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report. In STOC’76, pages 50–54. ACM Press, 1976.

[Rac78]

Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223–231, 1978.

[VVN81]

Rüdiger Valk and Guy Vidal-Naquet. Petri nets and regular languages. Journal of Computer and System Sciences, 23(3):299–325, 1981.

[Yen92]

Hsu-Chun Yen. A unified approach for deciding the existence of certain petri net paths. Information and Computation, 96(1):119–137, 1992.

This document was translated from L^AT_EX by H^EV^EA.