scholarly journals A uniform approach to true-concurrency and interleaving semantics for Petri nets

1998 ◽  
Vol 206 (1-2) ◽  
pp. 219-256 ◽  
Author(s):  
Lutz Priese ◽  
Harro Wimmel
Keyword(s):  
Petri Nets ◽  
True Concurrency ◽  
Uniform Approach ◽  
Interleaving Semantics

True Concurrency Semantics

2014 ◽  
Vol 5 (2) ◽  
pp. 22-42 ◽  
Author(s):  
Souad Guellati ◽  
Ilham Kitouni ◽  
Riad Matmat ◽  
Djamel-Eddine Saidouni
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Timed Automata ◽  
Model Data ◽  
True Concurrency ◽  
New Class ◽  
Computation Tree ◽  
Interleaving Semantics ◽  
Finite State ◽  
Validation Technique

The model checking algorithms have been widely studied for timed automata, it's a validation technique for automatically verifying correctness properties of finite-state systems, which are based on interleaving semantics. Therefore the actions are assumed instantaneous. To overcome the hypothesis of temporal and structural atomicity of actions, we use the durational actions timed automata model (daTA). This model is based on the maximality semantics. Properties to be verified are expressed using the Timed Computation Tree Logic (TCTL). For dealing with formal verification, the Maximality-based Region Graph (MRG) is defined and an adaptation of the model checking algorithm is proposed. The use of the maximality semantics based verification provides new class of properties related to simultaneous progress of actions at different states.

An interleaving semantics for UML 2 interactions using Petri nets

2013 ◽  
Vol 232 ◽  
pp. 276-293 ◽  
Author(s):  
Thouraya Bouabana-Tebibel ◽  
Stuart H. Rubin
Keyword(s):  
Petri Nets ◽  
Interleaving Semantics

scholarly journals Mechanized Theory of Event Structures: A Case of Parallel Register Machine

2021 ◽  
Vol 33 (3) ◽  
pp. 143-154
Author(s):  
Vladimir Gladstein ◽  
Dmitrii Mikhailovskii ◽  
Evgenii Moiseenko ◽  
Anton Trunov
Keyword(s):  
True Concurrency ◽  
Atomic Actions ◽  
Event Structures ◽  
The Coq Proof Assistant ◽  
Register Machine ◽  
Interleaving Semantics ◽  
Coq Proof Assistant ◽  
Concise Representation ◽  
The Individual ◽  
Semantics Of Concurrency

The true concurrency models, and in particular event structures, have been introduced in the 1980s as an alternative to operational interleaving semantics of concurrency, and nowadays they are regaining popularity. Event structures represent the causal dependency and conflict between the individual atomic actions of the system directly. This property leads to a more compact and concise representation of semantics. In this work-in-progress report, we present a theory of event structures mechanized in the COQ proof assistant and demonstrate how it can be applied to define certified executable semantics of a simple parallel register machine with shared memory.

Sign in / Sign up

Export Citation Format

Share Document