Domain equations for probabilistic processes

2000 ◽  
Vol 10 (6) ◽  
pp. 665-717 ◽  
Author(s):  
CHRISTEL BAIER ◽  
MARTA KWIATKOWSKA
Keyword(s):  
Metric Spaces ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Semantic Model ◽  
Transition Systems ◽  
Probabilistic Choice ◽  
Bisimulation Equivalence ◽  
Metric Semantics ◽  
Continuous Domains ◽  
Probabilistic Processes

In this paper we consider Milner's calculus CCS enriched by a probabilistic choice operator. The calculus is given operational semantics based on probabilistic transition systems. We define operational notions of preorder and equivalence as probabilistic extensions of the simulation preorder and the bisimulation equivalence respectively. We extend existing category-theoretic techniques for solving domain equations to the probabilistic case and give two denotational semantics for the calculus. The first, ‘smooth’, semantic model arises as a solution of a domain equation involving the probabilistic powerdomain and solved in the category CONT⊥ of continuous domains. The second model also involves an appropriately restricted probabilistic powerdomain, but is constructed in the category CUM of complete ultra-metric spaces, and hence is necessarily ‘discrete’. We show that the domain-theoretic semantics is fully abstract with respect to the simulation preorder, and that the metric semantics is fully abstract with respect to bisimulation.

scholarly journals On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces

1998 ◽  
Vol 8 (5) ◽  
pp. 481-540 ◽  
Author(s):  
DANIELE TURI ◽  
JAN RUTTEN
Keyword(s):  
Computer Science ◽  
Mathematical Theory ◽  
Metric Spaces ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Partial Orders ◽  
Present Survey ◽  
Induction Principle ◽  
Structural Operational Semantics ◽  
Modern Mathematics

This paper, a revised version of Rutten and Turi (1993), is part of a programme aiming at formulating a mathematical theory of structural operational semantics to complement the established theory of domains and denotational semantics to form a coherent whole (Turi 1996; Turi and Plotkin 1997). The programme is based on a suitable interplay between the induction principle, which pervades modern mathematics, and a dual, non-standard ‘coinduction principle’, which underlies many of the recursive phenomena occurring in computer science.The aim of the present survey is to show that the elementary categorical notion of a final coalgebra is a suitable foundation for such a coinduction principle. The properties of coalgebraic coinduction are studied both at an abstract categorical level and in some specific categories used in semantics, namely categories of non-well-founded sets, partial orders and metric spaces.

scholarly journals A Fully Abstract Presheaf Semantics of SCCS with Finite Delay

1999 ◽  
Vol 6 (28) ◽  
Author(s):  
Thomas Troels Hildebrandt
Keyword(s):  
Operational Semantics ◽  
Denotational Semantics ◽  
Transition Systems ◽  
Finite Delay ◽  
Open Map ◽  
Special Case

We present a presheaf model for the observation of infinite as well<br />as finite computations. We apply it to give a denotational semantics of<br />SCCS with finite delay, in which the meanings of recursion are given by<br />final coalgebras and meanings of finite delay by initial algebras of the<br />process equations for delay. This can be viewed as a first step in representing<br />fairness in presheaf semantics. We give a concrete representation<br />of the presheaf model as a category of generalised synchronisation<br />trees and show that it is coreflective in a category of generalised transition<br />systems, which are a special case of the general transition systems<br />of Hennessy and Stirling. The open map bisimulation is shown to coincide<br />with the extended bisimulation of Hennessy and Stirling. Finally<br />we formulate Milners operational semantics of SCCS with finite delay<br />in terms of generalised transition systems and prove that the presheaf<br />semantics is fully abstract with respect to extended bisimulation.

scholarly journals Processes as terms: non-well-founded models for bisimulation

1992 ◽  
Vol 2 (3) ◽  
pp. 257-275 ◽  
Author(s):  
J. J. M. M. Rutten
Keyword(s):  
Set Theory ◽  
Metric Spaces ◽  
Operational Semantics ◽  
Transition System ◽  
Recursive Equation ◽  
Compositional Semantics ◽  
Complete Metric Spaces ◽  
Bisimulation Equivalence ◽  
Nonstandard Set Theory ◽  
Standard Set

A compositional semantics characterizing bisimulation equivalence is derived from transition system specifications in the SOS style, satisfying certain syntactic syntactic conditions. We use Aczel's nonstandard set theory for solving a recursive equation for a domain fo processes. It contains non-well-founded elements modelling possibly infinite behaviour. Semantic interpretations of syntactic operators are obtained by defining the operational semantics for terms consisting of both syntactic and semantic (processes)entities. Finally, we return to standard set theory by observing that a similar, though less general, result can be obtained with the use of complete metric spaces.

