this position paper builds on the authors' previous work on paraconsistent transition systems to propose a modelling framework for quantum circuits with explicit representation of decoherence.
ISBN:
(纸本)9798400707551
this position paper builds on the authors' previous work on paraconsistent transition systems to propose a modelling framework for quantum circuits with explicit representation of decoherence.
Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. Currently, proof methods for low-level MPC protocols are primarily manual and thus tedious ...
详细信息
ISBN:
(纸本)9798400709692
Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. Currently, proof methods for low-level MPC protocols are primarily manual and thus tedious and error-prone, and are also non-standardized and unfamiliar to most PL theorists. As a step towards better language support and language-based enforcement, we develop a new staged PL for defining a variety of low-level probabilistic MPC protocols. We also formulate a collection of confidentiality and integrity hyperproperties for our language model that are familiar from information flow, including conditional noninterference, gradual release, and robust declassification. We demonstrate their relation to standard MPC threat models of passive and malicious security, and how they can be leveraged in security verification of protocols. To prove these properties we develop automated tactics in F-2 that can be integrated with separation logic-style reasoning.
Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving with intensional type theories, with ...
详细信息
ISBN:
(数字)9783031634987
ISBN:
(纸本)9783031634970;9783031634987
Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving with intensional type theories, with PVS being a notable exception. In this paper, we present native rules for automatedreasoning in a dependently-typed version (DHOL) of classical higher-order logic (HOL). DHOL has an extensional type theory with an undecidable type checking problem which contains theorem proving. We implemented the inference rules as well as an automatic type checking mode in Lash, a fork of Satallax, the leading tableaux-based prover for HOL. Our method is sound and complete with respect to provability in DHOL. Completeness is guaranteed by the incorporation of a sound and complete translation from DHOL to HOL recently proposed by Rothgang et al. While this translation can already be used as a preprocessing step to any HOL prover, to achieve better performance, our system directly works in DHOL. Moreover, experimental results show that the DHOL version of Lash can outperform all major HOL provers executed on the translation.
Don’t Starve is a non-linear, real-time survival video game where the player’s objective is to survive as long as possible. the game is challenging because randomly generated situations and events make it ...
详细信息
Quantum interconnects (QuICs), which connect multiple quantum devices to build distributed quantum systems, are essential for large-scale quantum information processing. While various software tools have been develope...
详细信息
ISBN:
(纸本)9798400707551
Quantum interconnects (QuICs), which connect multiple quantum devices to build distributed quantum systems, are essential for large-scale quantum information processing. While various software tools have been developed to analyze quantum programs running on QuICs, there are very few frameworks for formal reasoning about them on actual quantum devices. the lack of such tools may make distributed systems unreliable because of the complicated behavior of concurrent quantum processes and the physical constraints of quantum devices. this paper discusses the need for an infrastructure, including a distributed quantum programming language, to realize reliable distributed quantum computing.
the CTL learning problem consists in finding for a given sample of positive and negative Kripke structures a distinguishing CTL formula that is verified by the former but not by the latter. Further constraints may bou...
详细信息
ISBN:
(数字)9783031634987
ISBN:
(纸本)9783031634970;9783031634987
the CTL learning problem consists in finding for a given sample of positive and negative Kripke structures a distinguishing CTL formula that is verified by the former but not by the latter. Further constraints may bound the size and shape of the desired formula or even ask for its minimality in terms of syntactic size. this synthesis problem is motivated by explanation generation for dissimilar models, e.g. comparing a faulty implementation withthe original protocol. We devise a SAT-based encoding for a fixed size CTL formula, then provide an incremental approach that guarantees minimality. We further report on a prototype implementation whose contribution is twofold: first, it allows us to assess the efficiency of various output fragments and optimizations. Secondly, we can experimentally evaluate this tool by randomly mutating Kripke structures or syntactically introducing errors in higher-level models, then learning CTL distinguishing formulas.
We provide novel epistemic logical language and semantics for modeling and analysis of byzantine fault-tolerant multi-agent systems, withthe intent of not only facilitating reasoning about the agents' fault statu...
详细信息
ISBN:
(纸本)9783031635007;9783031635014
We provide novel epistemic logical language and semantics for modeling and analysis of byzantine fault-tolerant multi-agent systems, withthe intent of not only facilitating reasoning about the agents' fault status but also supporting model updates for repair and state recovery. Besides the standard knowledge modalities, our logic provides additional agent-specific hope modalities capable of expressing that an agent is not faulty, and also dynamic modalities enabling change to the agents' correctness status. these dynamic modalities are interpreted as model updates that come in three flavors: fully public, more private, and/or involving factual change. Tailored examples demonstrate the utility and flexibility of our logic for modeling a wide range of fault-detection, isolation, and recovery (FDIR) approaches in mission-critical distributed systems. By providing complete axiomatizations for all variants of our logic, we also create a foundation for building future verification tools for this important class of fault-tolerant applications.
the proceedings contain 116 papers. the topics discussed include: SMath studio in the engineering personnel training for thermal power engineering and heat engineering;3D modeling for a flexible detector in VR radiogr...
ISBN:
(纸本)9798350371369
the proceedings contain 116 papers. the topics discussed include: SMath studio in the engineering personnel training for thermal power engineering and heat engineering;3D modeling for a flexible detector in VR radiography simulator;implementation of a system for teaching the basics of fuzzy logic inference systems and fuzzy case-based reasoning;possibilities of integrating MOOCs in humanitarian and technical students foreign language curriculums;development, modeling and prototyping of a balun transformer for powering an induction-resistive heating system using modern CAD and CAE systems;ontological approach to the document synthesis based on data mining;and ensemble ARIMA-LSTM algorithm in predicting agriculture commodities market price for farmer’s education.
Communicating Datalog Programs (CDPs) are a distributed computing model grounded on logicprogramming: networks of nodes perform Datalog-like computations, leveraging on information coming from incoming messages and d...
详细信息
ISBN:
(纸本)9783031450716;9783031450723
Communicating Datalog Programs (CDPs) are a distributed computing model grounded on logicprogramming: networks of nodes perform Datalog-like computations, leveraging on information coming from incoming messages and databases received from external services. In previous works, the decidability and complexity border of verification for different variants of CDPs was charted. In general, the problem is undecidable, but model-checking of CTL formulas specialized to the data-centric and distributed setting is decidable for CDPs where all data-sources, except the external inputs, are bounded. An intuitive explanation is that "a bounded state is unable to fully take advantage of an unbounded input", a formal justification is missing. However, we note that traditional CDPs have a limited capability of handling external inputs, i.e., they cannot directly compare two successive inputs or messages. thus, an alternative explanation is that an unbounded data-source does per se not cause undecidability, as long as the CDP cannot compare two successive instances.
the comprehensive inspection trainset for urban rail transit is a type of large-scale inspection equipment that conforms to the green equipment system and intelligent inspection concept, equipped with multiple types o...
详细信息
ISBN:
(纸本)9781510674479
the comprehensive inspection trainset for urban rail transit is a type of large-scale inspection equipment that conforms to the green equipment system and intelligent inspection concept, equipped with multiple types of inspection systems. the existing control mode of the trainset is that each inspection system operation is handled by a dedicated person during the inspection task, which requires a large number of following personnel and high trainset usage costs. A new control mode has been explored, which is based on automated perception and processing technology and proposes automated operation logic for comprehensive inspection trainset. It utilizes this logic to design a vehicle-mounted centralized control system that automatically senses task information, sets data collection parameters, and automatically turns on and off the inspection systems. At the same time, for periodic inspection services, or by utilizing the inspection tasks of electronic tag readers and encoders, a series of logic is set to replace the role of humans to determine whether the inspection system is working properly, and to obtain information on the activation end of the trainset operation to ensure the correctness of inspection data collection. the vehicle-mounted centralized control system system provides an automated inspection process for the comprehensive inspection trainset, enabling the trainset to have the function of being unmanned during data collection, achieving cost reduction and efficiency increase in trainset use.
暂无评论