Given a demonstration of a complex manipulation task, such as pouring liquid from one container to another, we seek to generate a motion plan for a new task instance involving objects with different geometries. This is nontrivial since we need to simultaneously ensure that the implicit motion constraints are satisfied (glass held upright while moving), that the motion is collision-free, and that the task is successful (e.g., liquid is poured into the target container). We solve this problem by identifying the positions of critical locations and associating a reference frame (called motion transfer frames) on the manipulated object and the target, selected based on their geometries and the task at hand. By tracking and transferring the path of the motion transfer frames, we generate motion plans for arbitrary task instances with objects of different geometries and poses. We show results from simulation as well as robot experiments on physical objects to evaluate the effectiveness of our solution. A video supplement is available on YouTube: https://youtu.be/RuG9zMXnfR8

Present quantum computers are constrained by limited qubit capacity and restricted physical connectivity, leading to challenges in large-scale quantum computations. Distributing quantum computations across a network of quantum computers is a promising way to circumvent these challenges and facilitate large quantum computations. However, distributed quantum computations require entanglements (to execute remote gates) which can incur significant generation latency and, thus, lead to decoherence of qubits. In this work, we consider the problem of distributing quantum circuits across a quantum network to minimize the execution time. The problem entails mapping the circuit qubits to network memories, including within each computer since limited connectivity within computers can affect the circuit execution time. We provide two-step solutions for the above problem: In the first step, we allocate qubits to memories to minimize the estimated execution time; for this step, we design an efficient algorithm based on an approximation algorithm for the max-quadratic-assignment problem. In the second step, we determine an efficient execution scheme, including generating required entanglements with minimum latency under the network resource and decoherence constraints; for this step, we develop two algorithms with appropriate performance guarantees under certain settings or assumptions. We consider multiple protocols for executing remote gates, viz., telegates and cat-entanglements. With extensive simulations over NetSquid, a quantum network simulator, we demonstrate the effectiveness of our developed techniques and show that they outperform a scheme based on prior work by 40 to 50% on average and up to 95% in some cases.

Quantum computing hardware is improving in robustness, but individual computers still have small number of qubits (for storing quantum information). Computations needing a large number of qubits can only be performed by distributing them over a network of smaller quantum computers. In this paper, we consider the problem of distributing a quantum computation, represented as a quantum circuit, over a homogeneous network of quantum computers, minimizing the number of communication operations needed to complete every step of the computation. We propose a two-step solution: dividing the given circuit’s qubits among the computers in the network, and scheduling communication operations, called migrations, to share quantum information among the computers to ensure that every operation can be performed locally. While the first step is an intractable problem, we present a polynomial-time solution for the second step in a special setting, and a O(log n)-approximate solution in the general setting. We provide empirical results which show that our two-step solution outperforms existing heuristic for this problem by a significant margin (up to 90%, in some cases).

Decision-making based on probabilistic reasoning often involves selecting a subset of expensive observations that best predict the system state. In an earlier work, adopting the general notion of value of information (VoI) first introduced by Krause and Guestrin, Ghosh and Ramakrishnan considered the problem of determining optimal conditional observation plans in temporal graphical models, based on non-myopic (non-greedy) VoI, over a finite time horizon. They cast the problem as determining optimal policies in finite-horizon, non-discounted Markov Decision Processes (MDPs). However, there are many practical scenarios where a time horizon is undefinable. In this paper, we consider the VoI optimization problem over an infinite (or equivalently, undefined) time horizon. Adopting an approach similar to Ghosh and Ramakrishnan's, we cast this problem as determining optimal policies in infinite-horizon, finite-state, discounted MDPs. Although our MDP-based framework addresses Dynamic Bayesian Networks (DBNs) that are more restricted than those addressed by Ghosh and Ramakrishnan, we incorporate Krause and Guestrin's general idea of VoI even though it was fundamentally envisioned for finite-horizon settings. We establish the utility of our approach on two graphical models based on real-world datasets.

