On temporal logics with data variable quantifications

摘要: Although data values are available in almost every computer system, reasoning about them is a challenging task due to the huge size or even infinite domains. Temporal logics well-known specification formalisms for reactive and concurrent systems. Various extensions of temporal have been proposed reason values, mostly last decade. Among them, one natural idea extend with variable quantifications ranging over an domain. Grumberg, Kupferman Sheinvald initiated research on this topic recently obtained several interesting results. However, there still lack systematic investigation theoretical aspects logics. Our goal paper fill gap. Around goal, we make following choices: 1. We consider two widely used logics, Linear Logic (LTL) Computation Tree (CTL), allow arbitrary nestings Boolean operators (the resulting called respectively variable-LTL, brief VLTL, variable-CTL, VCTL). 2. investigate decidability complexity both satisfiability model checking problems, finite words (trees). In particular, obtain results: Existential quantifiers single universal quantifier beginning already entail undecidability problems VLTL VCTL, (trees); if only existential path then problem (over trees) decidable, no matter which available; formulae beginning, occurrences non-parameterized atomic propositions guarded by positive quantified variables, its becomes words; based these results problem, deduce (un)decidability problem.