Alban Ponse

TCS Journal 2011 Journal Article

Preface

• Inge Bethke
• Alban Ponse
• Piet H. Rodenburg

TCS Journal 2007 Journal Article

Belnap’s logic and conditional composition

• Alban Ponse
• Mark B. van der Zwaag

We study two alternative bases for Belnap’s four-valued logic and provide complete equational axiomatizations for them. One is called conditional composition logic. It has a single, ternary if-then-else connective with a sequential, operational reading, and four constants for the truth values. The other logic is called guard logic. The main motivation for this logic lies in its technical properties. It admits a useful type of canonical form (term representation), and a relatively simple strategy for equational reasoning.

TCS Journal 2003 Journal Article

Branching time and orthogonal bisimulation equivalence

• Jan A. Bergstra
• Alban Ponse
• Mark B. van der Zwaag

We propose a refinement of branching bisimulation equivalence that we call orthogonal bisimulation equivalence. Typically, internal activity (the performance of τ-steps) may be compressed, but not completely discarded. Hence, a process with τ-steps cannot be equivalent to one without τ-steps. Also, we present a modal characterization of orthogonal bisimulation equivalence. This equivalence is a congruence for ACP extended with abstraction and priority operators. We provide a complete axiomatization, and describe some expressiveness results. Finally, we present the verification of a PAR protocol that is specified with use of priorities.

TCS Journal 2001 Journal Article

Non-regular iterators in process algebra

• Jan A. Bergstra
• Alban Ponse

We consider three forms of non-regular iteration in process algebra: the push-down operation $, defined by x$y=x((x$y)(x$y))+y, the nesting operation ♯, defined by x ♯ y=x((x ♯ y)x)+y, and the back and forth operation ⇆, defined by x ⇆ y=x((x ⇆ y)y)+y. In the process algebraic framework ACP with abstraction and one of $, ♯ or ⇆ we provide definitions of the following standard processes: stack, context-free process, bag, and queue. These definitions apply to all standard behavioural equivalences (we only use xτ=x, where τ is the silent step). Moreover, these results yield the expressive power to express computable processes modulo rooted branching bisimulation equivalence, and hence support the equational founding of process algebra: standard processes can be represented as terms.

TCS Journal 1997 Journal Article

Preface

• Alban Ponse
• Chris Verhoef
• Bas van Vlijmen

TCS Journal 1997 Journal Article

Two finite specifications of a queue

• Marc Bezem
• Alban Ponse

It is known that a queue is not finitely definable in ACP with handshaking communication (Baeten and Bergstra, 1988). In this paper, two finite specifications of a queue in ACP with abstraction and handshaking are proved correct relative to a standard specification of a queue that employs an infinite data type for representing its contents. The proofs are given in the proof theory of μCRL, and the only ‘τ-laws’ used are xτ = x and x(τ(y + z) + y) = x(y + z). Therefore the proofs are adequate for both ‘branching bisimilarity’ and ‘observation equivalence’. Additionally, it is shown that standard concurrency follows from RSP for a class of processes guardedly specifiable in ACP with abstraction.

CSL Conference 1994 Conference Paper

Process Algebra with Combinators

• Jan A. Bergstra
• Inge Bethke
• Alban Ponse

Abstract We introduce typed combinatory process algebra, a system combining process algebra with types and combinators. We describe its syntax and semantics, and by way of example, verify within this frame-work the Simple Alternating Bit Protocol.

I&C Journal 1991 Journal Article

Process expressions and Hoare's logic: Showing an irreconcilability of context-free recursion with Scott's induction rule

• Alban Ponse

In this paper processes specifiable over a non-uniform language are considered. The language contains constants for a set of atomic actions and constructs for alternative and sequential composition. Furthermore it provides a mechanism for specifying processes recursively (including nested recursion). We consider processes as having a state: atomic actions are to be specified in terms of observable behaviour (relative to initial states) and state transformations. Any process having some initial state can be associated with a transition system representing all possible courses of execution. This leads to an operational semantics in the style of Plotkin. The partial correctness assertion {α} p{β} expresses that for any transition system associated with the process p and having some initial state satisfying α, its final states representing successful execution satisfy β. A logic in the style of Hoare, containing a proof system for deriving partial correctness assertions, is presented. This proof system is sound and relatively complete, so any partial correctness assertion can be evaluated by investigating its derivability. Included is a short discussion about the extension of the process language with “guarded recursion”. It appears that such an extension violates the completeness of the Hoare logic. This reveals a remarkable property of Scott's induction rule in the context of non-determinism: only regular recursion allows a completeness result.