اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدDL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE
31
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We prove that the model checking and the satisfiability problem of both Dynamic Logic of Propositional Assignments DL-PA and Coalition Logic of Propositional Control and Delegation DCL-PC are in PSPACE. We explain why the proof of EXPTIME-hardness of the model checking problem of DL-PA presented in (Balbiani, Herzig, Troquard, 2013) is false. We also explain why the proof of membership in PSPACE of the model checking problem of DCL-PC given in (van der Hoek, Walther, Wooldridge, 2010) is wrong.
قيم البحث
اقرأ أيضاً
The expressive power of interval temporal logics (ITLs) makes them really fascinating, and one of the most natural choices as specification and planning language. However, for a long time, due to their high computational complexity, they were conside
red not suitable for practical purposes. The recent discovery of several computationally well-behaved ITLs has finally changed the scenario. In this paper, we investigate the finite satisfiability and model checking problems for the ITL D featuring the sub-interval relation, under the homogeneity assumption (that constrains a proposition letter to hold over an interval if and only if it holds over all its points). First we prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete; then we show that its model checking problem, over finite Kripke structures, is PSPACE-complete as well. The paper enrich the set of tractable interval temporal logics with a meaningful representative.
Binary decision diagrams can compactly represent vast sets of states, mitigating the state space explosion problem in model checking. Probabilistic systems, however, require multi-terminal diagrams storing rational numbers. They are inefficient for m
odels with many distinct probabilities and for iterative numeric algorithms like value iteration. In this paper, we present a new symblicit approach to checking Markov chains and related probabilistic models: We first generate a decision diagram that symbolically collects all reachable states and their predecessors. We then concretise states one-by-one into an explicit partial state space representation. Whenever all predecessors of a state have been concretised, we eliminate it from the explicit state space in a way that preserves all relevant probabilities and rewards. We thus keep few explicit states in memory at any time. Experiments show that very large models can be model-checked in this way with very low memory consumption.
In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and vario
We prove that Strings-and-Coins -- the combinatorial two-player game generalizing the dual of Dots-and-Boxes -- is strongly PSPACE-complete on multigraphs. This result improves the best previous result, NP-hardness, argued in Winning Ways. Our result
also applies to the Nimstring variant, where the winner is determined by normal play; indeed, one step in our reduction is the standard reduction (also from Winning Ways) from Nimstring to Strings-and-Coins.
We present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in emph{C. Elegans}, the common roundworm. TW is a reflexive behavio
r exhibited by emph{C. Elegans} in response to vibrating the surface on which it is moving; the neural circuit underlying this response is the subject of this investigation. Specifically, we perform reachability analysis on the TW circuit model of Wicks et al. (1996), which enables us to estimate key circuit parameters. Underlying our approach is the use of Fan and Mitras recently developed technique for automatically computing local discrepancy (convergence and divergence rates) of general nonlinear systems. We show that the results we obtain are in agreement with the experimental results of Wicks et al. (1995). As opposed to the fixed parameters found in most biological models, which can only produce the predominant behavior, our techniques characterize ranges of parameters that produce (and do not produce) all three observed behaviors: reversal of movement, acceleration, and lack of response.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
