Narrow Results

We introduce a certain restriction of weighted automata over the rationals, called image-binary automata. We show that such automata accept the regular languages, can be exponentially more succinct than corresponding NFAs, and allow for polynomial complementation, union, and intersection. This compares favourably with unambiguous automata whose complementation requires a superpolynomial state blowup. We also study an infinite-word version, image-binary Büchi automata. We show that such automata are amenable to probabilistic model checking, similarly to unambiguous Büchi automata. We provide algorithms to translate $k$-ambiguous Büchi automata to image-binary Büchi automata, leading to model-checking algorithms with optimal computational complexity.

A common characteristic of the new distributed systems is the increasing complexity. Useful paradigms to cope with the complexity of systems are modularity and compositionality. In this paper we define a compositional method to attack the state explosion problem in model checking. The method, given a formula to be checked on a system composed of a set of parallel processes, allows syntactically reducing in a modular way the processes, in order to reduce the state space of their composition. The reduction is formula driven and is based on a notion of equivalence between processes, which is a congruence w.r.t. the parallel composition operator.

Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be inconclusive, however, in which case the abstraction must be refined. This paper presents a new procedure to perform this refinement operation for abstractions of hybrid systems. Following an approach originally developed for finite-state systems [11, 25], the refinement procedure constructs a new abstraction that eliminates a counterexample generated by the model checker. For hybrid systems, analysis of the counterexample requires the computation of sets of reachable states in the continuous state space. We show how such reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently. Examples illustrate our counterexample-guided refinement procedure. Experimental results for a prototype implementation indicate significant advantages over existing methods.

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.

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.

Predicate abstraction has become one of the most successful methodologies for proving safety properties of programs. Recently, several abstraction methodologies have been proposed for proving liveness properties. This paper studies "ranking abstraction" where a program is augmented by a non-constraining progress monitor based on a set of ranking functions, and further abstracted by predicate-abstraction, to allow for automatic verification of progress properties. Unlike many liveness methodologies, the augmentation does not require a complete ranking function that is expected to decrease with each helpful step. Rather, adequate user-provided inputs are component rankings from which a complete ranking function may be automatically formed.

The premise of the paper is an analogy between the methods of ranking abstraction and predicate abstraction, one ingredient of which is refinement: When predicate abstraction fails, one can refine it. When ranking abstraction fails, one must determine whether the predicate abstraction, or the ranking abstraction, needs be refined. The paper presents strategies for determining which case is at hand, and methods for performing the apporpriate refinements.

The other part of the analogy is that of automatically deriving deductive proof constructs: Predicate abstraction is often used to derive program invariants for proving safety properties as a boolean combination of the given predicates. Deductive proof of progress properties requires well-founded ranking functions in addition to invariants. We show how the constructs necessary for a deductive proof of an arbitrary LTL formula can be automatically extracted from a successful application of the ranking abstraction method.

Recent advances in scheduling and networking have paved the way for efficient exploitation of large-scale distributed computing platforms such as computational grids and huge clusters. Such infrastructures hold great promise for the highly resource-demanding task of verifying and checking large models, given that model checkers would be designed with a high degree of scalability and flexibility in mind.

In this paper we focus on the mechanisms required to execute a high-performance, distributed, symbolic model checker on top of a large-scale distributed environment. We develop a hybrid algorithm for slicing the state space and dynamically distribute the work among the worker processes. We show that the new approach is faster, more effective, and thus much more scalable than previous slicing algorithms. We then present a checkpoint-restart module that has very low overhead. This module can be used to combat failures, the likelihood of which increases with the size of the computing plat-form. However, checkpoint-restart is even more handy for the scheduling system: it can be used to avoid reserving large numbers of workers, thus making the distributed computation work-efficient. Finally, we discuss for the first time the effect of reorder on the distributed model checker and show how the distributed system performs more efficient reordering than the sequential one.

We implemented our contributions on a network of 200 processors, using a distributed scalable scheme that employs a high-performance industrial model checker from Intel. Our results show that the system was able to verify real-life models much larger than was previously possible.

This paper addresses the challenges of symbolic model checking and language emptiness checking where the specification is given as an alternating Büchi automaton.

We introduce a novel version of Miyano and Hayashi's construction that allows us to directly convert an alternating automaton to a polynomially-sized symbolic structure. We thus avoid building an exponentially-sized explicit representation of the corresponding nondeterministic automaton.

For one-weak automata, Gastin and Oddoux' construction produces smaller automata than Miyano and Hayashi's construction. We present a (symbolic) hybrid approach that combines the benefits of both: while retaining full generality, it uses the cheaper construction for those parts of the automaton that are one-weak.

We performed a thorough experimental comparison of the explicit and symbolic approaches and several variants of Miyano and Hayashi's construction, using both BDD-based and SAT-based model checking techniques. The symbolic approaches clearly outperform the explicit one.

Switching graphs are graphs that contain switches. A switch is a pair of edges that start in the same vertex and of which precisely one edge is enabled at any time. By using a Boolean function called a switch setting, the switches in a switching graph can be put in a fixed direction to obtain an ordinary graph. For many problems, switching graphs are a remarkable straightforward and natural model, but they have hardly been studied. We study the complexity of several natural questions in switching graphs of which some are polynomial, and others are NP-complete. We started investigating switching graphs because they turned out to be a natural framework for studying the problem of solving Boolean equation systems, which is equivalent to model checking of the modal µ-calculus and deciding the winner in parity games. We give direct, polynomial encodings of Boolean equation systems in switching graphs and vice versa, and prove correctness of the encodings.

