Search

Polarity classification of words is important for applications such as Opinion Mining and Sentiment Analysis. A number of sentiment word/sense dictionaries have been manually or (semi)automatically constructed. We notice that these sentiment dictionaries have numerous inaccuracies. Besides obvious instances, where the same word appears with different polarities in different dictionaries, the dictionaries exhibit complex cases of polarity inconsistency, which cannot be detected by mere manual inspection. We introduce the concept of polarity consistency of words/senses in sentiment dictionaries in this paper. We show that the consistency problem is NP-complete. We reduce the polarity consistency problem to the satisfiability problem and utilize two fast SAT solvers to detect inconsistencies in a sentiment dictionary. We perform experiments on five sentiment dictionaries and WordNet to show inter- and intra-dictionaries inconsistencies.

We consider the model-checking problem for a particular class of parameterized systems: systems that consist of arbitrary numbers of components. The task is to show correctness regardless of the number of components. The term parameterized refers to the fact that the size of the system is a parameter of the verification problem. Examples of parameterized systems include mutual exclusion algorithms, bus protocols, networking protocols, cache coherence protocols, web services, and sensor networks. In this chapter, we will give four examples of techniques that have been used (among many others) for the verification of parameterized systems.

The design of security protocols is extremely subtle and vulnerable to potentially devastating flaws. As a result, many tools and techniques for the automated verification of protocol designs have been developed. Unfortunately, these tools don’t have the ability to model and reason about protocols with randomization, which are becoming increasingly prevalent in systems providing privacy and anonymity guarantees. The security guarantees of these systems are often formulated by means of the indistinguishability of two protocols. In this paper, we give the first practical algorithms for model checking indistinguishability properties of randomized security protocols against the powerful threat model of a bounded Dolev-Yao adversary. Our techniques are implemented in the Stochastic Protocol ANalayzer (Span) and evaluated on several examples. As part of our evaluation, we conduct the first automated analysis of an electronic voting protocol based on the 3-ballot design.

Intelligent Transportation Systems envision a networked environment consisting of vehicles, the infrastructure, and hand-held devices (e.g., smart-phones). The environment will enable numerous safety, mobility, and environmental improvement applications. For example, drivers can be warned of dangers in their local environment or when risking to leave their lane. Furthermore, their visibility range can be expanded by providing highly up-to-date information from areas that are currently invisible. For another example, the road weather—up-to-the-minute visibility, precipitation, and pavement condition information—can be provided at high spatial resolution. Intelligent Transportation efforts are currently being undertaken throughout the world. In addition to the IntelliDrive initiative of the US Department of Transportation, similar efforts exist in Europe, Japan, and China. But these efforts are largely decoupled from, and often incognizant of, the advances in spatio-temporal information management. This paper outlines a spatio-temporal data management language, Transportation Query Language (TranQuyl), which will facilitate the specification of a wide variety of queries of interest to travelers, to transportation agencies, and to industry. Queries in TranQuyl may be processed in either client server mode, or mobile peer-to-peer (P2P) mode, or both. TranQuyl will provide support for the specification of uncertainty either quantitatively or qualitatively as fuzzy queries, for example: “retrieve safety/emergency information around me”. In response, query processing should avoid overloading the traveler with information, and instead present only the most relevant answers to the query.

The goal of recent research projects on integrating Web databases has been to enable uniform access to the large amount of data behind query interfaces. Among the tasks addressed are: source discovery, query interface extraction, schema matching, etc. There are also a number of tasks that are commonly ignored or assumed to be apriori solved either manually or by some oracle. These tasks include (1) finding the set of stop words and (2) handling occurrences of "semantic enrichment words" within labels. These two subproblems have a direct impact on determining the synonymy and hyponymy relationships between labels. In (1), a word like "from" is a stop word in general but it is a content word in domains such as Airline and Real Estate. We formulate the stop word problem , prove its complexity and provide an approximation algorithm. In (2), we study the impact of words like AND and OR on establishing semantic relationships between labels (e.g. "departure date and time" is a hypernym of "departure date"). In addition, we develop a theoretical framework to differentiate synonymy relationship from hyponymy relationship among labels involving multiple words. We scrutinize its strength and limitations both analytically and experimentally. We use real data from the Web in our experiments. We analyze over 2300 labels of 220 user interfaces in 9 distinct domains.

