The verification of differential privacy algorithms that employ Gaussian distributions is little understood. This paper tackles the challenge of verifying such programs by introducing a novel approach to approximating probability distributions of loop-free programs that sample from both discrete and continuous distributions with computable probability density functions, including Gaussian and Laplace. We establish that verifying $(ε,δ)$-differential privacy for these programs is \emph{almost decidable}, meaning the problem is decidable for all values of $δ$ except those in a finite set. Our verification algorithm is based on computing probabilities to any desired precision by combining integral approximations, and tail probability bounds. The proposed methods are implemented in the tool, DipApprox, using the FLINT library for high-precision integral computations, and incorporate optimizations to enhance scalability. We validate {\ourtool} on fundamental privacy-preserving algorithms, such as Gaussian variants of the Sparse Vector Technique and Noisy Max, demonstrating its effectiveness in both confirming privacy guarantees and detecting violations.

Many synthesis and verification problems can be reduced to determining the truth of formulas over the real numbers. These formulas often involve constraints with integrals in them. To this end, we extend the framework of δ -decision procedures with techniques for handling integrals of user-specified real functions. We implement this decision procedure in the tool ∫dReal, which is built on top of dReal. We evaluate ∫dReal on a suite of problems that include formulas verifying the fairness of algorithms and the privacy and the utility of privacy mechanisms and formulas that synthesize parameters for the desired utility of privacy mechanisms. The performance of the tool in these experiments demonstrates the effectiveness of ∫dReal.

We consider the problem of checking the differential privacy of online randomized algorithms that process a stream of inputs and produce outputs corresponding to each input. This paper generalizes an automaton model called DiP automata [10] to describe such algorithms by allowing multiple real-valued storage variables. A DiP automaton is a parametric automaton whose behavior depends on the privacy budget ∈. An automaton A will be said to be differentially private if, for some D, the automaton is D∈-differentially private for all values of ∈ > 0. We identify a precise characterization of the class of all differentially private DiP automata. We show that the problem of determining if a given DiP automaton belongs to this class is PSPACE-complete. Our PSPACE algorithm also computes a value for D when the given automaton is differentially private. The algorithm has been implemented, and experiments demonstrating its effectiveness are presented.

We introduce an automata model for describing interesting classes of differential privacy mechanisms/algorithms that include known mechanisms from the literature. These automata can model algorithms whose inputs can be an unbounded sequence of real-valued query answers. We consider the problem of checking whether there exists a constant d such that the algorithm described by these automata are dϵ-differentially private for all positive values of the privacy budget parameter ϵ. We show that this problem can be decided in time linear in the automaton's size by identifying a necessary and sufficient condition on the underlying graph of the automaton. This paper's results are the first decidability results known for algorithms with an unbounded number of query answers taking values from the set of reals.

Differential privacy is a mathematical framework for developing statistical computations with provable guarantees of privacy and accuracy. In contrast to the privacy component of differential privacy, which has a clear mathematical and intuitive meaning, the accuracy component of differential privacy does not have a generally accepted definition; accuracy claims of differential privacy algorithms vary from algorithm to algorithm and are not instantiations of a general definition. We identify program discontinuity as a common theme in existing ad hoc definitions and introduce an alternative notion of accuracy parametrized by, what we call, — the of an input x w.r.t. a deterministic computation f and a distance d , is the minimal distance d ( x , y ) over all y such that f ( y )≠ f ( x ). We show that our notion of accuracy subsumes the definition used in theoretical computer science, and captures known accuracy claims for differential privacy algorithms. In fact, our general notion of accuracy helps us prove better claims in some cases. Next, we study the decidability of accuracy. We first show that accuracy is in general undecidable. Then, we define a non-trivial class of probabilistic computations for which accuracy is decidable (unconditionally, or assuming Schanuel’s conjecture). We implement our decision procedure and experimentally evaluate the effectiveness of our approach for generating proofs or counterexamples of accuracy for common algorithms from the literature.

Differential privacy is a de facto standard for statistical computations over databases that contain private data. Its main and rather surprising strength is to guarantee individual privacy and yet allow for accurate statistical results. Thanks to its mathematical definition, differential privacy is also a natural target for formal analysis. A broad line of work develops and uses logical methods for proving privacy. A more recent and complementary line of work uses statistical methods for finding privacy violations. Although both lines of work are practically successful, they elide the fundamental question of decidability.

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.

A probabilistic finite automaton (PFA) A is said to be regular-approximable with respect to (x,y), if there is a regular language that contains all words accepted by A with probability at least x+y, but does not contain any word accepted with probability at most x. We show that the problem of determining if a PFA A is regular-approximable with respect to (x,y) is not recursively enumerable. We then show that many tractable sub-classes of PFAs identified in the literature - hierarchical PFAs, polynomially ambiguous PFAs, and eventually weakly ergodic PFAs - are regular-approximable with respect to all (x,y). Establishing the regular-approximability of a PFA has the nice consequence that its value can be effectively approximated, and the emptiness problem can be decided under the assumption of isolation.

The design of security protocols is extremely subtle and is prone to serious faults. Many tools for automatic analysis of such protocols have been developed. However, none of them have the ability to model protocols that use explicit randomization. Such randomized protocols are being increasingly used in systems to provide privacy and anonymity guarantees. In this talk we consider the problem of automatic verification of randomized security protocols. We consider verification of secrecy and indistinguishability properties under a powerful threat model of Dolev-Yao adversary. We present some complexity bounds on verification of these properties. We also describe practical algorithms for checking indistinguishability. These algorithms have been implemented in the tool SPAN and have been experimentally evaluated. The talk concludes with future challenges. (Joint work with: Matt Bauer, Rohit Chadha and Mahesh Viswanathan)

Model checking of systems formalized using probabilistic models such as discrete time Markov chains (DTMCs) and Markov decision processes (MDPs) can be reduced to computing constrained reachability properties. Linear programming methods to compute reachability probabilities for DTMCs and MDPs do not scale to large models. Thus, model checking tools often employ iterative methods to approximate reachability probabilities. These approximations can be far from the actual probabilities, leading to inaccurate model checking results. In this article, we present a new algorithm and its implementation that improves approximate results obtained by scalable techniques like value iteration to compute exact reachability probabilities.

We consider the problem of verifying the security of finitely many sessions of a protocol that tosses coins in addition to standard cryptographic primitives against a Dolev-Yao adversary. Two properties are investigated here - secrecy, which asks if no adversary interacting with a protocol P can determine a secret sec with probability > 1 - p; and indistinguishability, which asks if the probability observing any sequence 0̅ in P1is the same as that of observing 0̅ in P2, under the same adversary. Both secrecy and indistinguishability are known to be coNP-complete for non-randomized protocols. In contrast, we show that, for randomized protocols, secrecy and indistinguishability are both decidable in coNEXPTIME. We also prove a matching lower bound for the secrecy problem by reducing the non-satisfiability problem of monadic first order logic without equality.

Hidden Markov Chains (HMCs) are commonly used mathematical models of probabilistic systems. They are employed in various fields such as speech recognition, signal processing, and biological sequence analysis. Motivated by applications in stochastic runtime verification, we consider the problem of distinguishing two given HMCs based on a single observation sequence that one of the HMCs generates. More precisely, given two HMCs and an observation sequence, a distinguishing algorithm is expected to identify the HMC that generates the observation sequence. Two HMCs are called distinguishable if for every ε > 0 there is a distinguishing algorithm whose error probability is less than ε. We show that one can decide in polynomial time whether two HMCs are distinguishable. Further, we present and analyze two distinguishing algorithms for distinguishable HMCs. The first algorithm makes a decision after processing a fixed number of observations, and it exhibits two-sided error. The second algorithm processes an unbounded number of observations, but the algorithm has only one-sided error. The error probability, for both algorithms, decays exponentially with the number of processed observations. We also provide an algorithm for distinguishing multiple HMCs.

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 interand intra-dictionaries inconsistencies.

The prolonged lifetime of sensitive data (such as passwords) in applications gives rise to several security risks. A promising approach is to erase sensitive data in an "eager fashion", i.e., as soon as its use is no longer required in the application. This approach of minimizing the lifetime of sensitive data has been applied to sequential programs. In this short paper, we present an extension of the this approach to concurrent programs where the interleaving of threads makes such eager erasures a challenging research problem.

Ensuring the correct behavior of cyber physical systems at run time is of critical importance for their safe deployment. Any malfunctioning of such systems should be detected in a timely manner for further actions. This paper addresses the issue of how quickly a monitor raises an alarm after the occurrence of a failure in cyber physical systems. Towards this end, it introduces a class of systems called exponentially converging monitorable systems. The paper shows that failures in these systems can be detected fast by employing the traditional threshold monitors. It shows that the expected failure detection time for exponentially converging monitorable systems has logarithmic relationship with the inverse of the chosen threshold value. The paper identifies well defined natural classes of these systems. Experimental results are presented that confirm the theoretical results on the relationship between the failure detection time and the chosen threshold values.

We describe SWIPE, an approach to reduce the life time of sensitive, memory resident data in large scale applications written in C. In contrast to prior approaches that used a delayed or lazy approach to the problem of erasing sensitive data, SWIPE uses a novel eager erasure approach that minimizes the risk of accidental sensitive data leakage. SWIPE achieves this by transforming a legacy C program to include additional instructions that erase sensitive data immediately after its intended use. SWIPE is guided by a highly-scalable static analysis technique that precisely identifies the locations to introduce erase instructions in the original program. The programs transformed using SWIPE enjoy several additional benefits: minimization of leaks that arise due to data dependencies; erasure of sensitive data with minimal developer guidance; and negligible performance overheads.

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.

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.

For concurrent probabilistic programs having process-level nondeterminism, it is often necessary to restrict the class of schedulers that resolve nondeterminism to obtain sound and precise model checking algorithms. In this paper, we introduce two classes of schedulers called view consistent and locally Markovian schedulers and consider the model checking problem of concurrent, probabilistic programs under these alternate semantics. Specifically, given a B\"{u}chi automaton $Spec$, a threshold $x$ in $[0,1]$, and a concurrent program $P$, the model checking problem asks if the measure of computations of $P$ that satisfy $Spec$ is at least $x$, under all view consistent (or locally Markovian) schedulers. We give precise complexity results for the model checking problem (for different classes of B\"{u}chi automata specifications) and contrast it with the complexity under the standard semantics that considers all schedulers.

This paper introduces the problem of modeling urban transportation systems in a database where certain aspects of the data are probabilistic in nature. The transportation network is composed of multiple modes (e.g., automobile, bus, train, pedestrian) that the user can alternate between. A trip – a path between an origin and destination subject to some constraints – is the central concept. How these trips and the network can be represented as both a graph and relational model, as well as the requirements for querying are the main contributions of this paper. A set of operators are defined to work over these transportation concepts and they are integrated within a SQL-like syntax to express queries over the uncertain transportation network. Additionally, the paper shows how this model can be integrated within other moving objects and spatio-temporal data models, and how these graph-based queries can be processed. 1.

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 article, we introduce the model of finite state probabilistic monitors (FPM), which are finite state automata on infinite strings that have probabilistic transitions and an absorbing reject state. FPMs are a natural automata model that can be seen as either randomized run-time monitoring algorithms or as models of open, probabilistic reactive systems that can fail. We give a number of results that characterize, topologically as well as with respect to their computational power, the sets of languages recognized by FPMs. We also study the emptiness and universality problems for such automata and give exact complexity bounds for these problems.

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.

A concern about personal information confidentiality typically arises when any desktop application communicates to the external network, for example, to its producer's server for obtaining software version updates. We address this confidentiality concern of end users by an approach called shadow execution. A key property of shadow execution is that it allows applications to successfully communicate over the network while disallowing any information leaks. We describe the design and implementation of this approach for Windows applications. Experiments with our prototype implementation indicate that shadow execution allows applications to execute without inhibiting any behaviors, has acceptable performance overheads while preventing any information leaks.

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.

The continuous run-time monitoring of the behavior of a system is a technique that is used both as a complementary approach to formal verification and testing to ensure reliability, as well as a means to discover emergent properties in a distributed system, like intrusion and event correlation. The monitors in all these scenarios can be abstractly viewed as automata that process a (unbounded) stream of events to and from the component being observed, and raise an ``alarm'' when an error or intrusion is discovered. These monitors indicate the absence of error or intrusion in a behavior implicitly by the absence of an alarm.In this paper we study the power of randomization in run-time monitoring. Specifically, we examine \emph{finite memory} monitoring algorithms that toss coins to make decisions on the behavior they are observing. We give a number of results that characterize, topologically as well as with respect to their computational power, the sets of sequences the monitors permit. We also present results on the complexity of deciding non-emptiness of the set of sequences permitted by a monitor.

Enterprise software systems need to deal with two dominant data models. While object oriented languages (such as Java, C#, C++) are the dominant ways to write business logic, relational databases are the dominant ways to store data. Object-relational (OR) maps are widely used to mediate between these two data models. We present a system to verify correctness of OR maps. We formulate simple correctness conditions for OR maps, and convert these conditions to validity of formulas in first order logic. We have built a verification tool called ROUND TRIP that is able to both validate and find errors in OR maps defined in the ESQL language of the Microsoft EDM data model.

Recently, there are many e-commerce search engines that return information from Web databases. Unlike text search engines, these e-commerce search engines have more complicated user interfaces. Our aim is to construct automatically a natural query user interface that integrates a set of interfaces over a given domain of interest. For example, each airline company has a query interface for ticket reservation and our system can construct an integrated interface for all these companies. This will permit users to access information uniformly from multiple sources. Each query interface from an e-commerce search engine is designed so as to facilitate users to provide necessary information. Specifically, (1) related pieces of information such as first name and last name are grouped together and (2) certain hierarchical relationships are maintained. In this paper, we provide an algorithm to compute an integrated interface from query interfaces of the same domain. The integrated query interface can be proved to preserve the above two types of relationships. Experiments on five domains verify our theoretical study.

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.

Symmetry reduction methods exploit symmetry in a system in order to efficiently verify its temporal properties. Two problems may prevent the use of symmetry reduction in practice: (1) the property to be checked may distinguish symmetric states and hence not be preserved by the symmetry, and (2) the system may exhibit little or no symmetry. In this article, we present a general framework that addresses both of these problems. We introduce "Guarded Annotated Quotient Structures" for compactly representing the state space of systems even when those are asymmetric. We then present algorithms for checking any temporal property on such representations, including non-symmetric properties.

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).

The article presents the SMC system. SMC can be used for checking safety and liveness properties of concurrent programs under different fairness assumptions. It is based on explicit state enumeration. It combats the state explosion by exploiting symmetries of the input concurrent program, usually present in the form of identical processes, in two different ways. Firstly, it reduces the number of explored states by identifying those states that are equivalent under the symmetries of the system; this is called process symmetry . Secondly, it reduces the number of edges explored from each state, in0 the reduced state graph, by exploiting the symmetry of a single state; this is called state symmetry . SMC works in an on-the-fly manner; it constructs the reduced state graph as and when it is needed. This method facilitates early termination, speeds up model checking, and reduces memory requirements. We employed SMC to check the correctness of, among other standard examples, the Link Layer part of the IEEE Standard 1394 “Firewire” high-speed serial bus protocol. SMC found deadlocks in the protocol. SMC was also to check certain liveness properties. A report on the case study is included in the article.

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.

Abstract. The paper proposes an induction based approach, that employs automata as inductive invariants, for verifying safety and liveness properties of linear networks of arbitrary size. The proposed method has been shown to be complete for verifying safety properties. Automated methods that check for correcteness of such families of networks are proposed. These methods are based on generating an invariant automaton from the correctness property which is also specified by an automaton. These methods have been implemented and successfully tested on some examples.

We present an incremental algorithm for model checking the real-time systems against the requirements specified in the real-time extension of modal mu-calculus. Using this algorithm, we avoid the repeated construction and analysis of the whole state-space during the course of evolution of the system from time to time. We use a finite representation of the system, like most other algorithms on real-time systems. We construct and update a graph (called TSG) that is derived from the region graph and the formula. This allows us to halt the construction of this graph when enough nodes have been explored to determine the truth of the formula. TSG is minimal in the sense of partitioning the infinite state space into regions and it expresses a relation on the set of regions of the partition. We use the structure of the formula to derive this partition. When a change is applied to the timed automaton of the system, we find a new partition from the current partition and the TSG with minimum cost.

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.

The concept of software architecture has recently emerged as a new way to improve our ability to effectively construct large scale software systems. However, there is no formal architecture specification language available to model and analyze temporal properties of complex real-time systems. In this paper, an object-oriented logic-based architecture specification language for real-time systems is discussed. Representation of the temporal properties and timing constraints, and their integration with the language to model real-time concurrent systems is given. Architecture based specification languages enable the construction of large system architectures and provide a means of testing and validation. In general, checking the timing constraints of real-time systems is done by applying model checking to the constraint expressed as a formula in temporal logic. The complexity of such a formal method depends on the size of the representation of the system. It is possible that this size could increase exponentially when the system consists of several concurrently executing real-time processes. This means that the complexity of the algorithm will be exponential in the number of processes of the system and thus the size of the system becomes a limiting factor. Such a problem has been defined in the literature as "state explosion problem". We propose a method of incremental verification of architectural specifications for real-time systems. The method has a lower complexity in a sense that it does not work on the whole state space, but only on a subset of it that is relevant to the property to be verified.

One of the features that distinguishes digital libraries from traditional databases is new cost models for client access to intellectual property. Clients will pay for accessing data items in digital libraries, and we believe that optimizing these costs will be as important as optimizing performance in traditional databases. In this article we discuss cost models and protocols for accessing digital libraries, with the objective of determining the minimum cost protocol for each model. We expect that in the future information appliances will come equipped with a cost optimizer, in the same way that computers today come with a built-in operating system. This article makes the initial steps towards a thery and practice of intellectual property cost management.

Users of mobile computers will soon have online access to a large number of databases via wireless networks. Because of limited bandwidth, wireless communication is more expensive than wire communication. In this paper, we present and analyze various static and dynamic data allocation methods. The objective is to optimize the communication cost between a mobile computer and the stationary computer that stores the online database. Analysis is performed in two cost models. One is connection (or time) based, as in cellular telephones, where the user is charged per minute of connection. The other is message based, as in packet radio networks, where the user is charged per message. Our analysis addresses both the average case and the worst case for determining the best allocation method.

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.

The authors propose a language, called Hierarchical Temporal Logic (HTL), for specifying queries on video databases. The language is based on the hierarchical as well as temporal nature of video data. They give similarity based semantics for the logic, and give efficient methods for computing similarity values for subclasses of HTL formulas. Experimental results, indicating the effectiveness of the methods, are presented.

One useful technique for combating the state explosion problem is to exploit symmetry when performing temporal logic model checking. In previous work it is shown how, using some basic notions of group theory, symmetry may be exploited for the full range of correctness properties expressible in the very expressive temporal logic CTL*. Surprisingly, while fairness properties are readily expressible in CTL*, these methods are not powerful enough to admit any amelioration of state explosion, when fairness assumptions are involved. We show that it is nonetheless possible to handle fairness efficiently by trading some group theory for automata theory. Our automata-theoretic approach depends on detecting fair paths subtly encoded in a quotient structure whose arcs are annotated with permutations, by using a threaded structure that reflects coordinate shifts caused by the permutations.

Article Free Access Share on Performance evaluation of G-tree and its application in fuzzy databases Authors: Chengwen Liu DePaul University, Chicago, Illinois DePaul University, Chicago, IllinoisView Profile , Aris Ouksel University of Illinois at Chicago University of Illinois at ChicagoView Profile , Prasad Sistla University of Illinois at Chicago University of Illinois at ChicagoView Profile , Jing Wu University of Illinois at Chicago University of Illinois at ChicagoView Profile , Clement Yu University of Illinois at Chicago University of Illinois at ChicagoView Profile , Naphtali Rishe Florida International University Florida International UniversityView Profile Authors Info & Claims CIKM '96: Proceedings of the fifth international conference on Information and knowledge managementNovember 1996 Pages 235–242https://doi.org/10.1145/238355.238503Published:12 November 1996Publication History 11citation347DownloadsMetricsTotal Citations11Total Downloads347Last 12 Months6Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

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. 0 1 Introduction The most popular model of rules in active database systems is the ECA model [41, 6, 28, 5, 14, 18]. It defines a rule to consist of three parts, event, condition, and action. The semantics is that whenever the event happens, the condition (which is usually a database query) is evaluated, and if satisfied then the action is taken. The event may be composite and temporal, such as, transaction A starts after transaction B ended. However, the condition is static in the sense that it refers to the cu...

In this paper we propose two languages, called Future Temporal Logic (FTL) and Past Temporal Logic (PTL), for specifying temporal triggers. Some examples of trigger conditions that can be specified in our language are the following: "The value of a certain attribute increases by more than 10% in 10 minutes," "A tuple that satisfies a certain predicate is added to the database at least 10 minutes before another tuple, satisfying a different condition, is added to the database." Such triggers are important for monitor and control applications. In addition to the languages, we present algorithms for processing the trigger conditions specified in these languages, namely, procedures for determining when the trigger conditions are satisfied. These methods can be added as a "temporal" component to an existing database management systems. A preliminary prototype of the temporal component that uses the FTL language has been built on top of Sybase running on SUN workstations.>

Users of mobile computers will soon have online access to a large number of databases via wireless networks. Because of limited bandwidth, wireless communication is more expensive than wire communication. In this paper we present and analyze various static and dynamic data allocation methods. The objective is to optimize the communication cost between a mobile computer and the stationary computer that stores the online database. Analysis is performed in two cost models. One is connection (or time) based, as in cellular telephones, where the user is charged per minute of connection. The other is message based, as in packet radio networks, where the user is charged per message. Our analysis addresses both, the average case and the worst case for determining the best allocation method.

Abstract In this paper we present syntactic characterization of temporal formulas that express various properties of interest in the verification of concurrent programs. Such a characterization helps us in choosing the right techniques for proving correctness with respect to these properties. The properties that we consider include safety properties, liveness properties and fairness properties. We also present algorithms for checking if a given temporal formula expresses any of these properties.

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.

Article Efficient distributed recovery using message logging Share on Authors: A. P. Sistla GTE Laboratories Incorporated GTE Laboratories IncorporatedView Profile , J. L. Welch GTE Laboratories Incorporated GTE Laboratories IncorporatedView Profile Authors Info & Claims PODC '89: Proceedings of the eighth annual ACM Symposium on Principles of distributed computingJune 1989 Pages 223–238https://doi.org/10.1145/72981.72997Online:01 June 1989Publication History 114citation572DownloadsMetricsTotal Citations114Total Downloads572Last 12 Months9Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.

In the verification of concurrent programs two kinds of properties are of primary importance and have been extensively investigated([3]): safety properties and liveness properties.Safety properties assert that something bad never happens while liveness properties assert that something good will eventually happen.In this paper we investigate the possibility of syntactically characterizing safety properties and liveness properties in temporal logic.A formal definition for safety properties was first given by Lamport and a slightly less restrictive definition is given in [5].We cony sider the later definition which states that a formula f in temporal logic expresses a safety property iff the following condition is satisfied: f holds on a a sequence iff every prefix of this sequence can be extended to satisfy the formula.We also consider a stronger definition of safety properties called strong safety properties.We show that the set of strong safety properties that can be expressed in propositional temporal logic are exactly those properties which are expressed by formulae built using the modality G("always"), the propositional connectives A,v and atomic propositions or their negations.

The complexity of satisfiability and determination of truth in a particular finite structure are considered for different propositional linear temporal logics. It is shown that these problems are NP-complete for the logic with F and are PSPACE-complete for the logics with F, X, with U, with U, S, X operators and for the extended logic with regular operators given by Wolper.

Message passing is one of the primary methods of information exchange between communicating processes. Many programming languages (e.g., CSP, ADA) provide interprocess communication through a rendezvous in which a sender (receiver) process waits until the receiver (sender) is ready to receive (send) a message; thus there is no buffering of messages. Many of these languages also allow non-deterministic constructs by which a process may wait to communication with any of a set of other processes. In this paper we consider the problem of ensuring different fairness properties in such a system of processes. In a natural model we prove a simple lower bound on the time complexity to ensure weak fairness and present near optimal algorithms in special cases. We also give new efficient algorithms to ensure strong fairness.

In this paper we study the full branching time logic (CTL*) in which a path quantifier, either A (“for all paths”) or E (ldquo;for some path”), prefixes an assertion composed of arbitrary combinations of the usual linear time operators F (“sometime”), G (“always”), X (“nexttime”), and U (“until”). We show that the problem of determining if a CTL* formula is satisfiable in structure generated by a binary relation is decidable in triple exponential time. The decision procedure exploits the special structure of the finite state ω-automata for linear temporal formulae which allows them to be determinized with only a single exponential blowup in size. We also compare the expressive power of tree automata with CTL* augmented by quantified auxillary propositions.

We investigate extensions of temporal logic by finite automata on infinite words. There are three different types of acceptance conditions (finite, looping and repeating) that one can give for these finite automata. This gives rise to three different logics. It turns out, however. that these logics have the same expressive power but differ in the complexity of their decision problem. We also investigate the addition of alternation and show that it does not increase the complexity of the decision problem.

We give an efficient procedure for verifying that a finite state concurrent system meets a specification expressed in a (propositional) branching-time temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global transition graph for the concurrent system. We also show how the logic and our algorithm can be modified to handle fairness. We argue that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite state concurrent systems.

Exchange of information between executing processes is one of the primary reasons for process interaction. Many distributed systems implement explicit message passing primitives to facilitate intercommunication. Typically, a process executes a write command to pass a message to another process, and the target process accepts the message by executing a read command. The semantics of write and read may differ considerably depending on the methods used for storing or buffering messages that have been sent but not yet accepted by the receiving process.

We consider the complexity of satisfiability and determination of truth in a particular finite structure for different propositional linear temporal logics. We show that both the above problems are NP-complete for the logic with F operator and are PSPACE-complete for the logics with F,X, with U, with U,S,X, and Wolper's extended logic with regular operators [Wo81].