International Journal of Foundations of Computer Science

This paper shows how to perform model checking, a technique for automatic program verification, by a DNA algorithm. Our method depends on two ideas. First, Kripke structures can be compactly represented in a DNA substrate, coding each state and each edge by a strand of DNA. Second, satisfaction of temporal eventualities can be achieved through a self-propagating molecular chain reaction.

The outcome of verifying software is often a 'counterexample', i.e., a listing of the actions and states of a behavior not satisfying the specification. The verification is usually done using a model of the software (often also using some abstraction to reduce its complexity) rather than the actual code. In order to understand the reason for the failure manifested by such a counterexample, it is sometimes necessary to test such an execution using the actual code. In this way we also find out whether we have a genuine error or a "false negative". Due to nondeterminism in concurrent code, enforcing a particular behavior of an actual program is not guaranteed even when one starts the execution with the prescribed initial state. Testers are faced with a similar problem when they have to demonstrate that a suspicious scenario can actually be executed. Such a scenario may involve some intricate scheduling and thus be illusive to demonstrate. We describe here a transformation that allows us to repeat a selected execution sequences of concurrent code. Since the transformation implies changes to the original code, we strive to minimize its effect on the original program.

We present a new abstraction refinement algorithm to better refine the abstract model for formal property verification. In previous work, refinements are selected either based on a set of counter examples of the current abstract model, as in [5, 6, 7, 8, 9, 20, 21], or independent of any counter examples, as in [18]. We (1) introduce a new controllability analysis that is independent of any particular counter examples, (2) apply a new cooperativeness analysis that extracts information from a particular set of counter examples and (3) combine both to better refine the abstract model. We implemented the algorithm and applied it to verify several real-world designs and properties. We compared the algorithm against the abstraction refinement algorithms in [20] and [21] and the interpolation-based reachability analysis in [15]. The experimental results indicate that the new algorithm outperforms the other three algorithms in terms of runtime, abstraction efficiency (as defined in [20]) and the number of proven properties.

We propose a new SAT-based model checking algorithm to solve the reachability problem of real-time systems. In our algorithm, the behavior of region automata is encoded as Boolean formulas, and hence any SAT solver can be used to explore the region graph efficiently. Although our SAT-based algorithm performs better than other algorithms in flaw detection, it is less effective in proving properties. To overcome the problem, we incorporate a complete inductive method in our algorithm to improve the performance when the property is satisfied. We implement both algorithms in a tool called xBMC and report experimental results. The experiments show that the combination of efficient encoding and inductive methods offers an effective and practical method for the analysis of timing behavior.

This paper studies conflicts from a process-algebraic point of view and shows how they are related to the testing theory of fair testing. Conflicts have been introduced in the context of discrete event systems, where two concurrent systems are said to be in conflict if they can get trapped in a situation where they are waiting or running endlessly, forever unable to complete their common task. In order to analyse complex discrete event systems, conflict-preserving notions of refinement and equivalence are needed. This paper characterises an appropriate refinement, called the conflict preorder, and provides a denotational semantics for it. Its relationship to other known process preorders is explored, and it is shown to generalise the fair testing preorder in process-algebra for reasoning about conflicts in discrete event systems.

Testing equivalence is a quite powerful way of expressing security properties of cryptographic protocols, but its formal verification is a difficult task, because it is based on universal quantification over contexts. A technique based on state exploration to address this verification problem has previously been presented; it relies on an environment-sensitive labelled transition system (ES-LTS) and on symbolic term representation. This paper shows that such a technique can be enhanced by exploiting symmetries found in the ES-LTS structure. Experimental results show that the proposed enhancement can substantially reduce the size of the ES-LTS and that the technique as a whole compares favorably with respect to related work.

