1,720,976 research outputs found
An Approximation Algorithm for the Minimum Weight Vertex-Connectivity Problem with Sharpened Triangle Inequality
No full text
Graded-CTL: Satisfiability and Symbolic Model Checking
No full textIn this paper we continue the study of a strict extension of the Computation Tree Logic, called `graded-CTL`, recently introduced by the same authors in [FNP08]. This new logic augments the standard quantifiers with graded modalities, being able thus to express `There exist at least k` or `For all but k` futures, for some constant k. One can thus describe properties useful in system design, which cannot be expressed with CTL, like a sort of redundant liveness property asking whether there is more than one path satisfying that `something good eventually happens`, making thus the system more tolerant to possible faults. Graded-CTL formulas can also be used to determine whether there are more than a given number of bad behaviors of a system: this, in the model-checking framework, means that one can verify the existence of a user-defined number of counterexamples for a given specification and generate them, in a unique run of the model-checker. Here we show both theoretical and applicative contributions. On the theoretical side we give a simple algorithm to `decide` this logic and we prove that the satisfiability problem is ExpTime-complete when the constants of the quantifiers are represented in unary. On the applicative side we propose `symbolic` algorithms to solve the model checking problem. One of the main characteristics of these algorithms is that, though the the computation of `distinct` counterexamples has inherently high complexity when the model is represented symbolically (consider for example the implementation of a symbolic DFS), we have designed them to make the generation of multiple counterexamples as easy and quick as possible. The symbolic algorithms have also been implemented using BDD data structures, and have been integrated into the well known NuSMV model checker, that has also been modified to accept specifications expressed in graded-CTL. The test results we have reported are very comfortable in the sense that both the running time and the sizes of the BDD produced are comparable to those obtained with specifications expressed in classical CTL
On the Hardness of Optimization in Power Law Graphs
No full textAbstractOur motivation for this work is the remarkable discovery that many large-scale real-world graphs ranging from Internet and World Wide Web to social and biological networks appear to exhibit a power-law distribution: the number of nodes yi of a given degree i is proportional to i−β where β>0 is a constant that depends on the application domain. There is practical evidence that combinatorial optimization in power-law graphs is easier than in general graphs, prompting the basic theoretical question: Is combinatorial optimization in power-law graphs easy? Does the answer depend on the power-law exponent β? Our main result is the proof that many classical NP-hard graph-theoretic optimization problems remain NP-hard on power-law graphs for certain values of β. In particular, we show that some classical problems, such as CLIQUE and COLORING, remain NP-hard for all β≥1. Moreover, we show that all the problems that satisfy the so-called “optimal substructure property” remain NP-hard for all β>0. This includes classical problems such as MINIMUM VERTEX COVER, MAXIMUM INDEPENDENT SET, and MINIMUM DOMINATING SET. Our proofs involve designing efficient algorithms for constructing graphs with prescribed degree sequences that are tractable with respect to various optimization problems
MODEL-CHECKING FOR GRADED CTL
No full textRecently, complexity issues related to the decidability of the -calculus, when the universal and existential quantifiers are augmented with `graded modalities`, have been investigated by Kupfermann, Sattler and Vardi ([KSV02]). Graded modalities refer to the use of the universal and existential quantifiers with the added capability to express the concept of `at least` or `all but` , for a non-negative integer . In this paper we study the Computational Tree Logic CTL, a branching time extension of classical modal logic, augmented with graded modalities and investigate the complexity issues with respect to the model-checking problem. We consider a system model represented by a Kripke structure and give an algorithm to solve the model-checking problem running in time which is hence tight for the problem (here is the number of temporal and boolean operators and does not include the values occurring in the graded modalities). In this framework, the graded modalities express the ability to generate a user-defined number of counterexamples to a specification given in \ctl. However, these multiple counterexamples can partially overlap, that is they may share some behavior. We have hence investigated the case when all of them are completely disjoint. In this case we prove that the model-checking problem is both \NP-hard and \coNP-hard and give an algorithm for solving it running in polynomial space. We have thus studied a fragment of graded-\ctl, and have proved that the model-checking problem is solvable in polynomial time
- …
