Search

The quantitative information flow bounding problem asks, given a program P and threshold q, whether the information leaked by P is bounded by q. When the amount of information is measured using mutual information, the problem is known to be PSPACE-hard and decidable in EXPTIME. We show that the problem is in fact decidable in PSPACE, thus establishing the exact complexity of the quantitative information flow bounding problem. Thus, the complexity of bounding quantitative information flow in programs has the same complexity as safety verification of programs. We also show that the same bounds apply when comparing information leaked by two programs. [ABSTRACT FROM AUTHOR]

This paper investigates the power of Probabilistic Büchi Automata (PBA) when the threshold probability of acceptance is non-extremal, i.e., is a value strictly between 0 and 1. Many practical randomized algorithms are designed to work under non-extremal threshold probabilities and thus it is important to study power of PBAs for such cases. The paper presents a number of surprising expressiveness and decidability results for PBAs when the threshold probability is non-extremal. Some of these results sharply contrast with the results for extremal threshold probabilities. The paper also presents results for Hierarchical PBAs and for an interesting subclass of them called simple PBAs. [ABSTRACT FROM AUTHOR]

We present uniform approaches to establish complexity bounds for decision problems such as reachability and simulation, that arise naturally in the verification of timed software systems. We model timed software systems as timed automata augmented with a data store (like a pushdown stack) and show that there is at least an exponential blowup in complexity of verification when compared with untimed systems. Our proof techniques also establish complexity results for boolean programs, which are automata with stores that have additional boolean variables. [ABSTRACT FROM AUTHOR]

We introduce STORMED hybrid games (SHG), a generalization of STORMED Hybrid Systems [15], which have natural specifications, allow rich continuous dynamics and admit various properties to be decidable. We solve the control problem for SHG using a reduction to bisimulation on game graphs. This reduction generalizes to a greater family of games, which includes o-minimal hybrid games [5]. We also solve the optimal-cost reachability problem for Weighted SHG. [ABSTRACT FROM AUTHOR]

We study visibly pushdown automata (VPA) models for expressing and evaluating queries on words with a nesting structure. We define a query VPA model, which is a 2-way deterministic VPA that can mark in one run all positions in a document that satisfy a query, and show that it is equi-expressive as unary monadic queries. This surprising result parallels a classic result by Hopcroft and Ullman for queries on regular word languages. We also compare our model to query models on unranked trees, and show that our result is fundamentally different from those known for automata on trees. [ABSTRACT FROM AUTHOR]

Convergence is often the key liveness property for distributed systems that interact with physical processes. Techniques for proving convergence (asymptotic stability) have been extensively studied by control theorists. In particular, for the asynchronous model of computation Tsitsiklis [8] provides a set of necessary and sufficient conditions for proving stability and convergence under the assumption that each asynchronous operator (state transition function) is applied infinitely often. This paper generalize these results to obtain necessary and sufficient conditions for systems where the infinite sequence of operators is a member of an arbitrary omega regular language. This enables us to apply our theory to distributed systems with changing communication topology, node failures and joins. We illustrate an application of the new set of conditions in verifying the convergence of a simple (continuous) consensus protocol. [ABSTRACT FROM AUTHOR]

Probabilistic Büchi Automata (PBA) are randomized, finite state automata that process input strings of infinite length. Based on the threshold chosen for the acceptance probability, different classes of languages can be defined. In this paper, we present a number of results that clarify the power of such machines and properties of the languages they define. The broad themes we focus on are as follows. We precisely characterize the complexity of the emptiness, universality, and language containment problems for such machines, answering canonical questions central to the use of these models in formal verification. Next, we characterize the languages recognized by PBAs topologically, demonstrating that though general PBAs can recognize languages that are not regular, topologically the languages are as simple as ω-regular languages. Finally, we introduce Hierarchical PBAs, which are syntactically restricted forms of PBAs that are tractable and capture exactly the class of ω-regular languages. [ABSTRACT FROM AUTHOR]

The paper shows the decidability of the reachability problem for planar, monotonic, linear hybrid automata without resets. These automata are a special class of linear hybrid automata with only two variables, whose flows in all states is monotonic along some direction in the plane, and in which the continuous variables are not reset on a discrete transition. [ABSTRACT FROM AUTHOR]

Abstraction is a key technique to combat the state space explosion problem in model checking probabilistic systems. In this paper we present new ways to abstract Discrete Time Markov Chains (DTMCs), Markov Decision Processes (MDPs), and Continuous Time Markov Chains (CTMCs). The main advantage of our abstractions is that they result in abstract models that are purely probabilistic, which maybe more amenable to automatic analysis than models with both nondeterministic and probabilistic steps that typically arise from previously known abstraction techniques. A key technical tool, developed in this paper, is the construction of least upper bounds for any collection of probability measures. This upper bound construction may be of independent interest that could be useful in the abstract interpretation and static analysis of probabilistic programs. [ABSTRACT FROM AUTHOR]

