CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems

Boolean equation systems (Bess) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking and model checking. These problems can be solved on the fly (i.e., without constructing explicitly the state space of the system under analysis) by using a demand-driven construction and resolution of the corresponding Bes. In this article, we present a generic software library dedicated to on-the-fly resolution of alternation-free Bess. Four resolution algorithms are currently provided by the library: algorithms A1 and A2 are general, the latter being optimized to produce small-depth diagnostics, whereas algorithms A3 and A4 are specialized for handling acyclic and disjunctive/conjunctive Bess in a memory-efficient way. The library has been developed within the Cadp verification toolbox using the generic Open/Caesar environment and is currently used for three purposes: on-the-fly equivalence checking modulo five widely used equivalence relations, on-the-fly model checking of regular alternation-free modal μ-calculus, and on-the-fly reduction of state spaces based on τ-confluence .     

K: A heuristic search algorithm for finding the k shortest paths

We present a directed search algorithm, called K^?, for finding the k shortest paths between a designated pair of vertices in a given directed weighted graph. K^? has two advantages compared to current k-shortest-paths algorithms. First, K^? operates on-the-fly, which means that it does not require the graph to be explicitly available and stored in main memory. Portions of the graph will be generated as needed. Second, K^? can be guided using heuristic functions. We prove the correctness of K^? and determine its asymptotic worst-case complexity when using a consistent heuristic to be the same as the state of the art, , with respect to both runtime and space, where n is the number of vertices and m is the number of edges of the graph. We present an experimental evaluation of K^? by applying it to route planning problems as well as counterexample generation for stochastic model checking. The experimental results illustrate that due to the use of heuristic, on-the-fly search K^? can use less time and memory compared to the most efficient k-shortest-paths algorithms known so far.     

On-the-Fly Model Checking Under Fairness that Exploits Symmetry

An on-the-fly algorithm for model checking under fairness is presented. The algorithm utilizes symmetry in the program to reduce the state space, and employs novel techniques that make the on-the-fly model checking feasible. The algorithm uses state symmetry and eliminates parallel edges in the reachability graph. Experimental results demonstrating dramatic reductions in both the running time and memory usage are presented.     

Symmetry reductions for model checking of concurrent dynamic software

Symmetry reduction techniques exploit symmetries that occur during the execution of a system in order to minimize its state space for efficient verification of temporal logic properties. This paper presents a framework for concisely defining and evaluating symmetry reductions currently used in software model checking, involving heap objects and processes. An on-the-fly state space exploration algorithm combining both techniques will also be presented. Second, the relation between symmetry and partial-order reductions is investigated, showing how ones strengths can be used to compensate for the others weaknesses. The symmetry reductions presented here were implemented in the dSPIN model-checking tool. We also performed a number of experiments that show significant progress in reducing the cost of finite-state software verification.     

Photobook generation algorithms

Photobooks are comfortable and attractive solution for personal photo printing and storing. Photobook generation requires a lot of manual operations and takes a lot of time. Automation process will involve new users and allow making more photobooks. The algorithms should be quite fast, adjusted by user’s predilections and habits and ensure satisfied quality of work. We propose several adaptive photobook generation algorithms: photo quality recognition based on active learning, event-aware photo grouping, attractive photos selection, automatic photos layout through photobook pages, collage generation. We also suggest approaches to algorithms adjustment by user preferences on-the-fly.     

Efficient Algorithms for Dynamic Allocation of Distributed Memory

We consider the problem of dynamically allocating and deallocating local memory resources among multiple users in a parallel or distributed system. Given a group of independent users and a collection of interconnected local memory devices, we want to render the fragmentation of the memory resources irrelevant by allowing any user to allocate space for his or her purposes as long as there is space available anywhere in the system. In effect, we would like it to appear to the users as though they are allocating memory from a single central pool of memory, even though the space is distributed throughout the system. Our goal is to devise an on-line allocation algorithm that minimizes two cost measures: first, the fraction of unused space , which arises due to fragmentation of the memory; second, the slowdown needed by the system to service user requests, which arises due to the contention for access to the memory devices. We solve this distributed dynamic allocation problem in near-optimal fashion by devising an algorithm that allows the memory to be used to 100% of capacity despite the fragmentation and guarantees that service delays will always be within a constant factor of optimal. The algorithm is completely on-line (no foreknowledge of user activity is assumed) and can accommodate any sequence of allocations and deallocations by the users that does not violate global memory bounds. We also consider the distributed dynamic allocation problem in the more restrictive setting where the local memory devices are connected by a low-degree fixed-connection network, rather than being fully interconnected. In this case, communication costs must be more explicitly considered in our allocation algorithms. We give allocation algorithms for butterfly and hypercube networks, and prove necessary and sufficient conditions on the total amount of memory space needed for near-optimal algorithms to exist. Received November 5, 1996; revised December 10, 1997.     