Generalized Probabilistic Logic (GPL) is a temporal logic, based on the modal mu-calculus, for specifying properties of branching probabilistic systems. We consider GPL over branching systems that also exhibit internal non-determinism under linear-time semantics (which is resolved by schedulers), and focus on the problem of finding the capacity (supremum probability over all schedulers) of a fuzzy formula. Model checking GPL is undecidable, in general, over such systems, and existing GPL model checking algorithms are limited to systems without internal non-determinism, or to checking non-recursive formulae. We define a subclass, called separable GPL, which includes recursive formulae and for which model checking is decidable. A large class of interesting and decidable problems, such as termination of 1-exit Recursive MDPs, reachability of Branching MDPs, and LTL model checking of MDPs, whose decidability has been studied independently, can be reduced to model checking separable GPL. Thus, GPL is widely applicable and, with a suitable extension of its semantics, yields a uniform framework for studying problems involving systems with non-deterministic and probabilistic behaviors.

Abstract Probabilistic Logic Programs (PLPs) generalize traditional logic programs and allow the encoding of models combining logical structure and uncertainty. In PLP, inference is performed by summarizing the possible worlds which entail the query in a suitable data structure, and using this data structure to compute the answer probability. Systems such as ProbLog, PITA, etc., use propositional data structures like explanation graphs, BDDs, SDDs, etc., to represent the possible worlds. While this approach saves inference time due to substructure sharing, there are a number of problems where a more compact data structure is possible. We propose a data structure called Ordered Symbolic Derivation Diagram (OSDD) which captures the possible worlds by means of constraint formulas. We describe a program transformation technique to construct OSDDs via query evaluation, and give procedures to perform exact and approximate inference over OSDDs. Our approach has two key properties. Firstly, the exact inference procedure is a generalization of traditional inference, and results in speedup over the latter in certain settings. Secondly, the approximate technique is a generalization of likelihood weighting in Bayesian Networks, and allows us to perform sampling-based inference with lower rejection rate and variance. We evaluate the effectiveness of the proposed techniques through experiments on several problems.

Decision-making based on probabilistic reasoning often involves selecting a subset of expensive observations, that best predict the system state. Krause and Guestrin described two problems of non-myopically selecting observations in graphical models to optimize the value of information (VoI), namely, selection of an optimal subset of observations, and generation of an optimal conditional observation plan. They showed that these problems are intractable in general, but gave polynomial-time dynamic programming algorithms, called VoIDP, for chain graphical models. In this paper, we consider the general setting of Dynamic Bayesian Networks (DBNs), and formulate these problems in terms of finding optimal policies in Markov Decision Processes (MDPs). The time complexities of the resulting algorithms are exponential in general, but polynomial for chain models. Given a chain model, our algorithms compute the same subset, or plan, as VoIDP. Interestingly, despite their generality, our algorithms have significantly better time complexities for chain models compared to VoIDP. We also present an outline of how to use our framework to formulate an approximate, nonmyopic VoI optimization technique, with absolute a posteriori guarantees on approximation, that can handle arbitrary DBNs efficiently.

Software Model Checking consists of a broad collection of techniques to tackle the complexity and the diversity in the use of software in safety-critical systems. The contributions in this special issue address some of the core problems in software model checking. The articles are based on papers selected from the 2013 SPIN Symposium on Model Checking of Software, an annual forum for practitioners and researchers interested in symbolic and state space-based techniques for the validation and analysis of software systems.

Abstract We present a formulation of the problem of probabilistic model checking as one of query evaluation over probabilistic logic programs. To the best of our knowledge, our formulation is the first of its kind, and it covers a rich class of probabilistic models and probabilistic temporal logics. The inference algorithms of existing probabilistic logic-programming systems are well defined only for queries with a finite number of explanations. This restriction prohibits the encoding of probabilistic model checkers, where explanations correspond to executions of the system being model checked. To overcome this restriction, we propose a more general inference algorithm that uses finite generative structures (similar to automata) to represent families of explanations. The inference algorithm computes the probability of a possibly infinite set of explanations directly from the finite generative structure. We have implemented our inference algorithm in XSB Prolog, and use this implementation to encode probabilistic model checkers for a variety of temporal logics, including PCTL and GPL (which subsumes PCTL*). Our experiment results show that, despite the highly declarative nature of their encodings, the model checkers constructed in this manner are competitive with their native implementations.

Abstract Probabilistic Logic Programming (PLP), exemplified by Sato and Kameya's PRISM, Poole's ICL, Raedt et al.'s ProbLog and Vennekens et al.'s LPAD, is aimed at combining statistical and logical knowledge representation and inference. However, the inference techniques used in these works rely on enumerating sets of explanations for a query answer. Consequently, these languages permit very limited use of random variables with continuous distributions. In this paper, we present a symbolic inference procedure that uses constraints and represents sets of explanations without enumeration. This permits us to reason over PLPs with Gaussian or Gamma-distributed random variables (in addition to discrete-valued random variables) and linear equality constraints over reals. We develop the inference procedure in the context of PRISM; however the procedure's core ideas can be easily applied to other PLP languages as well. An interesting aspect of our inference procedure is that PRISM's query evaluation process becomes a special case in the absence of any continuous random variables in the program. The symbolic inference procedure enables us to reason over complex probabilistic models such as Kalman filters and a large subclass of Hybrid Bayesian networks that were hitherto not possible in PLP frameworks.

Role based access control (RBAC) is a widely used access control paradigm. In large organizations, the RBAC policy is managed by multiple administrators. An administrative role based access control (ARBAC) policy specifies how each administrator may change the RBAC policy. It is often difficult to fully understand the effect of an ARBAC policy by simple inspection, because sequences of changes by different administrators may interact in unexpected ways. ARBAC policy analysis algorithms can help by answering questions, such as user-role reachability, which asks whether a given user can be assigned to given roles by given administrators. Allowing roles and permissions to have parameters significantly enhances the scalability, flexibility, and expressiveness of ARBAC policies. This paper defines PARBAC, which extends the classic ARBAC97 model to support parameters, and presents an analysis algorithm for PARBAC. To the best of our knowledge, this is the first analysis algorithm specifically for parameterized ARBAC policies. We evaluate its efficiency by analyzing its parameterized complexity and benchmarking it on case studies and synthetic policies.

Screen readers, the dominant assistive technology used by visually impaired people to access the Web, function by speaking out the content of the screen serially. Using screen readers for conducting online transactions can cause considerable information overload, because transactions, such as shopping and paying bills, typically involve a number of steps spanning several web pages. One can combat this overload by using a transaction model for web accessibility that presents only fragments of web pages that are needed for doing transactions. We can realize such a model by coupling a process automaton, encoding states of a transaction, with concept classifiers that identify page fragments “relevant ” to a particular state of the transaction. In this paper we present a fully automated process that synergistically combines several techniques for transforming unlabeled

Synthesizing high-level semantic knowledge from low-level sensor data is an important problem in many sensor network applications. Programming a network to perform such synthesis in situ is especially difficult due to the stringent resource constraints, unreliable wireless communication, and complex distributed algorithms and network protocols required to manipulate the data. Recently, a declarative programming language called Snlog [5] has been developed to address this problem. However, statistical reasoning for modeling noise in the context of sensor networks has not been addressed in Snlog. In this paper, we develop a methodology based on the PRISM [36] framework, which integrates logical and statistical reasoning, for specifying sensor network programs that deal with noisy data and tolerate faults in the network. The relationship between high-level (synthesized) and low-level (observed) data is captured by logical rules, while statistical models are used to specify computations in the presence of noise and faults. We illustrate our methodology with three examples: (i) estimating temperature at various points in a region, (ii) evaluating the trajectory of an object observed by a sensor network, based on the Hidden Markov Model, and (iii) evaluating most reliable communication paths between sensor nodes. We analyze the results of simulations as well as an experimental deployment to evaluate the practical feasibility of our approach.

Administrative RBAC (ARBAC) policies specify how Role-Based Access Control (RBAC) policies may be changed by each administrator. It is often difficult to fully understand the effect of an ARBAC policy by simple inspection, because sequences of changes by different administrators may interact in unexpected ways. ARBAC policy analysis algorithms can help by answering questions, such a suser-role reachability, which asks whether a given user can be assigned to given roles by given administrators. This problem is intractable in general. This paper identifies classes of policies of practical interest, develops analysis algorithms for them, and analyzes their parameterized complexity, showing that the algorithms may have high complexity with respect to some parameter k characterizing the hardness of the input (such that k is often small in practice) but have polynomial complexity in terms of the overall input size when the value of k is fixed.

