Processes with infinite liveness requirementsby Hélia Guerra, José Félix Costa

The Journal of Logic and Algebraic Programming

About

Year
2013
DOI
10.1016/j.jlap.2013.03.001
Subject
Computational Theory and Mathematics / Software / Logic / Theoretical Computer Science

Similar

Text

The Journal of Logic and Algebraic Programming 82 (2013) 137–161

Contents lists available at SciVerse ScienceDirect

The Journal of Logic and Algebraic Programming j ou rna l homepage : www . e l s e v i e r . c om / l o c a t e / j l a p

Processes with infinite liveness requirements

Hélia Guerra a,∗, José Félix Costa b,c,1 a

Centre for Applied Mathematics and Information Technologies, Department of Mathematics, University of Azores, R. Mãe de Deus, 9501-801 Ponta Delgada, Portugal b

Department of Mathematics, Instituto Superior Técnico, Technical University of Lisbon, Av. Rovisco Pais, 1049-001 Lisboa, Portugal c

Centro de Matemática e Aplicações Fundamentais, University of Lisbon, Lisboa, Portugal

A R T I C L E I N F O A B S T R A C T

Article history:

Available online 27 March 2013

Keywords:

Process algebra

Liveness

Denotational semantics

Operational semantics

In this paper we develop a deterministic process algebra for describing and reasoning about liveness requirements of infinite behaviour systems beyond the ones usually captured by non-deterministic process models. These liveness requirements refer to the capability of processes to engage spontaneously in some actions and to wait passively for the triggering of other actions by other processes. A semantic theory based on three equivalent semantic domains (denotational, operational, and axiomatic) is developed for the language of process terms. © 2013 Elsevier Inc. All rights reserved. 1. Introduction 1.1. The QS and ωQS models

The deterministic Quiescence Model (QSmodel) introduced in [5,6] and later extended in [10], captures liveness properties, commonly specified in Temporal Logic, but not fully captured by non-deterministic process models (e.g., input/output systems of Jonsson [14,15], failure extensions for the CSP language [26,31], and the input/output automata of Lynch [17,18]).

The idea of quiescence, due to Chandy andMisra [23,24,22], was developed by Jonsson [14,15] in the context of a logic to reason about specifications of input/output systems, and also by Sernadas, Ehrich, and Costa in [32,4,5,6] within an algebraic framework, in order to provide a solution for the problem of representing state-dependent liveness as a process.

The model is able to describe liveness requirements concerning the capability of processes to engage spontaneously in some actions and to wait passively for the triggering of other actions by other processes. These liveness requirements are described by including two distinct prefixing operators in the process language: active and passive prefixing. The passive prefixing operator is the standard prefixing operator used inwell-knownprocess algebras (e.g., CSP [31]). The active prefixing operator is a kind of strong prefixing in the sense that the correspondent action must occur. It is related to the strong prefixing introduced in [9] for extending CCS with atomic actions but not used to explain transactional behaviour. With this new prefixing operator it is also possible to look at processes with transactions as QS processes with a special liveness requirement of the type “reach the end!”.

The basic idea of QS model has thrown away the traditional prefix-closure assumption in the classical trace semantic models, such as [12,31,3]. The behaviour of each process term is captured by a (finite or infinite) set of its quiescent finite traces (finite sequences of actions). According to the model, a quiescent trace of a process is the trace obtained in a state after which there is no commitment for the process to perform any further action. According to the QS model, a process (or a process community) is represented by the set of its quiescent traces, i.e., the set of traces obtained in a state after that there is no commitment for the process to perform any further action. The degree of liveness associated to a process is put in relation with the departure of its quiescent set from being prefix-closed. Two QS processes with the same prefix-closure ∗ Corresponding author. Tel.: +351 296 650509; fax: +351 296 650072.

E-mail addresses: helia@uac.pt (H. Guerra), fgc@math.ist.utl.pt (J.F. Costa). 1 The research of José Félix Costa is supported by Fundação para a Ciência e Tecnologia, PEst – OE/MAT/UI0209/2011. 1567-8326/$ - see front matter © 2013 Elsevier Inc. All rights reserved. http://dx.doi.org/10.1016/j.jlap.2013.03.001 138 H. Guerra, J.F. Costa / Journal of Logic and Algebraic Programming 82 (2013) 137–161 can be comparable with respect to liveness: the smaller number of quiescent traces corresponds to the higher degree of liveness. Moreover, a trace of a QS process community is quiescent iff it can be projected onto a quiescent trace of every one of its components, because the whole community is in a quiescent state iff all its components are in a quiescent state.

Consider the following QS process example, inspired by the well-known Hoare’s vending-machine in [12], appealing to the liveness differences just described by the active and the passive prefixing. Let the process term in a CSP notation [12]

ActiveMachine = μx.coin.(!coffee.x+!tea.x), describe the behaviour of a vending-machine that repeatedly provides either coffee or tea after receiving a coin from a customer. The customer takes the initiative to insert the coinwhereas the vending-machine waits passively for it. Moreover, the vending-machine takes the initiative to provide coffee or tea, after the insertion of a coin whereas the customer waits passively for coffee or tea. The ! in coffee and tea indicates that after coin the process is in a non-quiescent state, willing to perform either coffee or tea. The set of traces for ActiveMachine is the non prefix-closed regular language (coin coffee + coin tea)∗.

In general, we may want to impose infinite liveness requirements, such as the non-stop clock process described by the process term

Clock = μx.!tick.x, that has the recursive commitment of ticking. However, there is no trace in {tick}∗ afterwhich the clock is in a quiescent state.