Condensed State Spaces for Timed Petri Nets

2001 ◽  
pp. 101-120 ◽  
Author(s):  
Søren Christensen ◽  
Lars Michael Kristensen ◽  
Thomas Mailund
Keyword(s):  
Petri Nets ◽  
Condensed State ◽  
Timed Petri Nets ◽  
State Spaces

scholarly journals Well (and Better) Quasi-Ordered Transition Systems

2010 ◽  
Vol 16 (4) ◽  
pp. 457-515 ◽  
Author(s):  
Parosh Aziz Abdulla
Keyword(s):  
Petri Nets ◽  
Timed Automata ◽  
Timed Petri Nets ◽  
Transition Systems ◽  
State Spaces ◽  
Rewriting Systems ◽  
Symbolic Representations ◽  
Infinite State ◽  
Lossy Channel ◽  
Quasi Ordering

AbstractIn this paper, we give a step by step introduction to the theory ofwell quasi-orderedtransition systems. The framework combines two concepts, namely (i) transition systems which aremonotonicwrt. awell-quasi ordering; and (ii) a scheme for symbolicbackwardreachability analysis. We describe several models with infinite-state spaces, which can be analyzed within the framework, e.g., Petri nets, lossy channel systems, timed automata, timed Petri nets, and multiset rewriting systems. We will also presentbetter quasi-orderedtransition systems which allow the design of efficient symbolic representations of infinite sets of states.

scholarly journals Computer Aided Verification of Lamport's Fast Mutual Exclusion Algorithm - Using Coloured Petri Nets and Occurrence Graphs with Symmetries

1997 ◽  
Vol 26 (512) ◽  
Author(s):  
Jens Bæk Jørgensen ◽  
Lars Michael Kristensen
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Mutual Exclusion ◽  
Condensed State ◽  
Coloured Petri Nets ◽  
Computer Tool ◽  
State Spaces ◽  
Index Terms ◽  
High Level ◽  
Mutual Exclusion Algorithm

<p>In this paper, we present a new computer tool for verification of distributed systems. As an example, we establish the correctness of Lamport's Fast Mutual Exclusion Algorithm. The tool implements the method of occurrence graphs with symmetries (OS-graphs) for Coloured Petri Nets(CP-nets). The basic idea in the approach is to exploit the symmetries inherent in many distributed systems to construct a condensed state space. We demonstrate a signigicant increase in the number of states which can be analysed. The paper is to a large extent self-contained and does not assume any prior knowledge of CP-nets (or any other kinds of Petri Nets) or OS-graphs. CP-nets and OS-graphs are not our invention. Our contribution is development of the tool and verification of the example.</p><p><strong>Index Terms:</strong> Modelling and Analysis of Distributed Systems, Formal Verification, Coloured Petri Nets, High-Level Petri Nets, Occurrence Graphs, State Spaces, Symmetries, Mutual Exclusion.</p>

Two Heuristic Algorithms for the Minimum Initial Marking Problem of Timed Petri Nets

2013 ◽  
Vol E96.A (2) ◽  
pp. 540-553
Author(s):  
Satoru OCHIIWA ◽  
Satoshi TAOKA ◽  
Masahiro YAMAUCHI ◽  
Toshimasa WATANABE
Keyword(s):  
Petri Nets ◽  
Heuristic Algorithms ◽  
Timed Petri Nets

A Compositional Semantics for Timed Petri Nets1

1990 ◽  
Vol 13 (2) ◽  
pp. 141-170
Author(s):  
Andrea Maggiolo-Schettini ◽  
Józef Winkowski
Keyword(s):  
Petri Nets ◽  
Compositional Semantics ◽  
Timed Petri Nets ◽  
Event Structures ◽  
Configuration Systems

Timed Petri nets and their behaviours are considered. A concept of a seminet is introduced. which generalizes the concept of a net, and suitable operations on seminets are defined, which allow constructing seminets from atoms corresponding to places and transitions. The behaviours of seminets are given in the form of so called configuration systems, a notion close to labelled event structures. Such behaviours can be combined with the aid of operations corresponding to those on seminets. In particular, the behaviour of a compound seminet can be obtained by combining the behaviours of components.

Sign in / Sign up

Export Citation Format

Share Document