In the development of real-time communicating hardware/embedded-software systems, it is frequently the case that we want to refine/optimize the system's internal behavior while preserving the external timed I/O behavior. In such a design refinement, modification of the systems' internal branching structures, as well as re-scheduling of internal actions, may frequently occur. Our goal is, then, to ensure that such modification of internal branching structures and re-scheduling of internal actions preserve the systems' external timed behavior, which is typically formalized by the notion of (timed) failure equivalence since it is less sensitive to the difference of internal branching structures than (timed) weak bisimulation. In order to know the degree of freedom of such re-scheduling, parametric analysis is useful. One of the models suitable for such an analysis is a parametric time-interval automaton(PTIA), which is a subclass of the existing model, a parametric timed automaton. It has only a time interval with upper- and lower-bound parameters as a relative timing constraint between consecutive actions. In this paper, at first, we propose an abstraction algorithm of PTIA which preserves timed failure equivalence. Timed failure equivalence is strictly weaker than timed weak bisimulation in the sense that it does not distinguish the difference of the timing when the internal resolution of nondeterminism has occurred, but it does distinguish the difference of the refusals of communicating actions observed by an external environment. Then, we also show that after applying our algorithm, the reduced PTIA has no internal actions, and thus the problem deriving a parameter condition in order that given two models are timed failure equivalent can be reduced to the existing parametric strong bisimulation equivalence checking.

The complementation problem for nondeterministic word automata has numerous applications in formal verification. In particular, the language-containment problem, to which many verification problems is reduced, involves complementation. For automata on finite words, which correspond to safety properties, complementation involves determinization. The 2ⁿ blow-up that is caused by the subset construction is justified by a tight lower bound. For Büchi automata on infinite words, which are required for the modeling of liveness properties, optimal complementation constructions are quite complicated, as the subset construction is not sufficient. From a theoretical point of view, the problem is considered solved since 1988, when Safra came up with a determinization construction for Büchi automata, leading to a 2^{O(n log n)} complementation construction, and Michel came up with a matching lower bound. A careful analysis, however, of the exact blow-up in Safra's and Michel's bounds reveals an exponential gap in the constants hiding in the O( ) notations: while the upper bound on the number of states in Safra's complementary automaton is n²ⁿ, Michel's lower bound involves only an n! blow up, which is roughly (n/e)ⁿ. The exponential gap exists also in more recent complementation constructions. In particular, the upper bound on the number of states in the complementation construction of Kupferman and Vardi, which avoids determinization, is (6n)ⁿ. This is in contrast with the case of automata on finite words, where the upper and lower bounds coincides. In this work we describe an improved complementation construction for nondeterministic Büchi automata and analyze its complexity. We show that the new construction results in an automaton with at most (0.96n)ⁿ states. While this leaves the problem about the exact blow up open, the gap is now exponentially smaller. From a practical point of view, our solution enjoys the simplicity of the construction of Kupferman and Vardi, and results in much smaller automata.

We introduce and study three notions of typeness for automata on infinite words. For an acceptance-condition class γ (that is, γ is weak, Büchi, co-Büchi, Rabin, or Streett), deterministic γ-typeness asks for the existence of an equivalent γ-automaton on the same deterministic structure, nondeterministic γ-typeness asks for the existence of an equivalent γ-automaton on the same structure, and γ-powerset-typeness asks for the existence of an equivalent γ-automaton on the (deterministic) powerset structure – one obtained by applying the subset construction. The notions are helpful in studying the complexity and complication of translations between the various classes of automata. For example, we prove that deterministic Büchi automata are co-Büchi type; it follows that a translation from deterministic Büchi to deterministic co-Büchi automata, when exists, involves no blow up. On the other hand, we prove that nondeterministic Büchi automata are not co-Büchi type; it follows that a translation from a nondeterministic Büchi to nondeterministic co-Büchi automata, when exists, should be more complicated than just redefining the acceptance condition. As a third example, by proving that nondeterministic co-Büchi automata are Büchi-powerset type, we show that a translation of nondeterministic co-Büchi to deterministic Büchi automata, when exists, can be done applying the subset construction. We give a complete picture of typeness for the weak, Büchi, co-Büchi, Rabin, and Streett acceptance conditions, and discuss its usefulness.

Though model checking itself is a fully automated process, verifying correctness of a hybrid system design using model checking is not. This paper describes the necessary steps, and choices to be made, to go from an informal description of the problem to the final verification result for a formal model and requirement. It uses an automotive control system for illustration.

