Concurrent $$\forall \exists $$-Hyperproperties

Abstract 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.