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.

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 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 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 Baby Modula-3 and a theory of objects

1994 ◽  
Vol 4 (2) ◽  
pp. 249-283 ◽  
Author(s):  
Martin Abadi
Keyword(s):  
Programming Language ◽  
Formal Semantics ◽  
Operational Semantics ◽  
Object Oriented ◽  
Denotational Semantics ◽  
Object Oriented Programming ◽  
The Core ◽  
Functional Object ◽  
Oriented Programming Language

AbstractBaby Modula-3 is a small, functional, object-oriented programming language. It is intended as a vehicle for explaining the core of Modula-3 from a biased perspective: Baby Modula-3 includes the main features of Modula-3 related to objects, but not much else. To the theoretician, Baby Modula-3 provides a tractable, concrete example of an object-oriented language, and we use it to study the formal semantics of objects. Baby Modula-3 is defined with a structured operational semantics and with a set of static type rules. A denotational semantics guarantees the soundness of this definition.

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 A Denotational Semantics af Inheritance and its Correctness

1989 ◽  
Vol 18 (284) ◽  
Author(s):  
William Cook ◽  
Jens Palsberg
Keyword(s):  
Operational Semantics ◽  
Object Oriented ◽  
Denotational Semantics ◽  
General Mechanism ◽  
Recursive Definition ◽  
Object Oriented Languages

This paper presents a denotational model of inheritance. The model is based on an inituitive motivation of the purpose of inheritance. The correctness of the model is demonstrated by proving it equivalent to an operational semantics of inheritance based upon the methodlookup algorithm of object-oriented languages. Although it was originally developed to explain inheritance in object-oriented languages, the model shows that in heritance is a general mechanism that may be applied to any form of recursive definition.

scholarly journals Semantics, Modularity, and Rewriting Logic

1998 ◽  
Vol 5 (42) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Operational Semantics ◽  
Denotational Semantics ◽  
Rewriting Logic ◽  
Semantic Description ◽  
Semantic Framework ◽  
Action Semantics ◽  
Strong Indicator ◽  
Hybrid Framework ◽  
Structural Operational Semantics ◽  
Modular Monadic Semantics

A complete formal semantic description of a practical programming language (such as Java) is likely to be a lengthy document, regardless of which semantic framework is being used. Good modularity of the description is important to the person(s) developing it, to facilitate reuse, change, and extension. Unfortunately, the conventional versions<br />of the major semantic frameworks have rather poor modularity.<br /> In this paper, we first recall some approaches that improve the modularity of denotational semantics, namely action semantics, modular monadic semantics, and a hybrid framework that combines these: modular monadic action semantics. We then address the issue of modularity in operational semantics, which appears to have received comparatively little attention so far, and report on some preliminary investigations of how one might achieve the same kind of modularity in structural operational semantics as the use of monad transformers<br />can provide in denotational semantics|this is the main technical contribution of the paper. Finally, we briefly consider the representation of structural operational semantics in rewriting logic, and speculate on the possibility of using it to interpret programs in the described language. Providing powerful meta-tools for such semantics-based interpretation<br />is an interesting potential application of rewriting logic;<br />good modularity of the semantic descriptions may be crucial for the practicality of using the tools.<br />Much of the paper consists of (very) simple examples of semantic descriptions in the various frameworks, illustrating the degree of reformulation needed when extending the described language|a strong indicator of modularity. Throughout, it is assumed that the reader has some familiarity with the concepts and notation of denotational and structural operational semantics. Familiarity with the basic notions of monads and monad transformers is not a prerequisite.

Sign in / Sign up

Export Citation Format

Share Document