1,720,996 research outputs found
Solving Mean-Payoff Games via Quasi Dominions
Full text linkWe propose a novel algorithm for the solution of mean-payoff games that merges together two seemingly unrelated concepts introduced in the context of parity games, small progress measures and quasi dominions. We show that the integration of the two notions can be highly beneficial and significantly speeds up convergence to the problem solution. Experiments show that the resulting algorithm performs orders of magnitude better than the asymptotically-best solution algorithm currently known, without sacrificing on the worst-case complexity
Counterexample-guided abstraction refinement for linear programs with arrays
No full textPredicate abstraction refinement is one of the leading approaches to software verification. The key idea is to abstract the input program into a Boolean Program (i.e. a program whose variables range over the Boolean values only and model the truth values of predicates corresponding to properties of the program state), and refinement searches for new predicates in order to build a new, more refined abstraction. Thus Boolean programs are commonly employed as a simple, yet useful abstraction. However, the effectiveness of predicate abstraction refinement on programs that involve a tight interplay between data-flow and control-flow is still to be ascertained. We present a novel counterexample guided abstraction refinement procedure for Linear Programs with arrays, a fragment of the C programming language where variables and array elements range over a numeric domain and expressions involve linear combinations of variables and array elements. In our procedure the input program is abstracted w.r.t. a family of sets of array indices, the abstraction is a Linear Program (without arrays), and refinement searches for new array indices. We use Linear Programs as the target of the abstraction (instead of Boolean programs) as they allow to express complex correlations between data and control. Thus, unlike the approaches based on predicate abstraction, our approach treats arrays precisely. This is an important feature as arrays are ubiquitous in programming. We provide a precise account of the abstraction, Model Checking, and refinement processes, discuss their implementation in the EUREKA tool, and present a detailed analysis of the experimental results confirming the effectiveness of our approach on a number of programs of interest
Taming Strategy Logic: Non-Recurrent Fragments
Full text linkStrategy Logic ([Formula presented] for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends [Formula presented] with first-order quantifiers over the agent strategies and encompasses other formalisms, such as [Formula presented] and [Formula presented]. The model-checking problem for [Formula presented] and several of its fragments has been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal [Formula presented], where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these two logics, and for the corresponding fragments of [Formula presented] and [Formula presented], is in [Formula presented] and [Formula presented], respectively
Taming Strategy Logic: Non-Recurrent Fragments
Full text linkStrategy Logic (SL for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends LTL with first-order quantifiers over the agent strategies and encompasses other formalisms, such as ATL* and CTL*. The model-checking problem for SL and several of its fragments have been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal SL, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these logics, and for the corresponding fragments of ATL* and CTL*, is ExpSpace and PSpace-complete, respectively
Model Checking Linear Programs with Arrays
No full textAbstractIn previous work we proposed Linear Programs as a fine grained model for imperative programs, and showed how the model checking procedure used in SLAM can be generalised to a model checking procedure for Linear Programs. In this paper we show that our model checking procedure for linear programs can be extended in such a way to support the analysis of linear programs featuring a symbol for undefined values and conditional expressions. This extension is particularly important as it paves the way to the construction of model checking procedures for wider classes of imperative programs such as, e.g., linear programs with arrays. We provide a detailed account of a symbolic model checking procedure for this extended class of linear programs, discuss its implementation in the eureka tool, and present experimental results that confirm its effectiveness in the analysis of linear programs with arrays
Full Characterisation of Extended CTL
Full text linkThe precise identification of the expressive power of logic languages used in formal methods for specifying and verifying run-time properties of critical systems is a fundamental task and characterisation theorems play a crucial role as model-theoretic tools in this regard. While a clear picture of the expressive power of linear-time temporal logics in terms of word automata and predicate logics has long been established, a complete mapping of the corresponding relationships for branching-time temporal logics has proven to be a more elusive task over the past four decades with few scattered results. Only recently, an automata-theoretic characterisation of both CTL* and its full-ω-regular extension ECTL* has been provided in terms of Symmetric Hesitant Tree Automata (HTA), with and without a suitable counter-freeness restriction on their linear behaviours. These two temporal logics also correspond to the bisimulation-invariant semantic fragments of Monadic Path Logic (MPL) and Monadic Chain Logic (MCL), respectively. Additionally, it has been proven that the counting extensions of CTL* and ECTL*, namely CCTL* and CECTL*, enjoy equivalent graded versions of the HTAs for the corresponding non-counting logics. However, while Moller and Rabinovich have proved CCTL* to be equivalent to full MPL, thus filling the gap for the standard branching-time logic, no similar result has been given for CECTL*. This work completes the picture, by proving the expressive equivalence of CECTL* and full MCL, by means of a composition theorem for the latter logic. This also indirectly establishes the equivalence between HTAs and their first-order extensions HFTAs, as originally introduced by Walukiewicz
Alternating (In)Dependence-Friendly Logic
Full text linkHintikka and Sandu originally proposed Independence Friendly Logic ([Formula presented]) as a first-order logic of imperfect information to describe game-theoretic phenomena underlying the semantics of natural language. The logic allows for expressing independence constraints among quantified variables, in a similar vein to Henkin quantifiers, and has a nice game-theoretic semantics in terms of imperfect information games. However, the [Formula presented] semantics exhibits some limitations, at least from a purely logical perspective. It treats the players asymmetrically, considering only one of the two players as having imperfect information when evaluating truth, resp., falsity, of a sentence. In addition, truth and falsity of sentences coincide with the existence of a uniform winning strategy for one of the two players in the semantic imperfect information game. As a consequence, [Formula presented] does admit undetermined sentences, which are neither true nor false, thus failing the law of excluded middle. These idiosyncrasies limit its expressive power to the existential fragment of Second Order Logic ([Formula presented]). In this paper, we investigate an extension of [Formula presented], called Alternating Dependence/Independence Friendly Logic ([Formula presented]), tailored to overcome these limitations. To this end, we introduce a novel compositional semantics, generalising the one based on trumps proposed by Hodges for [Formula presented]. The new semantics (i) allows for meaningfully restricting both players at the same time, (ii) enjoys the property of game-theoretic determinacy, (iii) recovers the law of excluded middle for sentences, and (iv) grants [Formula presented] the full descriptive power of [Formula presented]. We also provide an equivalent Herbrand-Skolem semantics and a game-theoretic semantics for the prenex fragment of [Formula presented], the latter being defined in terms of a determined infinite-duration game that precisely captures the other two semantics on finite structures
Good-for-Game QPTL: An Alternating Hodges Semantics
No full textAn extension of QPTL is considered where functional dependencies among the quantified variables can be restricted in such a way that their current values are independent of the future values of the other variables. This restriction is tightly connected to the notion of behavioral strategies in game-theory and allows the resulting logic to naturally express game-theoretic concepts. Inspired by the work on logics of dependence and independence, we provide a new compositional semantics for QPTL that allows for expressing such functional dependencies among variables. The fragment where only restricted quantifications are considered, called behavioral quantifications, allows for linear-time properties that are satisfiable if and only if they are realisable in the Pnueli-Rosner sense. This fragment can be decided, for both model checking and satisfiability, in 2Exp Time and is expressively equivalent to QPTL, though significantly less succinct
Priority Promotion with Parysian flair
Full text linkWe develop an algorithm that combines the advantages of Priority Promotion, that is one of the leading approaches to solving large parity games in practice, with the quasi-polynomial time guarantees offered by Parys' algorithm. Hybridising these algorithms sounds both natural and difficult, as they both generalise the classic recursive algorithm in different ways that appear to be irreconcilable: while the promotion transcends the call structure, the guarantees change on each level. We show that an interface that respects both is not only effective, but also efficient
- …
