240 research outputs found
Precongruence Formats with Lookahead through Modal Decomposition
Full text linkBloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder
Failure Trace Semantics for a Process Algebra with Time-outs
Full text linkThis paper extends a standard process algebra with a time-out operator, thereby increasing its absolute expressiveness, while remaining within the realm of untimed process algebra, in the sense that the progress of time is not quantified. Trace and failures equivalence fail to be congruences for this operator; their congruence closure is characterised as failure trace equivalence.<br/
Is Speed-Independent Mutual Exclusion Implementable? (Invited Talk)
Full text linkA mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker's, Peterson's and Lamport's bakery are meant to be speed independent.
In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending on how we believe reading and writing to a memory location is really carried out. It can be implemented on electrical circuits, however.
This builds on previous work showing that mutual exclusion cannot be accurately modelled in standard process algebras
Reactive Bisimulation Semantics for a Process Algebra with Time-Outs
Full text linkThis paper introduces the counterpart of strong bisimilarity for labelled
transition systems extended with time-out transitions. It supports this concept
through a modal characterisation, congruence results for a standard process
algebra with recursion, and a complete axiomatisation.Comment: An extended abstract of this paper appears in the proceedings of
CONCUR 202
LIPIcs, Volume 140, CONCUR'19, Complete Volume
No full textLIPIcs, Volume 140, CONCUR'19, Complete Volum
Front Matter, Table of Contents, Preface, Conference Organization
Full text linkFront Matter, Table of Contents, Preface, Conference Organizatio
Full Abstraction in Structural Operational Semantics (Extended Abstract)
No full textion in Structural Operational Semantics (extended abstract) Rob van Glabbeek Computer Science Department, Stanford University Stanford, CA 94305, USA [email protected] Abstract This paper explores the connection between semantic equivalences for concrete sequential processes, represented by means of transition systems, and formats of transition system specifications using Plotkin's structural approach. For several equivalences in the linear time -- branching time spectrum a format is given, as general as possible, such that this equivalence is a congruence for all operators specifiable in that format. And for several formats it is determined what is the coarsest congruence with respect to all operators in this format that is finer than partial or completed trace equivalence. 1 Preorders and equivalences on labelled transition systems Definition 1 A labelled transition system (LTS) is a pair (IP; \Gamma!) with IP a set (of processes) and \Gamma!` IP \Theta A \Theta IP for A a se..
Enabling Preserving Bisimulation Equivalence
Full text linkMost fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition
Branching bisimilarity for processes with time-outs
Full text linkThis paper provides an adaptation of branching bisimilarity to reactive systems with time-outs. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process algebra with recursion. The last section presents a complete axiomatisation for guarded processes without infinite sequences of unobservable actions
- …