Formal Verification of an Executable LTL Model Checker with Partial Order Reduction

We present a formally verified and executable on-the-fly LTL model checker that uses ample set partial order reduction. The verification is done using the proof assistant Isabelle/HOL and covers everything from the abstract correctness proof down to the generated SML code. Building on Doron Peled’s paper “Combining Partial Order Reductions with On-the-Fly Model-Checking”, we formally prove abstract correctness of ample set partial order reduction. This theorem is independent of the actual reduction algorithm. We then verify a reduction algorithm for a simple but expressive fragment of Promela. We use static partial order reduction, which allows separating the partial order reduction and the model checking algorithms regarding both the correctness proof and the implementation. Thus, the Cava model checker that we verified in previous work can be used as a back end with only minimal changes. Finally, we generate executable SML code using a stepwise refinement approach. We test our model checker on some examples, observing the effectiveness of the partial order reduction algorithm.     

An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation

This paper presents a partial order reduction algorithm called Twophase that generates a significantly reduced state space on a large class of practical protocols over alternative algorithms in its class. The reduced state-space generated by Twophase preserves all CTL*-X assertions. Twophase achieves this reduction by following an alternative implementation of the proviso step. In particular, Twophase avoids the in-stack check that other tools use in order to realize the proviso step. In this paper, we demonstrate that the in-stack check is inefficient in practice, and demonstrate a much simpler alternative method of realizing the proviso. Twophase can be easily combined with an on-the-fly model-checking algorithm to reduce memory requirements further. A simple but powerful selective caching scheme can also be easily added to Twophase.A version of Twophase using on-the-fly model-checking and selective caching has been implemented in a model-checker called PV (Protocol Verifier) and is in routine use on large problems. PV accepts a proper subset of Promela and a never automaton expressing the LTL-X assertion to be verified. PV has helped us complete full state-space search several orders of magnitude faster than all alternative tools available in its class on dozens of real protocols. PV has helped us detect bugs in real Distributed Shared Memory cache coherency protocols that were missed during incomplete search using alternate tools.     

Optimal Algorithms for Finding User Access Sessions from Very Large Web Logs

Although efficient identification of user access sessions from very large web logs is an unavoidable data preparation task for the success of higher level web log mining, little attention has been paid to algorithmic study of this problem. In this paper we consider two types of user access sessions, interval sessions and gap sessions. We design two efficient algorithms for finding respectively those two types of sessions with the help of some proposed structures. We present theoretical analysis of the algorithms and prove that both algorithms have optimal time complexity and certain error-tolerant properties as well. We conduct empirical performance analysis of the algorithms with web logs ranging from 100 megabytes to 500 megabytes. The empirical analysis shows that the algorithms just take several seconds more than the baseline time, i.e., the time needed for reading the web log once sequentially from disk to RAM, testing whether each user access record is valid or not, and writing each valid user access record back to disk. The empirical analysis also shows that our algorithms are substantially faster than the sorting based session finding algorithms. Finally, optimal algorithms for finding user access sessions from distributed web logs are also presented.     

On the constructive orbit problem

Symmetry reduction techniques aim to combat the state-space explosion problem for model checking by restricting search to representative states from equivalence classes with respect to a group of symmetries. The standard approach to representative computation involves converting a state to its minimal image under a permutation group G, before storing the state. This is known as the constructive orbit problem (COP), and is NP{\mathit{NP}} hard. It may be possible to solve the COP efficiently if G is known to have certain structural properties: in particular if G is isomorphic to a full symmetry group, or G is a disjoint/wreath product of subgroups. We extend existing results on solving the COP efficiently for fully symmetric groups, and investigate the problem of automatically classifying an arbitrary permutation group as a disjoint/wreath product of subgroups. We also present an approximate COP strategy based on local search, and some computational group-theoretic optimisations to improve the basic approach of solving the COP by symmetry group enumeration. Experimental results using the TopSPIN symmetry reduction package, which interfaces with the computational group-theoretic system GAP, illustrate the effectiveness of our techniques.     

