اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدCompact Labelings For Efficient First-Order Model-Checking
278
0
0.0
(
0
)
نشر من قبل
Mamadou Moustapha Kant\\'e
تاريخ النشر
2014
مجال البحث
الهندسة المعلوماتية
والبحث باللغة
English
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We consider graph properties that can be checked from labels, i.e., bit sequences, of logarithmic length attached to vertices. We prove that there exists such a labeling for checking a first-order formula with free set variables in the graphs of every class that is emph{nicely locally cwd-decomposable}. This notion generalizes that of a emph{nicely locally tree-decomposable} class. The graphs of such classes can be covered by graphs of bounded emph{clique-width} with limited overlaps. We also consider such labelings for emph{bounded} first-order formulas on graph classes of emph{bounded expansion}. Some of these results are extended to counting queries.
قيم البحث
اقرأ أيضاً
We present a survey of the saturation method for model-checking pushdown systems.
Model checkers provide algorithms for proving that a mathematical model of a system satisfies a given specification. In case of a violation, a counterexample that shows the erroneous behavior is returned. Understanding these counterexamples is challe
nging, especially for hyperproperty specifications, i.e., specifications that relate multiple executions of a system to each other. We aim to facilitate the visual analysis of such counterexamples through our HyperVis tool, which provides interactive visualizations of the given model, specification, and counterexample. Within an iterative and interdisciplinary design process, we developed visualization solutions that can effectively communicate the core aspects of the model checking result. Specifically, we introduce graphical representations of binary values for improving pattern recognition, color encoding for better indicating related aspects, visually enhanced textual descriptions, as well as extensive cross-view highlighting mechanisms. Further, through an underlying causal analysis of the counterexample, we are also able to identify values that contributed to the violation and use this knowledge for both improved encoding and highlighting. Finally, the analyst can modify both the specification of the hyperproperty and the system directly within HyperVis and initiate the model checking of the new version. In combination, these features notably support the analyst in understanding the error leading to the counterexample as well as iterating the provided system and specification. We ran multiple case studies with HyperVis and tested it with domain experts in qualitative feedback sessions. The participants positive feedback confirms the considerable improvement over the manual, text-based status quo and the value of the tool for explaining hyperproperties.
Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialised the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by si
gnal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-art real root isolation algorithm under Schanuels conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.
In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HFL, we explain how it can be applied to program verification, and summarize the current status of the project.
We study the symmetric weighted first-order model counting task and present ApproxWFOMC, a novel anytime method for efficiently bounding the weighted first-order model count in the presence of an unweighted first-order model counting oracle. The algo
rithm has applications to inference in a variety of first-order probabilistic representations, such as Markov logic networks and probabilistic logic programs. Crucially for many applications, we make no assumptions on the form of the input sentence. Instead, our algorithm makes use of the symmetry inherent in the problem by imposing cardinality constraints on the number of possible true groundings of a sentences literals. Realising the first-order model counting oracle in practice using the approximate hashing-based model counter ApproxMC3, we show how our algorithm outperforms existing approximate and exact techniques for inference in first-order probabilistic models. We additionally provide PAC guarantees on the generated bounds.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