Role-based access control (RBAC) is a widely used model for expressing access control policies. In large organizations, the RBAC policy may be collectively managed by many administrators. Administrative RBAC (ARBAC) is a model for expressing the authority of administrators, thereby specifying how an organization's RBAC policy may change. Changes by one administrator may interact in unintended ways with changes by other administrators. Consequently, the effect of an ARBAC policy is hard to understand by simple inspection. In this paper, we consider the problem of analyzing ARBAC policies, in particular to determine reachability properties (e.g., whether a user can eventually be assigned to a role by a group of administrators) and availability properties (e.g., whether a user cannot be removed from a role by a group of administrators) implied by a policy. We first establish the connection between security policy analysis and planning in artificial intelligence. Based partly on this connection, we show that reachability analysis for ARBAC is PSPACE-complete. We also give algorithms and complexity results for reachability and related analysis problems for several categories of ARBAC policies, defined by simple restrictions on the policy language

Several program analysis problems can be cast elegantly as a logic program. In this paper we show how recently-developed techniques for incremental evaluation of logic programs can be refined and used for deriving practical implementations of incremental program analyzers. Incremental program analyzers compute the changes to the analysis information due to small changes in the input program rather than re-analyzing the program. Demand-driven analyzers compute only the information requested by the client analysis/optimization. We describe a framework based on logic programming for implementing program analyses that combines incremental and demand driven techniques. We show the effectiveness of this approach by building a practical incremental and demand-driven context insensitive points-to analysis and evaluating this implementation for analyzing C programs with 10-70K lines of code. Experiments show that our technique can compute the changes to analysis information due to small changes in the input program in, on the average, 6% of the time it takes to reanalyze the program from scratch, and with little space overhead.

Given a logic program P , an unfold/fold program transformation system derives a sequence of programs P = P 0 , P 1 , …, P n , such that P i +1 is derived from P i by application of either an unfolding or a folding step. Unfold/fold transformations have been widely used for improving program efficiency and for reasoning about programs. Unfolding corresponds to a resolution step and hence is semantics-preserving. Folding, which replaces an occurrence of the right hand side of a clause with its head, may on the other hand produce a semantically different program. Existing unfold/fold transformation systems for logic programs restrict the application of folding by placing (usually syntactic) conditions that are sufficient to guarantee the correctness of folding. These restrictions are often too strong, especially when the transformations are used for reasoning about programs. In this article we develop a transformation system (called SCOUT) for definite logic programs that is provably more powerful (in terms of transformation sequences allowed) than existing transformation systems. This extra power is needed for a novel use of logic program transformations: for the verification of a specific class of concurrent systems, called parameterized concurrent systems.Our transformation system is constructed by developing a framework, which is parameterized by a "measure space" and associated measure functions. This framework places no syntactic restriction on the application of folding, and it can be used to derive transformation systems (by fixing the measure space and functions). The power of the system is determined by the choice of the measure space and functions; thus the relative power of different transformation systems can be compared by considering their measure spaces and functions. The correctness of these transformation systems follows from the correctness of the framework. We show that various existing transformation systems can be obtained as instances of our framework. We extend the unfold/fold transformation framework with a goal replacement transformation that allows semantically equivalent conjunctions of atoms to be interchanged. We then derive a new transformation system SCOUT as an instance of the framework and show its power relative to the existing transformation systems. SCOUT has been used to inductively prove temporal properties of parameterized concurrent systems (infinite families of finite state concurrent systems). We demonstrate the use of the additional power of SCOUT in constructing such induction proofs.

The past decade has seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software systems. Recently, there has been increasing interest in applying logic programming techniques to model checking in particular and verification in general. For example, table-based logic programming can be used as an efficient means of performing explicit model checking. Other research has successfully exploited set-based logic program analysis, constraint logic programming, and logic program transformation techniques to verify systems.

