A More Sensitive Context

TL;DR

This paper introduces an improved method for model-checking continuous-state processes using a spatio-temporal logic with context, leveraging signal temporal logic and sensitivity analysis for efficiency and reliability.

Contribution

It advances LBC model-checking by integrating signal temporal logic and sensitivity analysis to reduce computational cost and improve intermediate value checking.

Findings

Boolean signals enable more efficient trace compression

Sensitivity analysis reduces the number of sample trajectories needed

The new approach improves model-checking performance for continuous processes

Abstract

Logic of Behaviour in Context (LBC) is a spatio-temporal logic for expressing properties of continuous-state processes, such as biochemical reaction networks. LBC builds on the existing Metric Interval Temporal Logic (MITL) and adds a "context modality" that explores the behaviour of a system when composed with an external process. LBC models are terms of the Continuous {\pi}-Calculus (c{\pi}), a process algebra with continuous state space. Our previously published LBC model-checking technique required examining many points along the behavioural trajectory of a process; and potentially computing further trajectories branching off at every such point. This raised two difficulties: mixing temporal and spatial modalities could require computing a large number of trajectories, with costly numerical solution of differential equations; and might still fail to check intermediate values between discrete points on those trajectories. In this paper we make progress against both of these problems using techniques from signal temporal logic and from sensitivity analysis. Boolean signals aggressively compress trace information, allowing more efficient computation; and sensitivity analysis lets us reliably check formulae over a region by calculating a smaller number of sample trajectories.