اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدConstraint-based reachability
66
0
0.0
(
0
)
تأليف
Arnaud Gotlieb
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Iterative imperative programs can be considered as infinite-state systems computing over possibly unbounded domains. Studying reachability in these systems is challenging as it requires to deal with an infinite number of states with standard backward or forward exploration strategies. An approach that we call Constraint-based reachability, is proposed to address reachability problems by exploring program states using a constraint model of the whole program. The keypoint of the approach is to interpret imperative constructions such as conditionals, loops, array and memory manipulations with the fundamental notion of constraint over a computational domain. By combining constraint filtering and abstraction techniques, Constraint-based reachability is able to solve reachability problems which are usually outside the scope of backward or forward exploration strategies. This paper proposes an interpretation of classical filtering consistencies used in Constraint Programming as abstract domain computations, and shows how this approach can be used to produce a constraint solver that efficiently generates solutions for reachability problems that are unsolvable by other approaches.
قيم البحث
اقرأ أيضاً
We introduce a description logic ALCQIO_{b,Re} which adds reachability assertions to ALCQIO, a sub-logic of the two-variable fragment of first order logic with counting quantifiers. ALCQIO_{b,Re} is well-suited for applications in software verificati
on and shape analysis. Shape analysis requires expressive logics which can express reachability and have good computational properties. We show that ALCQIO_{b,Re} can describe complex data structures with a high degree of sharing and allows compositions such as list of trees. We show that the finite satisfiability and implication problems of ALCQIO_{b,Re}-formulae are polynomial-time reducible to finite satisfiability of ALCQIO-formulae. As a consequence, we get that finite satisfiability and finite implication in ALCQIO_{b,Re} are NEXPTIME-complete. Description logics with transitive closure constructors have been studied before, but ALCQIO_{b,Re} is the first description logic that remains decidable on finite structures while allowing at the same time nominals, inverse roles, counting quantifiers and reachability assertions,
IC3 has been a leap forward in symbolic model checking. This paper proposes PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Our main focus is to develop the theory underlying PrIC3. Alongside, we pr
esent a first implementation of PrIC3 including the key ingredients from IC3 such as generalization, repushing, and propagation.
This paper is about reachability analysis in a restricted subclass of multi-pushdown automata. We assume that the control states of an automaton are partially ordered, and all transitions of an automaton go downwards with respect to the order. We pro
ve decidability of the reachability problem, and computability of the backward reachability set. As the main contribution, we identify relevant subclasses where the reachability problem becomes NP-complete. This matches the complexity of the same problem for communication-free vector addition systems, a special case of stateless multi-pushdown automata.
Parametric Interval Markov Chains (pIMCs) are a specification formalism that extend Markov Chains (MCs) and Interval Markov Chains (IMCs) by taking into account imprecision in the transition probability values: transitions in pIMCs are labeled with p
arametric intervals of probabilities. In this work, we study the difference between pIMCs and other Markov Chain abstractions models and investigate the two usual semantics for IMCs: once-and-for-all and at-every-step. In particular, we prove that both semantics agree on the maximal/minimal reachability probabilities of a given IMC. We then investigate solutions to several parameter synthesis problems in the context of pIMCs -- consistency, qualitative reachability and quantitative reachability -- that rely on constraint encodings. Finally, we propose a prototype implementation of our constraint encodings with promising results.
Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers
for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP and we show it to be a useful companion tool for the existing debugging techniques. Our technique starts by considering a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to timed variants of CCP. We also develop a prototypical implementation freely available for making experiments.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
