Deciding branching hyperproperties for real time systems
<|reference_start|>Deciding branching hyperproperties for real time systems: Security properties of real-time systems often involve reasoning about hyper-properties, as opposed to properties of single executions or trees of executions. These hyper-properties need to additionally be expressive enough to reason about real-time constraints. Examples of such properties include information flow, side channel attacks and service-level agreements. In this paper we study computational problems related to a branching-time, hyper-property extension of metric temporal logic (MTL) that we call HCMTL*. We consider both the interval-based and point-based semantics of this logic. The verification problem that we consider is to determine if a given HCMTL* formula $\varphi$ is true in a system represented by a timed automaton. We show that this problem is undecidable. We then show that the verification problem is decidable if we consider executions upto a fixed time horizon $T$. Our decidability result relies on reducing the verification problem to the truth of an MSO formula over reals with a bounded time interval.<|reference_end|>
@article{deka2024deciding,
    title={Deciding branching hyperproperties for real time systems},
    author={Nabarun Deka, Minjian Zhang, Rohit Chadha, and Mahesh Viswanathan},
    journal={arXiv preprint arXiv:2405.12104},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.12104},
    primaryClass={cs.CR cs.LO}
}