ε-TPN: definition of a Time Petri Net formalism simulating the behaviour of the timed grafcets

To allow a formal verification of timed GRAFCET models, many authors proposed to translate them into formal and well-reputed languages such as timed automata or Time Petri nets (TPN). Thus, the work presented in [Sogbohossou, Vianou, Formal modeling of grafcets with Time Petri nets, IEEE Transactions on Control Systems Technology, 23(5)(2015)] concerns the TPN formalism: the resulting TPN of the translation, called here ε-TPN, integrates some infinitesimal delays (ε) to simulate the synchronous semantics of the grafcet. The first goal of this paper is to specify a formal operational semantics for an ε-TPN to amend the previous one: especially, priority is introduced here between two defined categories of the ε-TPN transitions, in order to respect strictly the synchronous hypothesis. The second goal is to provide how to build the finite state space abstraction resulting from the new definitions. Afin de permettre la vérification formelle des grafcets temporisés, plusieurs auteurs ont proposé de les traduire dans des langages formels de réputation tels que les automates temporisés et les réseaux de Petri temporels (TPN). Ainsi, les travaux présentés dans [Sogbohossou, Vianou, Formal modeling of grafcets with Time Petri nets, IEEE Transactions on Control Systems Technology, 23(5)(2015)] concernent le formalisme des TPN: le réseau résultant de la traduction, dénommé ici ε-TPN, intègre des délais infinitésimaux (ε) pour simuler la sémantique synchrone du grafcet. Le premier objectif de cet article est de définir la sémantique opérationnelle d'un ε-TPN afin d'améliorer l'ancienne définition: spécifiquement, une priorité est introduite ici entre deux catégories de transitions définies pour ces réseaux, dans l'optique de respecter rigoureusement l'hypothèse synchrone. Le second but est de fournir une méthode de calcul de l'espace d'état fini qui découle des nouvelles définitions.

Download Full-text

Time Petri Nets with Action Duration

International Journal of Embedded and Real-Time Communication Systems ◽

10.4018/jertcs.2013040104 ◽

2013 ◽

Vol 4 (2) ◽

pp. 62-83 ◽

Cited By ~ 9

Author(s):

N. Belala ◽

D.E. Saїdouni ◽

R. Boukharrou ◽

A.C. Chaouche ◽

A. Seraoui ◽

...

Keyword(s):

Petri Nets ◽

Real Time ◽

Timed Automata ◽

Operational Semantics ◽

Time Interval ◽

Timing Constraints ◽

Time Petri Nets ◽

Real Time Systems ◽

High Level ◽

Time Systems

The design of real-time systems needs a high-level specification model supporting at the same time timing constraints and actions duration. The authors introduce in this paper an extension of Petri Nets called Time Petri Nets with Action Duration (DTPN) where time is associated with transitions. In DTPN, the firing of transitions is bound to a time interval and transitions represent actions which have explicit durations. The authors give an operational semantics for DTPN in terms of Durational Action Timed Automata (DATA). DTPN considers both timing constraints and durations under a true-concurrency semantics with an aim of better expressing concurrent and parallel behaviours of real-time systems.

Download Full-text

State space computation and analysis of Time Petri Nets

Theory and Practice of Logic Programming ◽

10.1017/s147106840600264x ◽

2006 ◽

Vol 6 (3) ◽

pp. 301-320 ◽

Cited By ~ 20

Author(s):

GUILLAUME GARDEY ◽

OLIVIER H. ROUX ◽

OLIVIER F. ROUX

Keyword(s):

Petri Nets ◽

State Space ◽

Petri Net ◽

Timed Automata ◽

Reactive Systems ◽

Time Petri Nets ◽

Classical State ◽

Time Petri Net ◽

Reduction Methods ◽

Timed Automaton

The theory of Petri Nets provides a general framework to specify the behaviors of real-time reactive systems and Time Petri Nets were introduced to take also temporal specifications into account. We present in this paper a forward zone-based algorithm to compute the state space of a bounded Time Petri Net: the method is different and more efficient than the classical State Class Graph. We prove the algorithm to be exact with respect to the reachability problem. Furthermore, we propose a translation of the computed state space into a Timed Automaton, proved to be timed bisimilar to the original Time Petri Net. As the method produce a single Timed Automaton, syntactical clocks reduction methods (DAWS and YOVINE for instance) may be applied to produce an automaton with fewer clocks. Then, our method allows to model-check T-TPN by the use of efficient Timed Automata tools.

Download Full-text

Verification of Event-Driven Process Chain with Timed Automata and Time Petri Nets

2017 9th IEEE-GCC Conference and Exhibition (GCCCE) ◽

10.1109/ieeegcc.2017.8448053 ◽

2017 ◽

Cited By ~ 1

Author(s):

Anam Amjad ◽

Farooque Azam ◽

Muhammad Waseem Anwar ◽

Wasi Haider Butt

Keyword(s):

Petri Nets ◽

Timed Automata ◽

Time Petri Nets ◽

Process Chain ◽

Event Driven

Download Full-text

Bridging the Gap Between Timed Automata and Bounded Time Petri Nets

Lecture Notes in Computer Science - Formal Modeling and Analysis of Timed Systems ◽

10.1007/11867340_7 ◽

2006 ◽

pp. 82-97 ◽

Cited By ~ 26

Author(s):

Bernard Berthomieu ◽

Florent Peres ◽

François Vernadat

Keyword(s):

Petri Nets ◽

Timed Automata ◽

Time Petri Nets

Download Full-text

Comparison of the Expressiveness of Timed Automata and Time Petri Nets

Lecture Notes in Computer Science - Formal Modeling and Analysis of Timed Systems ◽

10.1007/11603009_17 ◽

2005 ◽

pp. 211-225 ◽

Cited By ~ 34

Author(s):

Beatrice Bérard ◽

Franck Cassez ◽

Serge Haddad ◽

Didier Lime ◽

Olivier H. Roux

Keyword(s):

Petri Nets ◽

Timed Automata ◽

Time Petri Nets

Download Full-text

Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata

Lecture Notes in Computer Science - Applications and Theory of Petri Nets 2004 ◽

10.1007/978-3-540-27793-4_4 ◽

2004 ◽

pp. 37-76 ◽

Cited By ~ 20

Author(s):

Wojciech Penczek ◽

Agata Półrola

Keyword(s):

Model Checking ◽

Petri Nets ◽

Timed Automata ◽

Time Petri Nets ◽

Temporal Properties

Download Full-text

Description of membrane systems with time Petri nets: promoters/inhibitors, membrane dissolution, and priorities

Journal of Membrane Computing ◽

10.1007/s41965-020-00062-y ◽

2020 ◽

Vol 2 (4) ◽

pp. 341-354

Author(s):

Péter Battyányi ◽

György Vaszil

Keyword(s):

Petri Nets ◽

Petri Net ◽

Time Petri Nets ◽

Membrane Systems ◽

Time Petri Net ◽

Priority Relation ◽

Complex Cases

AbstractWe continue the investigations of the connection between membrane systems and time Petri nets by extending the examined class of systems from simple symbol-object membrane systems to more complex cases: rules with promoters/inhibitors, membrane dissolution, and priority relation on the rules. By constructing the simulating time Petri net, we retain one of the main characteristics of the Petri net model; namely, the firings of the transitions can take place in any order, and there is no need to introduce maximal parallelism in the Petri net semantics. Instead, we substantially exploit the gain in computational strength obtained by the introduction of the timing feature for Petri nets.

Download Full-text