Entity-linking is a natural-language-processing task that consists in identifying the entities mentioned in a piece of text, linking each to an appropriate item in some knowledge base; when the knowledge base is Wikipedia, the problem comes to be known as wikification (in this case, items are wikipedia articles). One instance of entity-linking can be formalized as an optimization problem on the underlying concept graph, where the quantity to be optimized is the average distance between chosen items. Inspired by this application, we define a new graph problem which is a natural variant of the Maximum Capacity Representative Set. We prove that our problem is NP-hard for general graphs; nonetheless, under some restrictive assumptions, it turns out to be solvable in linear time. For the general case, we propose two heuristics: one tries to enforce the above assumptions and another one is based on the notion of hitting distance; we show experimentally how these approaches perform with respect to some baselines on a real-world dataset.
The Paxos distributed consensus algorithm is a challenging case-study for standard, vector-based model checking techniques. Due to asynchronous communication, exhaustive analysis may generate very large state spaces already for small model instances. In this paper, we show the advantages of graph transformation as an alternative modelling technique. We model Paxos in a rich declarative transformation language, featuring (among other things) nested quantifiers, and we validate our model using the GROOVE model checker, a graph-based tool that exploits isomorphism as a natural way to prune the state space via symmetry reductions. We compare the results with those obtained by the standard model checker SPIN on the basis of a vector-based encoding of the algorithm.
In this paper we address the problem of planning in rich domains, where knowledge representation is a key aspect for managing the complexity and size of the planning domain. We follow the approach of Description Logic (DL) based Dynamic Knowledge Bases, where a state of the world is represented concisely by a (possibly changing) ABox and a (fixed) TBox con taining the axioms, and actions that allow to change the content of the ABox. The plan goal is given in terms of satisfaction of a DL query. In this paper we start from a traditional forward planning algorithm and we propose a much more efficient variant by combining backward and forwar d search. In particular, we propose a Backward State-space Reductiontechnique that consists in two phases: first, an Abstract Planning Graph P is created by using the Abstract Backward Planning Algorithm(ABP), then the abstract planning graph P is instantiated into a corresponding planning graph P by using the Forward Plan Instantiation Algorithm (FPI). The advantage is that in the preliminary ABP phase we produce a symbolic plan that is a pattern to direct the search of the concrete pla n. This can be seen as a kind of informed search where the preliminary backward phase is useful to discover properties of the statespace that can be used to direct the subsequent forward phase. We evaluate the effectiveness of our ABP+FPI algorithm in the reduction of the explored planning domain by comparing it to a standard forward planning algorithm and applying both of them to a concrete business case study.
We present a new tool for verification of modal mu- calculus formulae for process specifications, based on symbolic parity games. It enhances an existing method, that first encodes the problem to a Parameterised Boolean Equation System (PBES) and then instantiates the PBES to a parity game. We improved the translation from specification to PBES to preserve the structure of the specification in the PBES, we extended LTSmin to instantiate PBESs to symbolic parity games, and implemented the recursive parity game solving algorithm by Zielonka for symbolic parity games. We use Multi-valued Decision Diagrams (MDDs) to represent sets and relations, thus enabling the tools to deal with very large systems. The transition relation is partitioned based on the structure of the specification, which allows for efficient manipulation of the MDDs. We performed two case studies on modular specifications, that demonstrate that the new method has better time and memory performance than existing PBES based tools and can be faster (but slightly less memory efficient) than the symbolic model checker NuSMV.
We present strategic portgraph rewriting as a basis for the implementation of visual modelling and analysis tools. The goal is to facilitate the specification, analysis and simulation of complex systems, using port graphs. A system is represented by an initial graph and a collection of graph rewriting rules, together with a user-defined strategy to control the application of rules. The strategy language includes constructs to deal with graph traversal and management of rewriting positions in the graph. We give a small-step operational semantics for the language, and describe its implementation in the graph transformation and visualisation tool PORGY.
Modern software systems increasingly incorporate self-* behavior to adapt to changes in the environment at runtime. Such adaptations often involve reconfiguring the software architecture of the system. Many systems also need to manage their architecture themselves, i.e., they need a planning component to autonomously decide which reconfigurations to execute to reach a desired target configuration. For the specification of reconfigurations, we employ graph transformations systems (GTS) due to the close relation of graphs and UML object diagrams. We solve the resulting planning problems with a planning system that works directly on a GTS. It features a domain-independent heuristic that uses the solution length of an abstraction of the original problem as an estimate. Finally, we provide experimental results on two different domains, which confirm that our heuristic performs better than another domain-independent heuristic which resembles heuristics employed in related work.
Compiler optimizations, usually expressed as rewrites on program graphs, are a core part of all modern compilers.However, even production compilers have bugs, and these bugs are difficult to detect and resolve.The problem only becomes more complex when compiling parallel programs; from the choice of graph representation to the possibility of race conditions, optimization designers have a range of factors to consider that do not appear when dealing with single-threaded programs.In this paper we present PTRANS, a domain-specific language for formal specification of compiler transformations, and describe its executable semantics.The fundamental approach of PTRANS is to describe program transformations as rewrites on control flow graphs with temporal logic side conditions.The syntax of PTRANS allows cleaner, more comprehensible specification of program optimizations; its executable semantics allows these specifications to act as prototypes for the optimizations themselves, so that candidate optimizations can be tested and refined before going on to include them in a compiler.We demonstrate the use of PTRANS to state, test, and refine the specification of a redundant store elimination optimization on parallel programs.
The reachability problem in cooperating systems is known to be PSPACE-complete. We show here that this problem remains PSPACE-complete when we restrict the communication structure between the subsystems in various ways. For this purpose we introduce two basic and incomparable subclasses of cooperating systems that occur often in practice and provide respective reductions. The subclasses we consider consist of cooperating systems the communication structure of which forms a line respectively a star.
In this paper we present the extension of an existing method for abstract graph-based state space exploration, called neighbourhood abstraction, with a reduction technique based on subsumption.Basically, one abstract state subsumes another when it covers more concrete states; in such a case, the subsumed state need not be included in the state space, thus giving a reduction.We explain the theory and especially also report on a number of experiments, which show that subsumption indeed drastically reduces both the state space and the resources (time and memory) needed to compute it.
Parameterised Boolean Equation Systems (PBESs) are sequences of Boolean fixed point equations with data variables, used for, e.g., verification of modal mu-calculus formulae for process algebraic specifications with data. Solving a PBES is usually done by instantiation to a Parity Game and then solving the game. Practical game solvers exist, but the instantiation step is the bottleneck. We enhance the instantiation in two steps. First, we transform the PBES to a Parameterised Parity Game (PPG), a PBES with each equation either conjunctive or disjunctive. Then we use LTSmin, that offers transition caching, efficient storage of states and both distributed and symbolic state space generation, for generating the game graph. To that end we define a language module for LTSmin, consisting of an encoding of variables with parameters into state vectors, a grouped transition relation and a dependency matrix to indicate the dependencies between parts of the state vector and transition groups. Benchmarks on some large case studies, show that the method speeds up the instantiation significantly and decreases memory usage drastically.
For the exploration of large state spaces, symbolic search using binary decision diagrams (BDDs) can save huge amounts of memory and computation time. State sets are represented and modified by accessing and manipulating their characteristic functions. BDD partitioning is used to compute the image as the disjunction of smaller subimages.In this paper, we propose a novel BDD partitioning option. The partitioning is lexicographical in the binary representation of the states contained in the set that is represented by a BDD and uniform with respect to the number of states represented. The motivation of controlling the state set sizes in the partitioning is to eventually bridge the gap between explicit and symbolic search.Let n be the size of the binary state vector. We propose an O(n) ranking and unranking scheme that supports negated edges and operates on top of precomputed satcount values. For the uniform split of a BDD, we then use unranking to provide paths along which we partition the BDDs. In a shared BDD representation the efforts are O(n). The algorithms are fully integrated in the CUDD library and evaluated in strongly solving general game playing benchmarks.
We describe efficient algorithms to analyze the cycle structure of the graph induced by the state transition function of the A5/1 stream cipher used in GSM mobile phones and report on the results of the implementation. The analysis is performed in five steps utilizing HPC clusters, GPGPU and external memory computation. A great reduction of this huge state transition graph of 2 64 nodes is achieved by focusing on special nodes in the first step and removing leaf nodes that can be detected with limited effort in the second step. This step does not break the overall structure of the graph and keeps at least one node on every cycle. In the third step the nodes of the reduced graph are connected by weighted edges. Since the number of nodes is still huge an efficient bitslice approach is presented that is implemented with NVIDIA’s CUDA framework and executed on several GPUs concurrently. An external memory algorithm based on the STXXL library and its parallel pipelining feature further reduces the graph in the fourth step. The result is a graph containing only cycles that can be further analyzed in internal memory to count the number and size of the cycles. This full analysis which previously would take months can now be completed within a few days and allows to present structural results for the full graph for the first time. The structure of the A5/1 graph deviates notably from the theoretical results for random mappings.
We consider the problem of computing reachability probabilities: given a Markov chain, an initial state of the Markov chain, and a set of goal states of the Markov chain, what is the probability of reaching any of the goal states from the initial state? This problem can be reduced to solving a linear equation Ax = b for x, where A is a matrix and b is a vector. We consider two iterative methods to solve the linear equation: the Jacobi method and the biconjugate gradient stabilized (BiCGStab) method. For both methods, a sequential and a parallel version have been implemented. The parallel versions have been implemented on the compute unified device architecture (CUDA) so that they can be run on a NVIDIA graphics processing unit (GPU). From our experiments we conclude that as the size of the matrix increases, the CUDA implementations outperform the sequential implementations. Furthermore, the BiCGStab method performs better than the Jacobi method for dense matrices, whereas the Jacobi method does better for sparse ones. Since the reachability probabilities problem plays a key role in probabilistic model checking, we also compared the implementations for matrices obtained from a probabilistic model checker. Our experiments support the conjecture by Bosnacki et al. that the Jacobi method is superior to Krylov subspace methods, a class to which the BiCGStab method belongs, for probabilistic model checking.
The overall concept of Transmigrations: Cases of Corporate Reincarnation combines theories and research on social insects, traditional and contemporary corporate structures, job descriptions, and reincarnation scriptures. A variety of conceptual layers enhances the basic idea with depth and an intricate point-of-view. While the layers require study of a substantial amount of bibliography, they provide the project with a spine, by acting as a solid point of departure. Transmigrations showcases 24 portraits of senior executives who return to life as insects. The characters personify symbols and weapons of their trades on a number of levels, some instantly visible and others hidden.
The Artwork The most common format, as seen in this work, presents a page left (verso) and a page right (recto). The right page presents the opening text from George Boole’s “Investigation of the Laws of Thought” (1854) in a sequence of visual characters (glyphs). The glyphs read: “The design of the following treatise is to investigate the fundamental laws of those operations of the mind by which reasoning is performed; to give expression to them in the symbolical language of a Calculus, and upon this foundation to establish the science of Logic” (the glyphs do not include spaces between words)
A number of popular global illumination algorithms uses density estimation to approximate indirect illumination. The density estimate is performed on finite points -- particles -- generated by a stochastic sampling of the scene. In the course of the sampling, particles, representing light, are stochastically emitted from the light sources and reflected around the scene. The sampling induces noise, which in turn is handled by the density estimate during the illumination reconstruction. Unfortunately, this noise reduction imposes a systematic error (bias), which is seen as a blurring of prominent illumination features. This is often not desirable as these may lose clarity or vanish altogether. We present an accurate method for reconstruction of indirect illumination with photon mapping. Instead of reconstructing illumination using classic density estimation on finite points, we use the correlation of light footprints, created by using Ray Differentials during the light pass. This procedure gives a high illumination accuracy, improving the trade-off between bias and variance considerable as compared to traditional particle tracing algorithms. In this way we preserve structures in indirect illumination.
The idea behind Ascension and Scorpion sprang from an exhibition proposal called “Art From Science.” I have been working with satellite imagery over the past four years in my job as a visualization artist at NASA Goddard Space Flight Center. I wanted to incorporate both the satellite images and the scientific diagrams associated with them, as well as my art made outside of this context. I invited three other artists to participate in a collaborative process for the exhibition. Their role was to contribute their own art. I worked with the scientific images and artwork contributed by my collaborators as a starting point to the compositions.
A motion trend analysis method is proposed to reconstruct human motion from un-calibrated monocular video. In this paper, relocation of human subject is the main concern, which is one of the most difficult parts in motion reconstruction and critically affects the accuracy of human posture generation. Numerical studies are conducted on experiments from synthetic and real video data to demonstrate the correctness of the recovered human translation in the proposed system.
The emergence of digital Gesamtkunstwerk as a movement has been precipitated by an interactive installation. The goal of this paper is to research technology and to implement real-time interactive media with applied our project "Your Destiny." In this paper we will discuss the possibilities and advantages of using the background subtraction algorithm to create a dynamic interactive installation and points of issue that there are limitations and considerations to create a digital total work of art.
