Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes

要約

タイトル：ストキャスティックプロセスのSTL要件に対するコンホーマル量的予測モニタリング

要約：
– ランタイムでシステムの状態から望ましいプロパティの満足度を予測するプレディクティブモニタリング（PM）の問題を考慮する。
– ランタイムでの安全保証とオンライン制御にとって重要であるため、PMメソッドは時間の経過に応じた違反に対するタイムリーな介入を可能にするために効率的である必要があり、同時に正しさの保証を提供する必要がある。
– \ textit {量的予測モニタリング（QPM）}を紹介する。これは、シグナル一時論理（STL）で与えられた富豪的仕様をサポートする最初のPMメソッドである。既存のPM技術のほとんどが、あるプロパティ$\phi$が満足されているかどうかを予測するのに対して、QPMは$\phi$の量的（ロバスト）STL意味を予測する量的な措置を提供する。
– QPMは、システムの確率的進化に対してのSTLロバストネス値を任意の確率でカバーするような予測区間を導出する。これにより、ランタイムでのMonte-Carloシミュレーションによる区間の評価を回避し、コンフォーマル推論による量子回帰の最近の進歩を活用する機械学習アプローチを採用している。
– また、再トレーニングの必要性なしにコンポジット式を処理するために、監視機を合成する方法も示しており、保証を犠牲にすることなく、QPMの効果とスケーラビリティを、複雑さの異なる4つの離散時間のストキャスティックプロセスのベンチマークで示している。

要約(オリジナル)

We consider the problem of predictive monitoring (PM), i.e., predicting at runtime the satisfaction of a desired property from the current system’s state. Due to its relevance for runtime safety assurance and online control, PM methods need to be efficient to enable timely interventions against predicted violations, while providing correctness guarantees. We introduce \textit{quantitative predictive monitoring (QPM)}, the first PM method to support stochastic processes and rich specifications given in Signal Temporal Logic (STL). Unlike most of the existing PM techniques that predict whether or not some property $\phi$ is satisfied, QPM provides a quantitative measure of satisfaction by predicting the quantitative (aka robust) STL semantics of $\phi$. QPM derives prediction intervals that are highly efficient to compute and with probabilistic guarantees, in that the intervals cover with arbitrary probability the STL robustness values relative to the stochastic evolution of the system. To do so, we take a machine-learning approach and leverage recent advances in conformal inference for quantile regression, thereby avoiding expensive Monte-Carlo simulations at runtime to estimate the intervals. We also show how our monitors can be combined in a compositional manner to handle composite formulas, without retraining the predictors nor sacrificing the guarantees. We demonstrate the effectiveness and scalability of QPM over a benchmark of four discrete-time stochastic processes with varying degrees of complexity.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI