César Sánchez

Hyperproperties are a modern specification paradigm that extends properties of a single trace to express properties of a set of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a decidable model checking problem. In this paper, we introduce two asynchronous and orthogonal extensions of HyperLTL, Stuttering HyperLTL (HyperLTL _S ) and Context HyperLTL (HyperLTL _C ). Both of these extensions are useful, for instance, to formulate asynchronous variants of information-flow security properties. We show that for these logics, model checking is in general undecidable. On the positive side, for each of them, we identify a fragment with a decidable model checking problem that subsumes HyperLTL and that can express meaningful asynchronous requirements. Moreover, we provide the exact computational complexity of model checking for these two fragments which, for the (HyperLTL _S ) fragment, coincides with that of the strictly less expressive logic HyperLTL.

Quantum Communications promise advances in cryptography, quantum computing and clock synchronisation, among other emerging applications. However, communication based on quantum phenomena requires an extreme level of isolation from external disturbances, complicating the co-propagation of quantum and classical signals. The challenge is greater when deploying networks that are both heterogeneous (e.g., multiple vendors) and installed in production facilities, given that this type of infrastructure already supports networks loaded with their own requirements. Moreover, to achieve a broad acceptance among network operators, the joint management and operation of quantum and classical resources, compliance with standards, and legal and quality assurance need to be addressed. This article presents solutions to the aforementioned challenges validated in the Madrid quantum network during the implementation of the projects CiViC and OpenQKD. This network was designed to integrate quantum communications in the telecommunications ecosystem by installing quantum-key-distribution modules from multiple providers in production nodes of two different operators. The modules were connected through an optically-switched network with more than 130 km of deployed optical fibre. The tests were done in compliance with strict service level agreements that protected the legacy traffic of the pre-existing classical network. The goal was to ensure full quantum-classical interoperability at all levels, while limiting the modifications to optical transport and encryption and complying with relevant standards. This effort is intended to lay the foundation for large-scale quantum network deployments.