A complete SAT-based model checking algorithm for context-free processes is presented. We reduce proof search in local model checking to Boolean satisfiability. Bounded proof search can therefore be performed by SAT solvers. Moreover, the completeness of proof search is reduced to Boolean unsatisfiability and hence can be checked by SAT solvers. By encoding the local model checking algorithm in [13], SAT solvers are able to verify properties in the universal fragment of alternation-free µ-calculus formulae on context-free processes. Since software programs can be modeled by context-free processes, our result demonstrates that a purely SAT-based algorithm for software verification is indeed possible.

This paper presents an approach to P system verification using the Spin model checker. It proposes a P system implementation in PROMELA, the modeling language accepted by SPIN. It also provides the theoretical background for transforming the temporal logic properties expressed for the P system into properties of the executable implementation. Furthermore, a comparison between P systems verification using SPIN and NUSMV is realized. The results obtained show that the PROMELA implementation is more adequate, especially for verifying more complex models, such as P systems that model ecosystems.

In this work, we consider Discrete-Time Continuous-Space Dynamic Systems for which we study the computability of the standard semantics of CTL* (CTL, LTL) and provide a variant thereof computable in the sense of Type-2 Theory of Effectivity. In particular, we show how the computable model checking of existentially and universally quantified path formulae of LTL can be reduced to solving, respectively, repeated reachability and persistence problems on a model obtained as a parallel composition of the original one and a non-deterministic Büchi automaton corresponding to the verified LTL formula.

This paper brings together two methods to compositionally verify the generalized non-blocking property, which is a weak liveness property to express the ability of concurrent systems to terminate under given preconditions. Appropriate notions of equivalence and refinement for the generalized nonblocking property are discussed, and abstraction rules to simplify finite-state automata accordingly are presented. The paper also presents a unique canonical automaton representation for all generalized nonblocking equivalent automata, which gives rise to more general means of abstraction and to effective decision procedures for generalized nonblocking equivalence. Experimental results demonstrate how abstraction rules and canonical automata can be combined to model-check large models of concurrent software.

The computational problem of model checking for circumscription of first-order formulae is studied. It is shown that there is a universal first-order formula whose circumscription has coNP-complete model checking problem. This answers a question raised by P.H. Kolaitis and C.H. Papadimitriou.

This paper presents an analysis method for quantum information protocols based on model checking, with special focus on the quantum privacy comparison (QPC). The security properties of these protocols can be proved but in ways with much difficulty. Here we will discuss a probabilistic model checking tool — PRISM to verify specific properties of QPC protocol with multi-body and PRISM to verify specific properties of quantum private comparison (QPC) protocol with multi-party and d-dimensional entangled states.

The back-off procedure is one of the media access control technologies in 802.11P communication protocol. It plays an important role in avoiding message collisions and allocating channel resources. Formal methods are effective approaches for studying the performances of communication systems. In this paper, we establish a discrete time model for the back-off procedure. We use Markov Decision Processes (MDPs) to model the non-deterministic and probabilistic behaviors of the procedure, and use the probabilistic computation tree logic (PCTL) language to express different properties, which ensure that the discrete time model performs their basic functionality. Based on the model and PCTL specifications, we study the effect of contention window length on the number of senders in the neighborhood of given receivers, and that on the station’s expected cost required by the back-off procedure to successfully send packets. The variation of the window length may increase or decrease the maximum probability of correct transmissions within a time contention unit. We propose to use PRISM model checker to describe our proposed back-off procedure for IEEE802.11P protocol in vehicle network, and define different probability properties formulas to automatically verify the model and derive numerical results. The obtained results are helpful for justifying the values of the time contention unit.

Graph pattern matching that aims to seek out answer graphs in a data graph matching a provided graph, plays a fundamental role as a part of graph search for graph databases. “Matching” indicates that the two graphs are correlated, such as bisimulation, isomorphism, simulation, etc. The strictness of bisimulation is between simulation and isomorphism. Seldom work has been done to search for bisimulation subgraphs. This research focuses on the problem. The symbol $\ast$ is introduced to fundamental modal logic language, thereby yielding $ML+\ast$ language; the symbols ${\square }^{\ast }$ is added for forming $ML+\ast$ formulas. Then conclusions about graph bisimulations are shown. Subsequently, a theorem with detailed proof is presented, stating that $ML+\ast$ formulas characterize finite directed graphs modulo bisimulation. According to the conclusions and theorem, algorithms for finding subgraphs are proposed. After dividing the query graph, the match graphs undergo the characterization using $ML+\ast$ formulas. In the data graphs, by model checking the formulas, the answer graphs exhibiting bisimilarity to the match graphs are able to be captured.

In this paper, we propose to integrate an embedding of Property Specification Language (PSL) in Abstract State Machines Language (AsmL) with a top–down design for verification approach in order to enable the model checking of large systems at the early stages of the design process. We provide a complete embedding of PSL in the ASM language AsmL, which allows us to integrate PSL properties as a part of the design. For verification, we propose a technique based on the AsmL tool that translates the code containing both the design and the properties into a finite state machine (FSM) representation. We use the generated FSM to run model checking on an external tool, here SMV. Our approach takes advantage of the AsmL language capabilities to model designs at the system level as well as from the power of the AsmL tool in generating both C# code and FSMs from AsmL models. We applied our approach on the PCI-X bus standard, which AsmL model was constructed from the informal standard specifications and a subsequent UML model. Experimental results on the PCI-X bus case study showed a superiority of our approach to conventional verification.