English

Concurrent Hyperproperties

Logic in Computer Science 2023-10-03 v1

Abstract

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.

Keywords

Cite

@article{arxiv.2310.00705,
  title  = {Concurrent Hyperproperties},
  author = {Bernd Finkbeiner and Ernst-Rüdiger Olderog},
  journal= {arXiv preprint arXiv:2310.00705},
  year   = {2023}
}

Comments

Theories of Programming and Formal Methods 2023