Finitely Branching Labelled Transition Systems from Reaction Semantics for Process Calculi

2009 ◽  
pp. 119-134 ◽  
Author(s):  
Pietro Di Gianantonio ◽  
Furio Honsell ◽  
Marina Lenisa
Keyword(s):  
Transition Systems ◽  
Labelled Transition Systems ◽  
Process Calculi

scholarly journals RPO semantics for mobile ambients

2014 ◽  
Vol 24 (4) ◽  
Author(s):  
FILIPPO BONCHI ◽  
FABIO GADDUCCI ◽  
GIACOMA VALENTINA MONREALE
Keyword(s):  
Operational Semantics ◽  
Inference Rules ◽  
Synthesis Mechanism ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Process Calculi ◽  
Mobile Ambients

In this paper we focus on the synthesis of labelled transition systems (LTSs) for process calculi using Mobile Ambients (MAs) as a testbed. Our proposal is based on a graphical encoding: a process is mapped into a graph equipped with interfaces such that the denotation is fully abstract with respect to the standard structural congruence. Graphs with interfaces are amenable to the synthesis mechanism based on borrowed contexts (BCs), which is an instance of relative pushouts (RPOs). The BC mechanism allows the effective construction of an LTS that has graphs with interfaces as states and labels, and such that the associated bisimilarity is a congruence. We focus here on the analysis of an LTS over processes as graphs with interfaces: we use the LTS on graphs to recover an LTS directly defined over the structure of MA processes and define a set of SOS inference rules capturing the same operational semantics.

scholarly journals Natural Quantum Operational Semantics with Predicates

2008 ◽  
Vol 18 (3) ◽  
pp. 341-359 ◽  
Author(s):  
Marek Sawerwain ◽  
Roman Gielerak
Keyword(s):  
Positive Operator ◽  
Operational Semantics ◽  
General Definition ◽  
Completely Positive Maps ◽  
Transition Systems ◽  
Positive Operator Valued Measures ◽  
Labelled Transition Systems ◽  
Positive Maps ◽  
Definition Of ◽  
Positive Operator Valued Measure

Natural Quantum Operational Semantics with PredicatesA general definition of a quantum predicate and quantum labelled transition systems for finite quantum computation systems is presented. The notion of a quantum predicate as a positive operator-valued measure is developed. The main results of this paper are a theorem about the existence of generalised predicates for quantum programs defined as completely positive maps and a theorem about the existence of a GSOS format for quantum labelled transition systems. The first theorem is a slight generalisation of D'Hondt and Panagaden's theorem about the quantum weakest precondition in terms of discrete support positive operator-valued measures.

scholarly journals Model Checking Coloured Petri Nets - Exploiting Strongly Connected Components

1997 ◽  
Vol 26 (519) ◽  
Author(s):  
Allan Cheng ◽  
Søren Christensen ◽  
Kjeld Høyer Mortensen
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
The State ◽  
Connected Components ◽  
Coloured Petri Nets ◽  
Transition Systems ◽  
Strongly Connected Components ◽  
State Spaces ◽  
Labelled Transition Systems ◽  
Strongly Connected

In this paper we present a CTL-like logic which is interpreted over the state spaces of Coloured Petri Nets. The logic has been designed to express properties of both state and transition information. This is possible because the state spaces are labelled transition systems. We compare the expressiveness of our logic with CTL's. Then, we present a model checking algorithm which for efficiency reasons utilises strongly connected components and formula reduction rules. We present empirical results for non-trivial examples and compare the performance of our algorithm with that of Clarke, Emerson, and Sistla.

Sign in / Sign up

Export Citation Format

Share Document