Trace properties, which are sets of execution traces, are often used to analyze systems, but their expressiveness is limited. Clarkson and Schneider defined hyperproperties as a generalization of trace properties to sets of sets of traces. Typical applications of hyperproperties are found in information flow security. We introduce an analogous definition of concurrent hyperproperties, by generalizing traces to concurrent traces, which we define as partially ordered multisets. We take Petri nets as the basic semantic model. Concurrent traces are formalized via causal nets. To check concurrent hyperproperties, we define may and must testing of sets of concurrent traces in the style of DeNicola and Hennessy, using the parallel composition of Petri nets. In our approach, we thus distinguish nondeterministic and concurrent behavior. We discuss examples where concurrent hyperproperties are needed.

翻译：迹属性（即执行迹的集合）常用于分析系统，但其表达能力有限。Clarkson和Schneider将超属性定义为迹属性的泛化形式，即迹的集合的集合。超属性在信息流安全领域具有典型应用。本文通过将迹泛化为并发迹（定义为偏序多重集），引入并发超属性的对应定义。我们采用Petri网作为基本语义模型，并通过因果网对并发迹进行形式化。为检验并发超属性，借鉴DeNicola和Hennessy的方法，利用Petri网并行组合定义迹集合的may测试与must测试。由此，我们的方法能够区分非确定行为与并发行为。最后讨论需要并发超属性的典型示例。