SPKI/SDSI is a standard for issuing authorization and name certificates. SPKI/SDSI can be used to implement a Trust Management System, where the policy for resource access is distributively specified by multiple trusted entities. Agents in the system need a formal mechanism for understanding the current state of policy. We present a first order temporal logic, called FTPL for specifying properties of a given SPKI/SDSI policy state. We also present algorithms to check if a SPKI/SDSI policy state satisfies a property specified in FTPL.

Today, millions of people employ powerful search engines such as Google to retrieve information from the Web on a daily basis. In spite of the success, there are problems associated with such powerful search engines. First, the number of pages which are captured by a single search engine is a few billion, while it has been reported that the entire Web has about 500 billion pages and is rapidly growing. Thus, the coverage of the Web by a single search engine is rather small. Second, an index database has to be built to contain the key information of the captured Web pages. This database is huge and takes substantial amount of time to refresh its contents. Thus, it is not surprising that substantial amount of information in the indexed database can be weeks out-of-date. Third, in order to retrieve information from the large database when there are a large number of queries, enormous hardware resources are needed. It has been reported that Google is utilizing many thousands of computers.

In this paper, we consider databases representing information about moving objects (e.g., vehicles), particularly their location. We address the problems of updating and querying such databases. Specifically, the update problem is to determine when the location of a moving object in the database (namely its database location) should be updated. We answer this question by proposing an information cost model that captures uncertainty, deviation, and communication. Then we analyze dead-reckoning policies, namely policies that update the database location whenever the distance between the actual location and the database location exceeds a given threshold, x. Dead-reckoning is the prevalent approach in military applications, and our cost model enables us to determine the threshold x. We propose several dead-reckoning policies and we compare their performance by simulation. Then we consider the problem of processing range queries in the database. An example of a range query is ‘retrieve the objects that are currently inside a given polygon P′. We propose a probabilistic approach to solve the problem. Namely, the DBMS will answer such a query with a set of objects, each of which is associated with a probability that the object is inside P.

In this paper, we present a unified formalism, based on Past Temporal Logic, for specifying conditions and events in the rules for active database system. This language permits specification of many time varying properties of database systems. It also permits specification of temporal aggregates. We present an efficient incremental algorithm for detecting conditions specified in this language. The given algorithm, for a subclass of the logic, was implemented on top of Sybase.

The Web has plenty of reviews, comments and reports about products, services, government policies, institutions, etc. The opinions expressed in these reviews influence how people regard these entities. For example, a product with consistently good reviews is likely to sell well, while a product with numerous bad reviews is likely to sell poorly. Our aim is to build a sentimental word dictionary, which is larger than existing sentimental word dictionaries and has high accuracy. We introduce rules for deduction, which take words with known polarities as input and produce synsets (a set of synonyms with a definition) with polarities. The synsets with deduced polarities can then be used to further deduce the polarities of other words. Experimental results show that for a given sentimental word dictionary with D words, approximately an additional 50% of D words with polarities can be deduced. An experiment is conducted to find the accuracy of a random sample of the deduced words. It is found that the accuracy is about the same as that of comparing the judgment of one human with that of another.

