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

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.

scholarly journals Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf

2011 ◽  
Vol Volume 14 - 2011 - Special... ◽  
Author(s):  
M. Sogbohossou ◽  
D. Delfieu
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
The State ◽  
Time Petri Nets ◽  
Real Time System ◽  
Time Petri Net ◽  
Finite Set ◽  
International Audience ◽  
Hard Real Time ◽  
Temporal Specifications

International audience For the formal verification of the concurrent or communicating dynamic systems modeled with Petri nets, the method of the unfolding is used to cope with the well-known problem of the state explosion. An extension of the method to the non safe time Petri nets is presented. The obtained unfolding is simply a prefix of that from the underlying ordinary Petri net to the time Petri net. For a certain class of time Petri nets, a finite prefix capturing the state space and the timed language ensues from the calculation of a finite set of finite processes with valid timings. The quantitative temporal constraints associated with these processes can serve to validate more effectively the temporal specifications of a hard real-time system. Pour la vérification formelle des systèmes dynamiques concurrents ou coopérants modélisés à l’aide des réseaux de Petri, la méthode du dépliage est utilisée pour endiguer le phénomène bien connu de l’explosion combinatoire. Une extension de la méthode aux réseaux de Petri temporels à modèle sous-jacent non sauf est présentée. Le dépliage obtenu est simplement un préfixe de celui du réseau de Petri ordinaire sous-jacent au réseau temporel. Pour une certaine classe de réseaux temporels, un préfixe fini capturant l’espace d’état et le langage temporisé découle du calcul d’un ensemble fini de processus finis réalisables. Les contraintes temporelles quantitatives associées à ces processus peuvent servir à valider plus efficacement les spécifications temporelles d’un système temps réel dur.

scholarly journals State space computation and analysis of Time Petri Nets

2006 ◽  
Vol 6 (3) ◽  
pp. 301-320 ◽  
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.

scholarly journals Controller Synthesis of Time Petri Nets Using Stopwatch

2013 ◽  
Vol 2013 ◽  
pp. 1-13 ◽  
Author(s):  
Parisa Heidari ◽  
Hanifa Boucheneb
Keyword(s):  
Complex Systems ◽  
Petri Nets ◽  
Petri Net ◽  
Controller Synthesis ◽  
Preemptive Scheduling ◽  
Time Petri Nets ◽  
Shared Resources ◽  
Time Petri Net ◽  
Ordinary Time ◽  
The Given

Scheduling is often a difficult task specially in complex systems. Few tools are targeted at both modeling and scheduling of the systems. In controller synthesis, a scheduler is seen as a controller to manage shared resources and timing requirements of a system. This paper proposes a time Petri net-based approach for controller synthesis and finding a scheduler using stopwatch. The solution suggested here is particularly interesting for preemptive scheduling purposes. This paper deals with time Petri nets with controllable and uncontrollable transitions and assumes that a controllable transition can be suspended and retrieved when necessary. In fact, the paper supposes that every controllable transition can be associated with stopwatch. With this hypothesis, the objective is to model a system by time Petri nets and calculate subintervals where the system violates the given property. Then, the controller associates the corresponding controllable transitions with stopwatch to suspend them in their bad subintervals. The interesting advantage of this solution is that this approach synthesizes an ordinary time Petri net model before adding stopwatch. Therefore, complicated computations and overapproximations required during controller synthesis of time Petri nets associated with stopwatch are avoided.

Local time membrane systems and time Petri nets

2020 ◽  
Vol 805 ◽  
pp. 175-192 ◽  
Author(s):  
Bogdan Aman ◽  
Péter Battyányi ◽  
Gabriel Ciobanu ◽  
György Vaszil
Keyword(s):  
Petri Nets ◽  
Local Time ◽  
Time Petri Nets ◽  
Membrane Systems

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

