A logic of behaviour in context

C. J. Banks*, I. Stark

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

We present a novel temporal logic for expressing properties of behaviour in context. The logic is applied to models of continuous processes, specifically using the continuous π-calculus as a modelling language for biochemical systems. The logic allows the expression of the temporal behaviour of a system when placed in the context of another system. Here we study this in terms of biochemical reactions and the expression of temporal behaviour in the context of other biochemical processes. We present the syntax and semantics of the logic and study the model-checking problem over continuous time and continuous state-space process models, using the continuous π-calculus. We present a succinct, but naive, model-checking algorithm and then show how this can be improved. We investigate the complexity of model-checking, where repeated ODE solving emerges as a particular cost; assess some limitations of the technique; and identify potential routes to overcome these.
Original languageEnglish
Pages (from-to)3-18
Number of pages16
JournalInformation and Computation
Publication statusPublished - 1 Jan 2014


Dive into the research topics of 'A logic of behaviour in context'. Together they form a unique fingerprint.

Cite this