Combining Local and Global Model Checking

The verification process of reactive systems in local model checking [1,7] and in explicit state model checking is[13,15] on-the-fly. Therefore only those states of a system have to be traversed that are necessary to prove a property. In addition, if the property does not hold, than often only a small subset of the state space has to be traversed to produce a counterexample. Global model checking [6,23] and, in particular, symbolic model checking [4,22] can utilize compact representations of the state space, e.g. BDDs [3], to handle much larger designs than what is possible with local and explicit model checking. We present a new model checking algorithm for LTL that combines both approaches. In essence, it is a generalization of the tableau construction of [1] that enables the use of BDDs but still is on-the-fly.     

Exploiting equivalence reduction and the sweep-line method for detecting terminal states

State-space exploration is one of the main approaches to computer-aided verification and analysis of finite-state systems. It is used to reason about a wide range of properties during the design phase of a system, including system deadlocks. Unfortunately, state-space exploration needs to handle huge state spaces for most practical systems. Several state-space reduction methods have been developed to tackle this problem. In this paper, we develop algorithms for combining two of these methods: state equivalence class reduction and the sweep-line. The algorithms allow deadlocks to be detected by recording terminal states of the system on-the-fly during state-space exploration. We derive expressions for the complexity of the algorithms and demonstrate their usefulness with an industrial case study. Our results show that the combined method achieves at least a six-fold reduction of the state space for interesting parameter values compared with either method used in isolation while still proving the desired system property of the terminal states. The runtime performance of the combined method is almost the same as that of the equivalence class method over the chosen parameter range. Moreover, the improvement in space reduction increases with increased parameter values.     

Design,development and evaluation of a human-computer trust scale

ABSTRACT

New technologies, data, and algorithms impact nearly every aspect of daily life. Unfortunately, many of these algorithms operate like black boxes and cannot explain their results even to their programmers, let alone to end-users. As more and more tasks get delegated to such intelligent systems and the nature of user interactions with them becomes increasingly complex, it is important to understand the amount of trust that a user is willing to place on such systems. However, attempts at quantifying trust have either been limited in their scope or not empirically thorough. To address this, we build on prior work which empirically modelled trust in user-technology interactions and describe the development and evolution of a human computer trust scale. We present results of two studies (N=118 & N=183) which were undertaken to assess the reliability and validity of the proposed scale. Our study contributes to the literature by (a) developing a multi-dimensional scale to assess user trust in HCI and (b) being the first study to use the concept of design fiction and future scenarios to study trust.     

View management in multimedia databases

Abstract. Though there has been extensive work on multimedia databases in the last few years, there is no prevailing notion of a multimedia view, nor there are techniques to create, manage, and maintain such views. Visualizing the results of a dynamic multimedia query or materializing a dynamic multimedia view corresponds to assembling and delivering an interactive multimedia presentation in accordance with the visualization specifications. In this paper, we suggest that a non-interactive multimedia presentation is a set of virtual objects with associated spatial and temporal presentation constraints. A virtual object is either an object, or the result of a query. As queries may have different answers at different points in time, scheduling the presentation of such objects is nontrivial. We then develop a probabilistic model of interactive multimedia presentations, extending the non-interactive model described earlier. We also develop a probabilistic model of interactive visualization where the probabilities reflect the user profiles, or the likelihood of certain user interactions. Based on this probabilistic model, we develop three utility-theoretic based types of prefetching algorithms that anticipate how users will interact with the presentation. These prefetching algorithms allow efficient visualization of the query results in accordance with the underlying specification. We have built a prototype system that incorporates these algorithms. We report on the results of experiments conducted on top of this implementation. Received June 10, 1998 / Accepted November 10, 1999     

How efficiently can room at the bottom be traded away for speed at the top?

