Hyperproperties are properties of systems that relate more than one trace, which are common in information-flow, concurrency, symmetry, diagnosability, etc. Several temporal logics for hyperproperties have been proposed—like HyperLTL and HyperCTL* where traces are compared synchronously—and recently extended for comparing traces asynchronously. However, all these temporal hyperlogics are for infinite traces, in spite of the recent popularity of temporal logics on finite traces. In this paper, we introduce SC-HyperLTL, a logic for asynchronous hyperproperties on finite traces and with past operators, by adapting and combining two existing logics for asynchronous hyperproperties: stuttering HyperLTL ( \(\text {HyperLTL}_S\) ) and context HyperLTL ( \(\text {HyperLTL}_C\) ). We show that SC-HyperLTL is decidable and can encode many hyperproperties of interest. We present two practical algorithms that reduce the model checking problem of SC-HyperLTL to inputs of two existing tools: AutoHyper (which can model check hyperproperties on infinite traces) and nuXmv (a model checker for trace properties). We illustrate our algorithms on a prototype implementation.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

(Asynchronous) Temporal Logics for Hyperproperties on Finite Traces

  • Alberto Bombardelli,
  • Laura Bozzelli,
  • Cesar Sanchez,
  • Stefano Tonetta

摘要

Hyperproperties are properties of systems that relate more than one trace, which are common in information-flow, concurrency, symmetry, diagnosability, etc. Several temporal logics for hyperproperties have been proposed—like HyperLTL and HyperCTL* where traces are compared synchronously—and recently extended for comparing traces asynchronously. However, all these temporal hyperlogics are for infinite traces, in spite of the recent popularity of temporal logics on finite traces. In this paper, we introduce SC-HyperLTL, a logic for asynchronous hyperproperties on finite traces and with past operators, by adapting and combining two existing logics for asynchronous hyperproperties: stuttering HyperLTL ( \(\text {HyperLTL}_S\) ) and context HyperLTL ( \(\text {HyperLTL}_C\) ). We show that SC-HyperLTL is decidable and can encode many hyperproperties of interest. We present two practical algorithms that reduce the model checking problem of SC-HyperLTL to inputs of two existing tools: AutoHyper (which can model check hyperproperties on infinite traces) and nuXmv (a model checker for trace properties). We illustrate our algorithms on a prototype implementation.