scholarly journals On the Action Semantics of Concurrent Programming Languages

1992 ◽  
Vol 21 (424) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Semantic Description ◽  
Paper Briefly ◽  
Action Semantics ◽  
Concurrent Programming Languages ◽  
Structural Operational Semantics ◽  
Bisimulation Equivalence ◽  
Basic Concepts

<p>Action semantics is a framework for semantic description of prograrnming languages. In this framework, actions are semantic entities, used to represent the potential behaviour of programs --- also the contributions that parts of programs make to such behaviour. The notation for expressing actions, called action notation, is combinator-based. It is used in much the same way that lambda-notation is used in denotational semantics. However, the essence of action notation is operational, rather than mathematical, and its meaning is formally defined by a structural operational semantics together with a bisimulation equivalence.</p><p>This paper briefly motivates action semantics, and explains the basic concepts. It then illustrates the use of the framework by giving an action semantic description of a small example language. This language includes a simple form of concurrency: tasks that may synchronize by means of rendezvous. The paper also discusses the operational semantics of action notation, focusing on the primitive actions that represent asynchronous message transmission and process initiation.</p>

scholarly journals A Presheaf Semantics of Value-Passing Processes

1996 ◽  
Vol 3 (44) ◽  
Author(s):  
Glynn Winskel
Keyword(s):  
Operational Semantics ◽  
Denotational Semantics ◽  
Domain Theory ◽  
Process Calculi ◽  
Traditional Definition ◽  
Open Maps

This paper investigates presheaf models for process calculi with<br />value passing. Denotational semantics in presheaf models are shown<br />to correspond to operational semantics in that bisimulation obtained<br />from open maps is proved to coincide with bisimulation as defined<br />traditionally from the operational semantics. Both "early" and "late"<br />semantics are considered, though the more interesting "late" semantics<br />is emphasised. A presheaf model and denotational semantics is proposed<br />for a language allowing process passing, though there remains<br />the problem of relating the notion of bisimulation obtained from open<br />maps to a more traditional definition from the operational semantics.<br />A tentative beginning is made of a "domain theory" supporting<br />presheaf models.

Service Discovery and Composition Based on Contracts and Choreographic Descriptions

2012 ◽  
pp. 60-88
Author(s):  
Mario Bravetti ◽  
Gianluigi Zavattaro
Keyword(s):  
Service Discovery ◽  
Operational Semantics ◽  
Asynchronous Communication ◽  
Synchronous Communication ◽  
Transition Systems ◽  
Service Contracts ◽  
Contract Compliance ◽  
Service Oriented ◽  
Labeled Transition System ◽  
Contract Language

The authors discuss the interplay between the notions of contract compliance, contract refinement, and choreography conformance in the context of service oriented computing, by considering both synchronous and asynchronous communication. Service contracts are specified in a language independent way by means of finite labeled transition systems. In this way, the theory is general and foundational as the authors abstract away from the syntax of contracts and simply assume that a contract language has an operational semantics defined in terms of a labeled transition system. The chapter makes a comparative analysis of synchronous and asynchronous communication. Concerning the latter, a realistic scenario is considered in which services are endowed with queues used to store the received messages. In the simpler context of synchronous communication, the authors are able to resort to the theory of fair testing to provide decidability results.

scholarly journals Approximate Analyzing of Labeled Transition Systems

2015 ◽  
Vol 2015 ◽  
pp. 1-9
Author(s):  
Qiong Yu ◽  
Shihan Yang ◽  
Jinzhao Wu
Keyword(s):  
Control Systems ◽  
Linear Systems ◽  
Matrix Decomposition ◽  
Transition System ◽  
Formal Semantic ◽  
Semantic Model ◽  
Transition Systems ◽  
State Space Explosion ◽  
Normal Circumstance ◽  
Time Linear

As the most important formal semantic model, labeled transition systems are widely used, which can describe the general concurrent systems or control systems without disturbance. However, under normal circumstance, transition systems are complex and difficult to use due to large amount of calculation and the state space explosion problems. In order to overcome these problems, approximate equivalent labeled transition systems are proposed by means of incomplete low-up matrix decomposition factorization. This technique can reduce the complexity of computation and calculate under the allowing errors. As for continuous-time linear systems, we develop a modeling method of approximated transition system based on the approximate solution of matrix, which provides a facility for approximately formal semantic modeling for linear systems and to effectively analyze errors. An example of application in the context of linear systems without disturbances is studied.

Sign in / Sign up

Export Citation Format

Share Document