We investigate the problem of model checking Interval-valued Discrete-time Markov Chains (IDTMC). IDTMCs are discrete-time finite Markov Chains for which the exact transition probabilities are not known. Instead in IDTMCs, each transition is associated with an interval in which the actual transition probability must lie. We consider two semantic interpretations for the uncertainty in the transition probabilities of an IDTMC. In the first interpretation, we think of an IDTMC as representing a (possibly uncountable) family of (classical) discrete-time Markov Chains, where each member of the family is a Markov Chain whose transition probabilities lie within the interval range given in the IDTMC. This semantic interpretation we call Uncertain Markov Chains (UMC). In the second semantics for an IDTMC, which we call Interval Markov Decision Process (IMDP), we view the uncertainty as being resolved through non-determinism. In other words, each time a state is visited, we adversarially pick a transition distribution that respects the interval constraints, and take a probabilistic step according to the chosen distribution. We show that the PCTL model checking problem for both Uncertain Markov Chain semantics and Interval Markov Decision Process semantics is decidable in PSPACE. We also prove lower bounds for these model checking problems. [ABSTRACT FROM AUTHOR]

In the paper, we introduce a new tree automata framework, called propositional tree automata, capturing the class of tree languages that are closed under an equational theory and Boolean operations. This framework originates in work on developing a sufficient completeness checker for specifications with rewriting modulo an equational theory. Propositional tree automata recognize regular equational tree languages. However, unlike regular equational tree automata, the class of propositional tree automata is closed under Boolean operations. This extra expressiveness does not affect the decidability of the membership problem. This paper also analyzes in detail the emptiness problem for propositional tree automata with associative theories. Though undecidable in general, we present a semi-algorithm for checking emptiness based on machine learning that we have found useful in practice. [ABSTRACT FROM AUTHOR]

Boolean programs with recursion are convenient abstractions of sequential imperative programs, and can be represented as recursive state machines (RSMs) or pushdown automata. Motivated by the special structure of RSMs, we define a notion of modular visibly pushdown automata (modular VPA) and show that for the class of languages accepted by such automata, unique minimal modular VPA exist. This yields an efficient approximate minimization theorem that minimizes RSMs to within a factor of k of the minimal RSM, where k is the maximum number of parameters in any module. Using the congruence defined for minimization, we show an active learning algorithm (with a minimally adequate teacher) for context free languages in terms of modular VPAs. We also present an algorithm that constructs complete test suites for Boolean program specifications. Finally, we apply our results on learning and test generation to perform model checking of black-box Boolean programs. [ABSTRACT FROM AUTHOR]

Software systems are often modeled using infinite structures such as unbounded integers, infinite message queues and call stacks, and unbounded number of processes. This makes verification of these systems hard- in fact, for most common classes of infinite state systems, the verification problem is undecidable. [ABSTRACT FROM AUTHOR]

In order to make multithreaded programming manageable, programmers often follow a design principle where they break the problem into tasks which are then solved asynchronously and concurrently on different threads. This paper investigates the problem of model checking programs that follow this idiom. We present a programming language Spl that encapsulates this design pattern. Spl extends simplified form of sequential Java to which we add the capability of making asynchronous method invocations in addition to the standard synchronous method calls and the ability to execute asynchronous methods in threads atomically and concurrently. Our main result shows that the control state reachability problem for finite Spl programs is decidable. Therefore, such multithreaded programs can be model checked using the counterexample guided abstraction-refinement framework. [ABSTRACT FROM AUTHOR]

Statistical methods to model check stochastic systems have been, thus far, developed only for a sublogic of continuous stochastic logic (CSL) that does not have steady state operator and unbounded until formulas. In this paper, we present a statistical model checking algorithm that also verifies CSL formulas with unbounded untils. The algorithm is based on Monte Carlo simulation of the model and hypothesis testing of the samples, as opposed to sequential hypothesis testing. We have implemented the algorithm in a tool called VESTA, and found it to be effective in verifying several examples. [ABSTRACT FROM AUTHOR]

We study congruences on words in order to characterize the class of visibly pushdown languages (Vpl), a subclass of context-free languages. For any language L, we define a natural congruence on words that resembles the syntactic congruence for regular languages, such that this congruence is of finite index if, and only if, L is a Vpl. We then study the problem of finding canonical minimal deterministic automata for Vpls. Though Vpls in general do not have unique minimal automata, we consider a subclass of VPAs called k-module single-entry VPAs that correspond to programs with recursive procedures without input parameters, and show that the class of well-matched Vpls do indeed have unique minimal k-module single-entry automata. We also give a polynomial time algorithm that minimizes such k-module single-entry VPAs. [ABSTRACT FROM AUTHOR]