2019 ◽  
Vol Volume 31 - 2019 - CARI 2018 ◽  
Author(s):  
Médésu Sogbohossou ◽  
Medesu Sogbohossou ◽  
Antoine Vianou ◽  
Nabil Gmati ◽  
Eric Badouel ◽  
...  
Keyword(s):  
Petri Nets ◽  
Control Systems ◽  
Timed Automata ◽  
Operational Semantics ◽  
Formal Modeling ◽  
Time Petri Nets ◽  
Time Petri Net ◽  
Finite State ◽  
Definition Of ◽  
Finite State Space

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.

Schedule Optimization of Time Petri Nets Based on Ant Colony Systems

2012 ◽  
Vol 263-266 ◽  
pp. 1733-1739
Author(s):  
Xian Ming Liu ◽  
Li Pan ◽  
Hong Zheng
Keyword(s):  
Petri Net ◽  
Heuristic Search ◽  
Ant Colony ◽  
Time Petri Nets ◽  
Modeling And Analysis ◽  
Schedule Optimization ◽  
Artificial Ants ◽  
Time Petri Net ◽  
Ant Colony Systems ◽  
Update Rules

This paper presents a time Petri net model with the optimizing mechanism based on ant colony systems that addresses the problem of schedule optimization. The choice rules and pheromone update rules of artificial ants are embedded into the evolution rules of a time Petri net, so the modeling and scheduling analysis of real systems can be integrated into the same model. Compared with the approaches based on the heuristic search and genetic algorithms, our method efficiently unifies the modeling and analysis of schedule problems based on a time Petri net.

scholarly journals Applying global time Petri net analysis on the embedded software context

2011 ◽  
Vol 22 (6) ◽  
pp. 610-619 ◽  
Author(s):  
Leticia Mara Peres ◽  
Luis Allan Künzle ◽  
Eduardo Todt
Keyword(s):  
Petri Net ◽  
Schedulability Analysis ◽  
Embedded Software ◽  
Earliest Deadline First ◽  
Time Petri Nets ◽  
Time Petri Net ◽  
Global Time ◽  
Earliest Deadline ◽  
Class Graph ◽  
Time Type

This paper presents an application of Global Time technique (GTT) which is an approach to construct class graphs of Time Petri nets based on relative and global time. Besides the constructing of GTT class graph we propose a schedulability analysis of quantitative time type for fixed priority policies and Earliest Deadline First (EDF). We propose that analysis of scenarios, or behavior itineraries duration of a system, can be done using this approach.

SPECIFYING AND VERIFYING TEMPORAL BEHAVIOR OF HIGH ASSURANCE SYSTEMS USING REACHABILITY TREE LOGIC

1999 ◽  
Vol 09 (02) ◽  
pp. 233-249
Author(s):  
STEPHEN J. H. YANG ◽  
WILLIAM CHU ◽  
JONATHAN LEE
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Petri Net ◽  
System Modeling ◽  
Model System ◽  
Temporal Behavior ◽  
Time Petri Net ◽  
High Assurance ◽  
System Requirements ◽  
Reachability Tree

This paper presents our reachability tree logic (RTL) and its integration with time Petri nets to specify and verify the temporal behavior of high assurance systems. The specification phase begins with a system modeling to model system requirements into a time Petri net N and construct a reachability tree RT of N. We then use RTL to specify the desired temporal behavior as formula F. The verification phase uses a model-checking algorithm to check whether RT can satisfy F, that is to find firing sequences to satisfy F. If F is not satisfied, we then modify N into N′ and obtain a RT′ of the modified N′. The modification (refinement) continues until the modified RT′ can satisfy F. In addition, we will demonstrate how to reduce the complexity of model-checking by using our RTL-based algorithm. We have implemented a specification and verification toolkit called NCUPN (National Central University Petri Nets toolkit) using Java. NCUPN is now available on the Internet via

A Time Petri Net Model Based on Uniform Distribution

2010 ◽  
Vol 33 (5) ◽  
pp. 900-907 ◽  
Author(s):  
Li PAN ◽  
Zhi-Jun DING ◽  
Gang CHEN
Keyword(s):  
Uniform Distribution ◽  
Petri Net ◽  
Model Based ◽  
Time Petri Net
Sign in / Sign up

Export Citation Format

Share Document