Given exponential 2 ⁿ space, we know that an Adleman-Lipton computation can decide many hard problems – such as boolean formula and boolean circuit evaluation – in a number of steps that is linear in the problem size n. We wish to better understand the process of designing and comparing bio-molecular algorithms that trade away weakly exponential space to achieve as low a running time as possible, and to analyze the efficiency of their space and time utilization relative to those of their best extant classical/bio-molecular counterparts. We propose a randomized framework which augments that of the sticker model of Roweis et al. to provide an abstract setting for analyzing the space-time efficiency of both deterministic and randomized bio-molecular algorithms. We explore its power by developing and analyzing such algorithms for theCovering Code Creation (CCC) and k-SAT problems. In the process, we uncover new classical algorithms for CCC andk-SAT that, while exploiting the same space-time trade-off as the best previously known classical algorithms, are exponentially more efficient than them in terms of space-time product utilization. This work indicates that the proposed abstract bio-molecular setting for randomized algorithm design provides a logical tool of independent interest. This revised version was published online in June 2006 with corrections to the Cover Date.     

Direction-based surrounder queries for mobile recommendations

Location-based recommendation services recommend objects to the user based on the user’s preferences. In general, the nearest objects are good choices considering their spatial proximity to the user. However, not only the distance of an object to the user but also their directional relationship are important. Motivated by these, we propose a new spatial query, namely a direction-based surrounder (DBS) query, which retrieves the nearest objects around the user from different directions. We define the DBS query not only in a two-dimensional Euclidean space \mathbbE{\mathbb{E}} but also in a road network \mathbbR{\mathbb{R}} . In the Euclidean space \mathbbE{\mathbb{E}} , we consider two objects a and b are directional close w.r.t. a query point q iff the included angle Daqb{\angle aqb} is bounded by a threshold specified by the user at the query time. In a road network \mathbbR{\mathbb{R}} , we consider two objects a and b are directional close iff their shortest paths to q overlap. We say object a dominates object b iff they are directional close and meanwhile a is closer to q than b. All the objects that are not dominated by others based on the above dominance relationship constitute direction-based surrounders (DBSs). In this paper, we formalize the DBS query, study it in both the snapshot and continuous settings, and conduct extensive experiments with both real and synthetic datasets to evaluate our proposed algorithms. The experimental results demonstrate that the proposed algorithms can answer DBS queries efficiently.     

Reverse Shooting Made <Emphasis Type="Italic">Easy</Emphasis>: Automating the Search for the Global Nonlinear Saddle Path

We present the blueprints for a set of innovative reverse shooting algorithms that trap the global saddle path in systems with 2–4 state variables. The solution procedure is built around a new distance mapping and refined simplex algorithms. Since the algorithms are completely reliable and always work in the same way, we have been able to develop canned programs that solve for the global nonlinear saddle path in any model with 2–4 state variables. The programs are written in the spirit of plug and play: the user types in the equations of the model and then waits for the solution.     

On-the-fly, incremental, consistent reading of entire databases

We describe an algorithm to read entire databases with locking concurrency control allowing multiple readersor an exclusive writer. The algorithm runs concurrently with the normal transaction processing (on-the-fly), and locks the entities in the database one by one (incremental). We prove that the algorithm produces consistent pictures of the database. We also show that conflicts between the algorithm and some updates, although necessary, can be resolved.Reading entire databases consistently, on-the-fly, incremental algorithms can avoid the database downtime trade-off between frequent checkpoints and crash recovery delay, thus improving system availability and reliability. Our algorithm reads the database once and writes only to sequential output, lowering its implementation and execution costs. A simple extension runs in parallel on several processors and produces consistent pictures of entire distributed databases.This work was partially supported by the National Science Foundation under Grant No. MCS-8004111.     

Poisson‐Based Weight Reduction of Animated Meshes

While animation using barycentric coordinates or other automatic weight assignment methods has become a popular method for shape deformation, the global nature of the weights limits their use for real‐time applications. We present a method that reduces the number of control points influencing a vertex to a user‐specified number such that the deformations created by the reduced weight set resemble that of the original deformation. To do so we show how to set up a Poisson minimization problem to solve for a reduced weight set and illustrate its advantages over other weight reduction methods. Not only does weight reduction lower the amount of storage space necessary to deform these models but also allows GPU acceleration of the resulting deformations. Our experiments show that we can achieve a factor of 100 increase in speed over CPU deformations using the full weight set, which makes real‐time deformations of large models possible.