更敏感的背景

摘要：

上下文行为逻辑（Logic of Behaviour in Context，LBC）是一种时空逻辑，用于表达连续状态过程的属性，如生化反应网络。LBC建立在现有的度量间隔时态逻辑（MITL）的基础上，并增加了一个“上下文模态”，探索系统与外部过程组成时的行为。LBC模型是连续π-演算（cπ）的术语，连续π-演算是一种具有连续状态空间的过程代数。我们以前发表的LBC模型检查技术需要检查过程行为轨迹上的许多点;并可能计算在每个这样的点上分支的进一步轨迹。这引起了两个困难：混合时间和空间模态可能需要计算大量的轨迹，其中微分方程的数值解是昂贵的;并且可能仍然不能检查这些轨迹上的离散点之间的中间值。在本文中，我们取得了进展，对这两个问题使用技术从信号时序逻辑和灵敏度分析。布尔信号积极地压缩轨迹信息，允许更有效的计算;灵敏度分析使我们能够通过计算较少数量的样本轨迹来可靠地检查区域上的公式。

英文摘要：

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 π-Calculus (cπ), 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.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。