Vulnerability analysis is concerned with the problem of identifying weaknesses in computer systems that can be exploited to compromise their security. In this paper we describe a new approach to vulnerability analysis based on model checking. Our approach involves: Formal specification of desired security properties. An example of such a property is “no ordinary user can overwrite system log files”.An abstract model of the system that captures its security-related behaviors. This model is obtained by composing models of system components such as the file system, privileged processes, etc.A verification procedure that checks whether the abstract model satisfies the security properties, and if not, produces execution sequences (also called exploit scenarios) that lead to a violation of these properties. An important benefit of a model-based approach is that it can be used to detect known and as-yet-unknown vulnerabilities. This capability contrasts with previous approaches (such as those used in COPS and SATAN) which mainly address known vulnerabilities. This paper demonstrates our approach by modelling a simplified version of a UNIX-based system, and analyzing this system using model-checking techniques to identify nontrivial vulnerabilities. A key contribution of this paper is to show that such an automated analysis is feasible in spite of the fact that the system models are infinite-state systems. Our techniques exploit some of the latest techniques in model-checking, such as constraint-based (implicit) representation of state-space, together with domain-specific optimizations that are appropriate in the context of vulnerability analysis. Clearly, a realistic UNIX system is much more complex than the one that we have modelled in this paper. Nevertheless, we believe that our results show automated and systematic vulnerability analysis of realistic systems to be feasible in the near future, as model-checking techniques continue to improve.

A new approach for ensuring the security of mobile code is proposed. Our approach enables a mobile-code consumer to understand and formally reason about what a piece of mobile code can do; check if the actions of the code are compatible with his/her security policies; and, if so, execute the code. The compatibility-checking process is automated, but if there are conflicts, consumers have the opportunity to refine their policies, taking into account the functionality provided by the mobile code. Finally, when the code is executed, our framework uses runtime-monitoring techniques to ensure that the code does not violate the consumer's (refined) policies.At the heart of our method, which we call model-carrying code (MCC), is the idea that a piece of mobile code comes equipped with an expressive yet concise model of the code's (security-relevant) behavior. The generation of such models can be automated. MCC enjoys several advantages over current approaches to mobile-code security. It protects consumers of mobile code from malicious or faulty code without unduly restricting the code's functionality. Also, it is applicable to the vast majority of code that exists today, which is written in C or C++. This contrasts with previous approaches such as Java 2 security and proof-carrying code, which are either language-specific or are limited to type-safe languages. Finally, MCC can be combined with existing techniques such as cryptographic signing and proof-carrying code to yield additional benefits.

Tableau-based proof systems can be elegantly specified and directly executed by a tabled Logic Programming (LP) system. Our experience with the XMC model checker shows that such an encoding can be used to search for the existence of a proof very efficiently. However, the users of a tableau system are often interested in getting sufficient evidence (in terms of the tableau proof rules) on why a proof does or does not exist. In this paper, we address the problem of constructing such an evidence without introducing any additional computational overhead to the proof search. A tabled LP system maintains a memo table of "lemmas" that were tried and possibly proved during query evaluation. We propose the concept of justifier for extracting sufficient evidence for the truth or falsehood of literals in a logic program, by post-processing the memo tables created during query evaluation. Based on this logic program justifier, we showhow to construct evidence for the presence/absence of tableau in a tableau-based proof system. Weprovide experimental results showing the effectiveness of the justifier in constructing succinct evidence of the evaluation performed by the XMC model checker. Finally we discuss the role of the justifier as a programming abstraction for encoding efficient algorithms as tabled logic programs.

Presents a computational framework based on tabled resolution and constraint processing for verifying real-time systems. We also discuss the implementation of this framework in the context of the XMC/RT (eXtended Model Checker/Real-Time) verification tool. For systems specified using timed automata, XMC/RT offers backward and forward reachability analysis, as well as timed modal mu-calculus model checking. It can also handle timed infinite-state systems, such as those with unbounded message buffers, provided the set of reachable states is finite. We illustrate this capability on a real-time version of the Leader Election protocol. Finally, XMC/RT can function as a model checker for untimed systems. Despite this versatility, preliminary benchmarking experiments indicate that XMC/RT's performance remains competitive with that of other real-time verification tools.