Traditional network simulators perform well in evaluating the performance of network protocols but lack the capability of verifying the correctness of protocols. To address this problem, we have extended the J-Sim network simulator with a model checking capability that explores the state space of a network protocol to find an execution that violates a safety invariant. In this paper, we demonstrate the usefulness of this integrated tool for verification and performance evaluation by analyzing two widely used and important network protocols: AODV and directed diffusion. Our analysis discovered a previously unknown bug in the J-Sim implementation of AODV. More importantly, we also discovered a serious deficiency in directed diffusion. To enable the analysis of these fairly complex protocols, we needed to develop protocol-specific search heuristics that guide state-space exploration. We report our findings on discovering good search heuristics to analyze network protocols similar to AODV and directed diffusion. [ABSTRACT FROM AUTHOR]

When a system fails to satisfy its specification, the model checker produces an error trace (or counter-example) that demonstrates an undesirable behavior, which is then used in debugging the system. Error explanation is the task of discovering errors in the system or the reasons why the system exhibits the error trace. While there has been considerable recent interest in automating this task and developing tools based on different heuristics, there has been very little effort in characterizing the computational complexity of the problem of error explanation. In this paper, we study the complexity of two popular heuristics used in error explanation. The first approach tries to compute the smallest number of system changes that need to be made in order to ensure that the given counter-example is no longer exhibited, with the intuition being that these changes are the errors that need fixing. The second approach relies on the observation that differences between correct and faulty runs of a system shed considerable light on the sources of errors. In this approach, one tries to compute the correct trace of the system that is closest to the counter-example. We consider three commonly used abstractions to model programs and systems, namely, finite state Mealy machines, extended finite state machines and pushdown automata. We show that the first approach of trying to find the fewest program changes is NP-complete no matter which of the three formal models is used to represent the system. Moreover we show that no polynomial factor approximation algorithm for computing the smallest set of changes is possible, unless P = NP. For the second approach, we present a polynomial time algorithm that finds the closest correct trace, when the program is represented by a Mealy machine or a pushdown automata. When the program is represented by an extended finite state machine, the problem is once again NP-complete, and no polynomial factor approximation algorithm is likely. [ABSTRACT FROM AUTHOR]

A novel machine learning based approach was proposed recently as a complementary technique to the acceleration based methods for verifying infinite state systems. In this method, the set of states satisfying a fixpoint property is learnt as opposed to being iteratively computed. We extend the machine learning based approach to verifying general ω-regular properties that include both safety and liveness. To achieve this, we first develop a new fixpoint based characterization for the verification of ω-regular properties. Using this characterization, we present a general framework for verifying infinite state systems. We then instantiate our approach to the context of regular model checking where states are represented as strings over a finite alphabet and the transition relation of the system is given as a finite state transducer; unlike previous learning based algorithms, we make no assumption about the transducer being length-preserving. Using Angluin's L* algorithm for learning regular languages, we develop an algorithm for verification of ω-regular properties of such infinite state systems. The algorithm is a complete verification procedure for systems for whom the fixpoint can be represented as a regular set. We have implemented the technique in a tool called Lever and use it to analyze some examples. [ABSTRACT FROM AUTHOR]

As the complexity of systems grows, the correctness of systems becomes harder to achieve. This difficulty promotes a run-time monitoring technique as a promising complementary methodology for higher system assurance. To formalize and understand the computational nature of run-time monitoring is a key to utilize this valuable technique. In this paper, we formalize the notion of run-time monitoring of reactive systems in terms of ω-languages and show that the language of Monitoring and Checking (MaC) architecture, called MEDL, is expressive enough for the run-time monitoring. First, we provide a descriptive theory for the class of monitorable languages and show that this class of languages coincides with the class Π01 of the Arithmetic hierarchy. Second, we introduce a class of automata with storage that can be used to describe the class of monitorable languages using connections to the Arithmetic hierarchy. Finally, we show that MEDL can express the class of monitorable languages via the correspondence between MEDL and the automata with storage. [ABSTRACT FROM AUTHOR]

In this paper we present lower bounds and rewriting algorithms for testing membership of a word in a regular language described by an extended regular expression. Motivated by intuitions from monitoring and testing, where the words to be tested (execution traces) are typically much longer than the size of the regular expressions (patterns or requirements), and by the fact that in many applications the traces are only available incrementally, on an event by event basis, our algorithms are based on an event-consumption idea: a just arrived event is "consumed" by the regular expression, i.e., the regular expression modifies itself into another expression discarding the event. We present an exponential space lower bound for monitoring extended regular expressions and argue that the presented rewriting-based algorithms, besides their simplicity and elegance, are practical and almost as good as one can hope. We experimented with and evaluated our algorithms in Maude. [ABSTRACT FROM AUTHOR]