The largest common point set problem (LCP) is, given two point set P and Q in d-dimensional Euclidean space, to find a subset of P with the maximum cardinality that is congruent to some subset of Q. We consider a special case of LCP in which the size of the largest common point set is at least (|P| + |Q| - k)/2. We develop efficient algorithms for this special case of LCP and a related problem. In particular, we present an O(k³n^1.34 + kn²log n) time algorithm for LCP in two-dimensions, which is much better for small k than an existing O(n^3.2log n) time algorithm, where n = max{|P|,|Q|}.

Quantum games offer situations where quantum information theory may help in solving or improving games with lack of information. For example, one may rely upon properties of entanglement for showing the superiority of a quantum player who is allowed to use quantum operations against a classical player (penny flipover [5]). Quantum communication properties enter into play in cooperative games (prisoners game, [3], guessing number [10]). An introduction to this field and an overview of important results are proposed in [7, 8]. But games may also help to make notions easier to understand, and new ways of reasoning to apprehend. The objective of this paper is to formalize and study a simple game with qubits using quantum notions of measurement and superposition, while keeping a simple formalism so that knowing quantum mechanics is not necessary to play the game. We generalize Conway's classical octal games to quantum octal games, and we solve the quantum combinatorial game QO.07 by giving a winning strategy for it. A playable version of the studied qubit game is available at the address .

A signed n-permutation is a permutation on {1,2,…,n} in which each element is labelled by a positive or negative sign. Here we consider the problem of sorting signed permutations by fixed-length reversals. Indeed, limiting the transformations to reversals of length exactly k can be very restrictive, for example, (+1,+3,+2,+4,…,+n) can never be sorted to (+1,+2,+3,+4,…,+n) by 2-reversals. That is, for given two signed permutations it is not obvious whether they can be sorted to each other by k-reversals. Thus in 1996, Chen and Skiena gave the following open problem: what is the connectedness of signed permutations under fixed-length reversals? In this paper, we resolve this open problem when "fixed-length" is even, and give a characterization of the connectedness of signed n-permutations under 2l-reversal, for both linear and circular permutations.

Transient simulation of a gate circuit is an efficient method of counting signal changes occurring during a transition of the circuit. It is known that this simulation covers the results of classical binary analysis, in the sense that all signal changes appearing in binary analysis are also predicted by the simulation. For feedback-free circuits of 1- and 2-input gates, it had been shown that the converse also holds, if wire delays are taken into account. In this paper we generalize this result. First, we prove that, for any feedback-free circuit N of arbitrary gates, there exists an expanded circuit, constructed by adding a number of delays to each wire of N, such that binary analysis of covers transient simulation of N. For this result, the number of delays added to a wire is obtained from the transient simulation. Our second result involves adding only one delay per wire, which leads to the singular circuit of N. This result is restricted to circuits consisting only of gates realizing functions from the set , functions obtained by complementing any number of inputs and/or the output of a function from , and FORKS. The numbers of inputs of the AND, OR and XOR gates are arbitrary, and all functions of two variables are included. We show that binary analysis of such a circuit covers transient simulation of N. We also show that this result cannot be extended to arbitrary gates, if we allow only a constant number of delays per wire.

We continue here the study of the recently introduced spiking neural P systems, which mimic the way that neurons communicate with each other by means of short electrical impulses, identical in shape (voltage), but emitted at precise moments of time. The sequence of moments when a neuron emits a spike is called the spike train (of this neuron); by designating one neuron as the output neuron of a spiking neural P system II, one obtains a spike train of II. Given a specific way of assigning sets of numbers to spike trains of II, we obtain sets of numbers computed by II. In this way, spiking neural P systems become number computing devices. We consider a number of ways to assign (code) sets of numbers to (by) spike trains, and prove then computational completeness: the computed sets of numbers are exactly Turing computable sets. When the number of spikes present in the system is bounded, a characterization of semilinear sets of numbers is obtained. A number of research problems is also formulated.