اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدA Model for Probabilistic Reasoning on Assume/Guarantee Contracts
287
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
In this paper, we present a probabilistic adaptation of an Assume/Guarantee contract formalism. For the sake of generality, we assume that the extended state machines used in the contracts and implementations define sets of runs on a given set of variables, that compose by intersection over the common variables. In order to enable probabilistic reasoning, we consider that the contracts dictate how certain input variables will behave, being either non-deterministic, or probabilistic; the introduction of probabilistic variables leading us to tune the notions of implementation, refinement and composition. As shown in the report, this probabilistic adaptation of the Assume/Guarantee contract theory preserves compositionality and therefore allows modular reliability analysis, either with a top-down or a bottom-up approach.
قيم البحث
اقرأ أيضاً
Motivated by the growing requirements on the operation of complex engineering systems, we present contracts as specifications for continuous-time linear dynamical systems with inputs and outputs. A contract is defined as a pair of assumptions and gua
rantees, both characterized in a behavioural framework. The assumptions encapsulate the available information about the dynamic behaviour of the environment in which the system is supposed to operate, while the guarantees express the desired dynamic behaviour of the system when interconnected with relevant environments. In addition to defining contracts, we characterize contract implementation, and we find necessary conditions for the existence of an implementation. We also characterize contract refinement, which is used to characterize contract conjunction in two special cases. These concepts are then illustrated by an example of a vehicle following system.
Verifying specifications for large-scale modern engineering systems can be a time-consuming task, as most formal verification methods are limited to systems of modest size. Recently, contract-based design and verification has been proposed as a modul
ar framework for specifications, and linear-programming-based techniques have been presented for verifying that a given system satisfies a given contract. In this paper, we extend this assume/guarantee framework by presenting necessary and sufficient conditions for a collection of contracts on individual components to refine a contract on the composed system. These conditions can be verified by solving linear programs, whose number grows linearly with the number of specifications defined by the contracts. We exemplify the tools developed using a case study considering safety in a car-following scenario, where noise and time-varying delay are considered.
Due to its flexible and pervasive sensing ability, crowdsensing has been extensively studied recently in research communities. However, the fundamental issue of how to meet the requirement of sensing robustness in crowdsensing remains largely unsolve
d. Specifically, from the task owners perspective, how to minimize the total payment in crowdsensing while guaranteeing the sensing data quality is a critical issue to be resolved. We elegantly model the robustness requirement over sensing data quality as chance constraints, and investigate both hard and soft chance constraints for different crowdsensing applications. For the former, we reformulate the problem through Booles Inequality, and explore the optimal value gap between the original problem and the reformulated problem. For the latter, we study a serial of a general payment minimization problem, and propose a binary search algorithm that achieves both feasibility and low payment. The performance gap between our solution and the optimal solution is also theoretically analyzed. Extensive simulations validate our theoretical analysis.
We consider multi-agent systems where agents actions and beliefs are determined aleatorically, or by the throw of dice. This system consists of possible worlds that assign distributions to independent random variables, and agents who assign probabili
ties to these possible worlds. We present a novel syntax and semantics for such system, and show that they generalise Modal Logic. We also give a sound and complete calculus for reasoning in the base semantics, and a sound calculus for the full modal semantics, that we conjecture to be complete. Finally we discuss some application to reasoning about game playing agents.
In this paper, we investigate the problem of reasoning over natural language statements. Prior neural based approaches do not explicitly consider the inter-dependency among answers and their proofs. In this paper, we propose PRobr, a novel approach f
or joint answer prediction and proof generation. PRobr defines a joint probabilistic distribution over all possible proof graphs and answers via an induced graphical model. We then optimize the model using variational approximation on top of neural textual representation. Experiments on multiple datasets under diverse settings (fully supervised, few-shot and zero-shot evaluation) verify the effectiveness of PRobr, e.g., achieving 10%-30% improvement on QA accuracy in few/zero-shot evaluation. Our codes and models can be found at https://github.com/changzhisun/PRobr/.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
