اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدObservational Equivalence Using Schedulers for Quantum Processes
139
0
0.0
(
0
)
تأليف
Kazuya Yasuda
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
In the study of quantum process algebras, researchers have introduced different notions of equivalence between quantum processes like bisimulation or barbed congruence. However, there are intuitively equivalent quantum processes that these notions do not regard as equivalent. In this paper, we introduce a notion of equivalence named observational equivalence into qCCS. Since quantum processes have both probabilistic and nondeterministic transitions, we introduce schedulers that solve nondeterministic choices and obtain probability distribution of quantum processes. By definition, the restrictions of schedulers change observational equivalence. We propose some definitions of schedulers, and investigate the relation between the restrictions of schedulers and observational equivalence.
قيم البحث
اقرأ أيضاً
Quantum processes describe concurrent communicating systems that may involve quantum information. We propose a notion of open bisimulation for quantum processes and show that it provides both a sound and complete proof methodology for a natural exten
sional behavioural equivalence between quantum processes. We also give a modal characterisation of open bisimulation, by extending the Hennessy-Milner logic to a quantum setting.
Intruders can infer properties of a system by measuring the time it takes for the system to respond to some request of a given protocol, that is, by exploiting time side channels. These properties may help intruders distinguish whether a system is a
honeypot or concrete system helping him avoid defense mechanisms, or track a user among others violating his privacy. Observational equivalence is the technical machinery used for verifying whether two systems are distinguishable. Moreover, efficient symbolic methods have been developed for automating the check of observational equivalence of systems. This paper introduces a novel definition of timed observational equivalence which also distinguishes systems according to their time side channels. Moreover, as our definition uses symbolic time constraints, it can be automated by using SMT-solvers.
With the previous notions of bisimulation presented in literature, to check if two quantum processes are bisimilar, we have to instantiate the free quantum variables of them with arbitrary quantum states, and verify the bisimilarity of resultant conf
igurations. This makes checking bisimilarity infeasible from an algorithmic point of view because quantum states constitute a continuum. In this paper, we introduce a symbolic operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in the previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal logical characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes.
We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- a
nd post-conditions are BI formulas describing quantum states -- the program logic can be seen as a counterpart of separation logic for imperative quantum programs. We exercise the logic for proving the security of quantum one-time pad and secret sharing, and we show how the program logic can be used to discover a flaw in Google Cirqs tutorial on the Variational Quantum Algorithm (VQA).
Fluctuation dissipation theorems connect the linear response of a physical system to a perturbation to the steady-state correlation functions. Until now, most of these theorems have been derived for finite-dimensional systems. However, many relevant
physical processes are described by systems of infinite dimension in the Gaussian regime. In this work, we find a linear response theory for quantum Gaussian systems subject to time dependent Gaussian channels. In particular, we establish a fluctuation dissipation theorem for the covariance matrix that connects its linear response at any time to the steady state two-time correlations. The theorem covers non-equilibrium scenarios as it does not require the steady state to be at thermal equilibrium. We further show how our results simplify the study of Gaussian systems subject to a time dependent Lindbladian master equation. Finally, we illustrate the usage of our new scheme through some examples. Due to broad generality of the Gaussian formalism, we expect our results to find an application in many physical platforms, such as opto-mechanical systems in the presence of external noise or driven quantum heat devices.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
