Hyperproperties are system properties that relate multiple traces (executions) of a system. Typical applications of hyperproperties are found in information flow security. In a previous paper, we introduced concurrent hyperproperties, by generalizing traces to concurrent traces, defined as partially ordered multisets. We take Petri nets as the basic semantic model. To check concurrent hyperproperties, we extended the testing of processes due to De Nicola and Hennessy to the setting of concurrent traces, using the parallel composition of Petri nets. In this paper, we present new results on decidability and undecidability of may and must testing of universal and existential concurrent hyperproperties, and analyze the case of concurrent hyperproperties with quantifier alternation.

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

Concurrent \(\forall \exists \) -Hyperproperties

  • Bernd Finkbeiner,
  • Ernst-Rüdiger Olderog

摘要

Hyperproperties are system properties that relate multiple traces (executions) of a system. Typical applications of hyperproperties are found in information flow security. In a previous paper, we introduced concurrent hyperproperties, by generalizing traces to concurrent traces, defined as partially ordered multisets. We take Petri nets as the basic semantic model. To check concurrent hyperproperties, we extended the testing of processes due to De Nicola and Hennessy to the setting of concurrent traces, using the parallel composition of Petri nets. In this paper, we present new results on decidability and undecidability of may and must testing of universal and existential concurrent hyperproperties, and analyze the case of concurrent hyperproperties with quantifier alternation.