We present the first sound program transformation approach for automatically transforming the code of a legacy web application to employ PREPARE statements in place of unsafe SQL queries. Our approach therefore opens the way for eradicating the SQL injection threat vector from legacy web applications. This extended abstract is based on our paper[4] that appeared in the Financial Cryptography and Data Security (FC'2010) conference.

Methods are given for automatically verifying temporal properties of concurrent systems containing an arbitrary number of finite-state processes that communicate using CCS actions. TWo models of systems are considered. Systems in the first model consist of a unique control process and an arbitrary number of user processes with identical definitions. For this model, a decision procedure to check whether all the executions of a process satisfy a given specification is presented. This algorithm runs in time double exponential in the sizes of the control and the user process definitions. It is also proven that it is decidable whether all the fair executions of a process satisfy a given specification. The second model is a special case of the first. In this model, all the processes have identical definitions. For this model, an efficient decision procedure is presented that checks if every execution of a process satisfies a given temporal logic specification. This algorithm runs in time polynomial in the size of the process definition. It is shown how to verify certain global properties such as mutual exclusion and absence of deadlocks. Finally, it is shown how these decision procedures can be used to reason about certain systems with a communication network.

Networks of sensors are used in many different fields, from industrial applications to surveillance applications. A common feature of these applications is the necessity of a monitoring infrastructure that analyzes a large number of data streams and outputs values that satisfy certain constraints.In this paper, we present a query processor for monitoring queries in a network of sensors with prediction functions. Sensors communicate their values according to a threshold policy, and the proposed query processor leverages prediction functions to compare tuples efficiently and to generate answers even in the absence of new incoming tuples. Two types of constraints are managed by the query processor: window-join constraints and value constraints. Uncertainty issues are considered to assign probabilistic values to the results returned to the user. Moreover, we have developed an appropriate buffer management strategy, that takes into account the contributions of the prediction functions contained in the tuples. We also present some experimental results that show the benefits of the proposal.

Runtime monitoring systems play an important role in system security, and verification efforts that ensure that these systems satisfy certain desirable security properties are growing in importance. One such security property is complete mediation, which requires that sensitive operations are performed by a piece of code only after the monitoring system authorizes these actions. In this paper, we describe a verification technique that is designed to check for the satisfaction of this property directly on code from Java standard libraries. We describe a tool CMV that implements this technique and automatically checks shrink-wrapped Java bytecode for the complete mediation property. Experimental results on running our tool over several thousands of lines of bytecode from the Java libraries suggest that our approach is scalable, and leads to a very significant reduction in human efforts required for system verification.

A substantially large class of programs operate in distributed and real-time environments, and an integral part of their correctness specification requires the expression of time-critical properties that relate the occurrence of events of the system. We focus on the formal specification and reasoning about the correctness of such programs. We popose a system of temporal logic, RTCTL (Real-Time Computation Tree Logic), that allows the melding of qualitative temporal assertions together with real-time constraints to permit specification and reasoning at the twin levels of abstraction: qualitative and quantitative. We show that several practically useful correctness properties of temporal systems, which need to express timing as an essential part of their functionality requirements, can be expressed in RTCTL. We also develop a model-checking algorithm for RTCTL whose complexity is linear in the size of the RTCTL specification formula and in the size of the global state-space graph. Finally, we present an optimal, exponential time tableau-based decision procedure for the satisfiability of RTCTL formulae, which can be used as the basis of a technique to automate the synthesis of real-time programs from specifications.

In this paper we examine the dissemination of availability reports about resources in mobile peer-to-peer networks, where moving objects communicate with each other via short-range wireless transmission. Each disseminated report represents an observed spatial-temporal event, and the relevance of the report to a moving object decays as the age of the reported resource and the distance from its location increase. We propose an opportunistic approach, in which an object propagates the reports it carries (namely the information that it has about these resources) to encountered objects and obtains new reports in exchange. Least relevant reports are discarded after each exchange so as to limit the communication data volume of future exchanges. Our theoretical and experimental analysis indicates that the opportunistic dissemination algorithm automatically limits the global distribution of a report to a bounded spatial area and to the duration for which it is of interest. We propose two variants of the opportunistic dissemination algorithm and compare them with the traditional client-server architecture in terms of data accuracy. The proposed system has the potential to create a completely new information marketplace.

Software is often being assembled using third-party components where the developers have little knowledge of, and even less control over, the internals of the components comprising the overall system. One obstacle to composing agents is that current formal methods are mainly concerned with "closed" systems that are built from the ground up. Such systems are fully under the control of the user.Hence, problems arising from ill-specified components can be resolved by a close inspection of the systems. When composing systems using "off-the-shelf" components, this is often no longer the case.The paper addresses the problem of under-specification, where an off-the-shelf component does only what it claims to do, however, it claims more behaviors than it actually has and that one wishes for, some of which may render it useless. Given such an under-specified module, we propose a method to automatically synthesize some safety properties from it that would tame its "bad" behaviors. The advantage of restricting to safety properties is that they are monitorable.The safety properties are derived using an automata-theoretic approach. We show that, when restricting to ω-regular languages, there is no maximal safety property. For this case we construct a sequence of increasingly larger safety properties. We also show how to construct an infinite-state automata that can capture any safety property that is contained in the original specifications.

A.P. Sistla et al. (1997) designed a similarity-based video retrieval system. Queries were specified in a language called the Hierarchical Temporal Language (HTL). In this paper, we present several extensions of HTL. These extensions include queries that can have the negation operator and any other logical and temporal operators such as disjunction. Efficient algorithms for processing queries in the extended language are also presented.

We propose a data model for representing moving objects in database systems. It is called the Moving Objects Spatio-Temporal (MOST) data model. We also propose Future Temporal Logic (FTL) as the query language for the MOST model, and devise an algorithm for processing FTL queries in MOST.

Similarity based retrieval from sequence databases is of importance in many applications such as time-series, video and textual databases. In this paper, automata based formalisms are introduced for specifying queries over such databases. Various measures defining the distance of a database sequence from an automaton are defined. Efficient methods for similarity based retrieval are presented for each of the distance measures. These methods answer nearest neighbor queries (i.e. retrieval of k closest subsequences), or range queries (i.e., retrieval of all sequences with in a given distance).

Similarity based retrieval is of major importance for querying sequence databases. We consider formalisms based on automata, temporal logics and regular expressions for querying such databases. We define two different types of similarity measures--syntax based and semantics based. These measures are divided into a spectrum of measures based on the vector distance function that is employed. We consider norm vector distance functions and give efficient query processing algorithms when these measures are employed.

Consider a database that represents information about moving objects and their location. For example, for a database representing the location of taxi-cabs a typical query may be: retrieve the free cabs that are currently within 1 mile of 33 N. Michigan Ave., Chicago (to pick-up a customer); or for a trucking company database a typical query may be: retrieve the trucks that are currently within 1 mile of truck ABT312 (which needs assistance); or for a database representing the current location of objects in a battlefield a typical query may be: retrieve the friendly helicopters that are in a given region, or, retrieve the friendly helicopters that are expected to enter the region within the next 10 minutes. The queries may originate from the moving objects, or from stationary users. We will refer to applications with the above characteristics as moving-objects-database (MOD) applications, and to queries as the ones mentioned above as MOD queries. In the military MOD applications arise in the context of the digital battlefield (see [1]), and in the civilian industry they arise in transportation systems. For example, Omnitracs developed by Qualcomm (see[2]) is a commercial system used by the transportation industry, which enables MOD functionality. It provides location management by connecting vehicles (e.g. trucks), via satellites, to company databases. The vehicles are equipped with a Global Positioning System (GPS), and they automatically and periodically report their location.

In this paper we propose a data model for representing moving objects with uncertain positions in database systems. It is called the Moving Objects Spatio-Temporal (MOST) data model. We also propose Future Temporal Logic (FTL) as the query language for the MOST model, and devise an algorithm for processing FTL queries in MOST.

G-tree is a data structure designed to provide multidimensional access in databases. It has the self-balancing property of B+-tree. In this paper, performance evahtation of G-tree is provided for various data distributions. For point queries, the experiments show that its retrieval and update performance is similar to that of l?+-trees independently of the data distribution. For range queries, the performance varies significantly with the data distributions. While the performance is good for the 2-dimensional case, it deteriorates as the number of dimensions increases. This empirical evidence is confirmed by an analytical proof, which also yields a simple way of computing the expected number of data pages accessed. This analytical result which shows that the number of data pages accessed by a range query increases exponentially with the number of dimensions applies to many multi-dimensional schemes. We also apply the G-tree to fuzzy databases and show empirically that it has good performance for imprecise queries on relatively imprecise data. But it is less efficient for precise queries on relatively precise data.