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.
ABSTRACT
PUBLICATION RECORD
- Publication year
2014
- Venue
Information and Computation
- Publication date
2014-08-01
- Fields of study
Biology, Mathematics, Computer Science
- Identifiers
- External record
- Source metadata
Semantic Scholar
CITATION MAP
EXTRACTION MAP
CLAIMS
- No claims are published for this paper.
CONCEPTS
- No concepts are published for this paper.
REFERENCES
Showing 1-26 of 26 references · Page 1 of 1