Quantitative testing semantics for non interleaving Emmanuel Beffara

icon

21

pages

icon

English

icon

Documents

Écrit par

Publié par

Lire un extrait
Lire un extrait
icon

21

pages

icon

English

icon

Ebook

Lire un extrait
Lire un extrait
Quantitative testing semantics for non-interleaving Emmanuel Beffara? IML, CNRS & Université Aix-Marseille II April 15, 2009 Abstract. This paper presents a non-interleaving denotational semantics for the pi-calculus. The basic idea is to define a notion of test where the outcome is not only whether a given process passes a given test, but also in how many different ways it can pass it. More abstractly, the set of possible outcomes for tests forms a semiring, and the set of process interpretations appears as a module over this semiring, in which basic syntactic constructs are affine operators. This notion of test leads to a trace semantics in which traces are partial orders, in the style of Mazurkiewicz traces, extended with readiness information. Our construction has standard may- and must-testing as special cases. 1 Introduction The theory of concurrency has developed several very different models for processes, focusing on different aspects of computation. Process calculi are an appealing framework for describing and analyzing concurrent systems, because the formal language approach is well suited to modular reasoning, allowing to study sophisticated systems by means of abstract programming primitives for which powerful theoretical tools can be developed. However, the vast majority of the semantic studies on process calculi like the pi-calculus have focused on the so-called interleaving operational semantics, which is the basic definition of the dynamic of a process: the interaction of a program with its environment is reduced to possible sequences of transitions, thus considering that parallel composition of program components is merely an abstraction that represents all possible ways of

  • proved transitions

  • processes include

  • can pass

  • transition labels

  • congruence ≈

  • probably has

  • recursive processes

  • ab ≈ ba

  • semantics


Voir icon arrow

Publié par

Nombre de lectures

29

Langue

English

Alternate Text