WC propose Concurrent Transaction Logic (C7X) as the language for specifying, analyzing, and scheduling of workflows.We show that both local and global properties of worktlows can be naturally represented as C7X formulas and reasoning can be done with the use of the proof theory and the semantics of this logic, We describe a transformation that leads to an eilicicnt algorithm for scheduling worldlows in the presencc of global temporal constraints, which leads to decision proccdurcs for dealing with several safety related properties such as whether every valid execution of the workflow satisfits a particular property or whether a worlcfiow execution is consistent with some given global constraints on the ordering of events in a workflow.We also provide tight complexity results on the running times of these algorithms.

This paper describes E QUALS , a fast parallel implementation of a lazy functional language on a commercially available shared-memory parallel machine, the Sequent Symmetry. In contrast to previous implementations, we propagate normal form demand at compile time as well as run time, and detect parallelism automatically using strictness analysis. The E QUALS implementation indicates the effectiveness of NF-demand propagation in identifying significant parallelism and in achieving good sequential as well as parallel performance. Another important difference between E QUALS and previous implementations is the use of reference counting for memory management, instead of mark-and-sweep or copying garbage collection. Implementation results show that reference counting leads to very good scalability and low memory requirements, and offers sequential performance comparable to generational garbage collectors. We compare the performance of E QUALS with that of other parallel implementations (the 〈 v , G 〉-machine and GAML) as well as with the performance of SML/NJ, a sequential implementation of a strict language.

Many analysis problems can be cast in the form of evaluating minimal models of a logic program. Although such formulations are appealing due to their simplicity and declarativeness, they have not been widely used in practice because, either existing logic programming systems do not guarantee completeness, or those that do have been viewed as too inefficient for integration into a compiler. The objective of this paper is to re-examine this issue in the context of recent advances in implementation technologies of logic programming systems.We find that such declarative formulations can indeed be used in practical systems, when combined with the appropriate tool for evaluation. We use existing formulations of analysis problems --- groundness analysis of logic programs, and strictness analysis of functional programs --- in this case study, and the XSB system, a table-based logic programming system, as the evaluation tool of choice. We give experimental evidence that the resultant groundness and strictness analysis systems are practical in terms of both time and space. In terms of implementation effort, the analyzers took less than 2 man-weeks (in total), to develop, optimize and evaluate. The analyzer itself consists of about 100 lines of tabled Prolog code and the entire system, including the components to read and preprocess input programs and to collect the analysis results, consists of about 500 lines of code.

The efficiency of resolution-based logic programming languages, such as Prolog, depends critically on selecting and executing sets of applicable clause heads to resolve against subgoals. Traditional approaches to this problem have focused on using indexing to determine the smallest possible applicable set. Despite their usefulness, these approaches ignore the nondeterminism inherent in many programming languages to the extent that they do not attempt to optimize execution after the applicable set has been determined. Unification factoring seeks to rectify this omission by regarding the indexing and unification phases of clause resolution as a single process. This article formalizes that process through the construction of factoring automata . A polynomial-time algorithm is given for constructing optimal factoring automata that preserve the clause selection strategy of Prolog. More generally, when the clause selection strategy is not fixed, constructing such an optimal automaton is shown to be NP-complete, solving an open trie minimization problem. Unification factoring is implemented through a source code transformation that preserves the full semantics of Prolog. This transformation is specified in the article, and using it, several well-known programs show significant performance improvements across several different systems. A prototype of unification factoring is available by anonymous ftp.

Interpretation of logic programs using symbolic constraints has attracted a lot of attention lately since such layers that enables us to modularize not only our algorithms and implementations, but also the proof efforts.Prototype implementation of our framework shows that it scales very well to large domains, and furthermore, compares favorably with existing implementations of other analysis methods.

The efficiency of resolution-based logic programming languages, such as Prolog, depends critically on selecting and executing sets of applicable clause heads to resolve against subgoals. Traditional approaches to this problem have focused on using indexing to determine the smallest possible applicable set. Despite their usefulness, these approaches ignore the non-determinism inherent in many programming languages to the extent that they do not attempt to optimize execution after the applicable set theory has been determined.