Verification by State Spaces with Equivalence Classes

1997 ◽  
Vol 26 (515) ◽  
Author(s):  
Jens Bæk Jørgensen ◽  
Lars Michael Kristensen
Keyword(s):  
Petri Nets ◽  
State Space ◽  
Equivalence Classes ◽  
Equivalence Relations ◽  
General Notion ◽  
State Spaces ◽  
Space Reduction ◽  
Full State ◽  
Reduction Methods ◽  
High Level

<p>This paper demonstrates the pontential of verification based on state spaces reduced by equivalence relations. The basic observation is that quite often, some states of a system are similar, i.e., they induce similar behaviours. Similarity can be formally expressed by defining equivalence relations on the set of states and the set of actions of a system under consideration. A state space can be constructed, in which the nodes correspond to equivalence classes of states and the arcs correspond to equivalence classes of actions. Such a state space is often much smaller than the ordinary full state space, but does allow derivation of many verification results.</p><p>Other researches have taken advantage of the symmetries of systems, which induce a certain kind of equivalence. The contribution fo this paper is to show that a more general notion of equivalence is useful. As example, a communication protocol modelled in the formalism of Coloured Petri Nets is verified. Aided by a computer tool supporting state spaces with equivalence classes, significant reduction of state spaces are exhibited.</p><p><strong>Topics</strong>. State space reduction methods, equivalence vs. symmetry, High-level Petri Nets, communication protocols.</p>

scholarly journals Modular State Space Analysis of Coloured Petri Nets

1997 ◽  
Vol 26 (524) ◽  
Author(s):  
Søren Christensen ◽  
Laure Petrucci
Keyword(s):  
Petri Nets ◽  
State Space ◽  
The State ◽  
Total System ◽  
Entire System ◽  
State Spaces ◽  
Space Analysis ◽  
State Space Analysis ◽  
Full State ◽  
Local Properties

<p>State Space Analysis is one of the most developed analysis methods for Petri Nets. The main problem of state space analysis is the size of the state spaces. Several ways to reduce it have been proposed but cannot yet handle industrial size systems.</p><p>Large models often consist of a set of modules. Local properties of each module can be checked separately, before checking the validity of the entire system. We want to avoid the construction of a single state space of the entire system.</p><p>When considering transition sharing, the behaviour of the total system can be capture by the state spaces of modules combined with a Synchronisation Graph. To verify that we do not lose information we show how the full state space can be conctructed.</p><p>We show how it is possible to determine usual Petri Nets properites, without unfolding to the ordinary state space.</p>

Exploiting symmetries of high-level Petri games in distributed synthesis

2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Nick Würdemann
Keyword(s):  
Petri Nets ◽  
State Space ◽  
Distributed System ◽  
Petri Net ◽  
Space Reduction ◽  
Ongoing Work ◽  
Player Game ◽  
High Level ◽  
State Space Reduction

Abstract Distributed Synthesis is the problem of automatically generating correct controllers for individual agents in a distributed system. Petri games model this problem by a game between two teams of players on a Petri net structure. Under some restrictions, Petri games can be solved by a reduction to a two player game. The concept of symmetries in Petri nets is closely related to high-level representations of Petri games. Applying symmetries to the states in the two-player game results in a significant state space reduction. We give an overview about (high-level) Petri games and the application of symmetries in this setting. We present ongoing work aiming to concisely describe solutions of Petri games by a high-level representation.

Using state space reduction methods for deadlock analysis in Ada tasking

1993 ◽  
Vol 18 (3) ◽  
pp. 51-60 ◽  
Author(s):  
S. Duri ◽  
U. Buy ◽  
R. Devarapalli ◽  
S. M. Shatz
Keyword(s):  
State Space ◽  
Space Reduction ◽  
Deadlock Analysis ◽  
Reduction Methods ◽  
State Space Reduction

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>

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.

Study of Performance Equivalent Simplification Analysis and Application of Stochastic Petri Nets

2013 ◽  
Vol 756-759 ◽  
pp. 2975-2978
Author(s):  
Da Bin Qi ◽  
Qiu Ju Li
Keyword(s):  
Petri Nets ◽  
State Space ◽  
Model Performance ◽  
Stochastic Petri Nets ◽  
Workflow Model ◽  
State Spaces ◽  
The Real ◽  
State Space Explosion ◽  
Model Based

State spaces of Stochastic Petri Nets (SPN) are exponent explosion based on subordinate models quantities, it is feasible to solve state space explosion. This article introduces basic theories of SPN performance equivalence simplification, integrates the real workflow of sanction management, constructs workflow model based on SPN comparatively, further more, simplifies the model by equivalence simplification theories, reduces models complexity, solves the model performance quantity analysis effective.

Sign in / Sign up

Export Citation Format

Share Document