生成诊断公式的有限状态进程等价验证

分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题.给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统.给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式.算法的时间复杂度为O(m log n),空间复杂度为O(m+n).     

Adaptive Verification using Forced Simulation

Simulation (a pre-order) over Kripke structures is a well known formal verification technique. Simulation guarantees that all behaviours of an abstracted structure (a property or function, F) are contained in a larger structure (a model M). A model, however, may not always simulate a property due to the presence of design errors. In this case, the model is debugged manually. In this paper, we propose a weaker simulation over structures called forced simulation for automated debugging. Forced simulation is applied when normal simulation fails. Forced simulation between a model (M) and a function (F) guarantees the existence of a modifier, D, to adapt M so that the composition of M and D is observationally equivalent to F. Observational equivalence over structures called weak bisimulation is developed in this paper. It is also established that when two structures are weakly bisimilar all CTL^* properties holding over one also holds over the other structure. Forced simulation based algorithm has been used to adapt many designs which had failed certain properties during conventional verification.     

Decision procedures and graph reductions for bisimulation equivalences part 1

In Process Algebra, processes are often specified in a framework of bisimulation semantics. The notion of bisimulation therefore plays an important role.

In this paper some existing and new decision methods are presented for strong bisimulation, τ-bisimulation and η-bisimulation. Each of these bisimulation equivalences corresponds to a certain abstraction mechanism.

In strong bisimulation, all events in a system are treated equally whereas τ-bisimulation takes into account the silent step τ; η-bisimulation was introduced recently for an alternative silent step η that is less abstract than τ. It is shown that the problem of η-bisimulation decision can be reduced to an abstract graph partitioning problem called the Product Relational Coarsest Partition problem. Special attention is paid to computational complexity of the decision methods.

As it turns out. finite process graphs can be reduced to unique minimal normalforms under all three bisimulation semantics mentioned.

The last section demonstrates how the decision methods can be used with a particular algebraic model to enable effective verification of specifications.     

Visual coding by optimal graph-coloring

A formal study of visual codings in user interface design is presented. Visual codings for maximum distinction of different objects in displayed images are formulated as a discrete optimization problem of maximum-distance graph-coloring. The formulation is a generalization of the classical coloring problem in graph theory. Having pointed out that maximum-distance graph-coloring is NP-complete, we develop new, fast approximation algorithms for optimal visual codings. The proposed algorthms run inO (M N) time, whereM is the number of visual codes used andN is the number of objects to be encoded. Besides being efficient, the algorithms are simple and easy to implement. Our experiments showed that geographic maps automatically colored by the new algorithms were preferred to those colored by the previous graph-theoretical approach and they are competitive, if not better, in terms of the visual distinction of different regions than those drawn by hand.Supported by grans from Natural Science and Enginneering Research Council of Canada     

A note on the size of OBDDs for the graph of integer multiplication

Integer multiplication as one of the basic arithmetic functions has been in the focus of several complexity theoretical investigations and ordered binary decision diagrams (OBDDs) are the most common dynamic data structure for Boolean functions. Among the many areas of application are verification, model checking, computer-aided design, relational algebra, and symbolic graph algorithms. Analyzing the limits of symbolic graph algorithms for the all-pairs-shortest paths problem which work on OBDD-represented graph instances the so-called graph of integer multiplication has been investigated by Sawitzki [D. Sawitzki, Lower bounds on the OBDD size of graphs of some popular functions, in: Proc. of SOFSEM, LNCS, vol. 3381, 2005, pp. 298-309]. Using simple arguments his lower bound of ²n/768−1 on the size of OBDDs representing the graph of integer multiplication is improved up to ²n/24.     

Memory-efficient algorithms for the verification of temporal properties

This article addresses the problem of designing memory-efficient algorithms for the verification of temporal properties of finite-state programs. Both the programs and their desired temporal properties are modeled as automata on infinite words (Büchi automata). Verification is then reduced to checking the emptiness of the automaton resulting from the product of the program and the property. This problem is usually solved by computing the strongly connected components of the graph representing the product automaton. Here, we present algorithms that solve the emptiness problem without explicitly constructing the strongly connected components of the product graph. By allowing the algorithms to err with some probability, we can implement them with a randomly accessed memory of size O(n) bits, where n is the number of states of the graph, instead of O(n log n) bits that the presently known algorithms require.     

Exact OBDD Bounds for Some Fundamental Functions

Ordered binary decision diagrams (OBDDs) are nowadays one of the most common dynamic data structures or representation types for Boolean functions. Among the many areas of application are verification, model checking, computer aided design, relational algebra, and symbolic graph algorithms. Although many exponential lower bounds on the OBDD size of Boolean functions are known, there are only few functions where the OBDD size is asymptotically known exactly. In this paper the exact OBDD sizes of the fundamental functions multiplexer and addition of n-bit numbers are determined.     

Finding the closed partition of a planar graph

In this paper we consider the problem of finding aclosed partition in a directed graph. This problem has applications in concurrent probabilistic program verification. The best sequential algorithm known for this problem runs inO(mn) time wherem is the number of directed edges andn is the number of vertices in the given digraph. In this paper we present a linear-time sequential algorithm to solve the closed partition problem for planar digraphs that arecompact. We then build on this algorithm to obtain an O(n^1.5)-time sequential algorithm to solve the closed partition problem for a general planar digraph.This work was supported in part by NSF Grant CCR 89-10707.     

Parallel PROFIT/COST algorithms through fast derandomization

We present parallel algorithms for the PROFIT/COST problem with time complexity using O(m+n) processors. The design of these algorithms employ both the derandomization technique and the pipeline technique. They can be used to partition the vertices of a graph into two sets such that the number of edges incident with vertices in both sets is at least half of the total number of edges in the graph. Parallel algorithms for the PROFIT/COST problem have known applications in the design of parallel algorithms for several graph problems. Received: 18 March 1992 / 8 January 1999     

Computing Bisimulations for Finite-Controlπ-Calculus

Symbolic bisimulation avoids the infinite branching problem caused by instantiating input names with all names in the standard definition of bisimulation in π-calculus.However,it does not automatically lead to an efficient algorithm,because symbolic bisimulation is indexed by conditions on names,and directly manipulating such conditions can be computationally costly.In this paper a new notion of bisimulation is introduced,in which the manipulation of maximally consistent conditions is replaced with a systematic employment of schematic names.It is shown that the new notion captures symbolic bisimulation in a precise sense.Based on the new definition an efficient algorithm,which instantiates input names “on-the -fly“,is presented to check bisimulations for finite-control π-calculus.     

O-Minimal Hybrid Systems

An important approach to decidability questions for verification algorithms of hybrid systems has been the construction of a bisimulation. Bisimulations are finite state quotients whose reachability properties are equivalent to those of the original infinite state hybrid system. In this paper we introduce the notion of o-minimal hybrid systems, which are initialized hybrid systems whose relevant sets and flows are definable in an o-minimal theory. We prove that o-minimal hybrid systems always admit finite bisimulations. We then present specific examples of hybrid systems with complex continuous dynamics for which finite bisimulations exist. Date received: June 9, 1998. Date revised: June 28, 1999.     

Bisimulation equivalence of differential-algebraic systems

In this paper, the notion of bisimulation relation for linear input-state-output systems is extended to general linear differential-algebraic (DAE) systems. Geometric control theory is used to derive a linear-algebraic characterisation of bisimulation relations, and an algorithm for computing the maximal bisimulation relation between two linear DAE systems. The general definition is specialised to the case where the matrix pencil sE ? A is regular. Furthermore, by developing a one-sided version of bisimulation, characterisations of simulation and abstraction are obtained.     

Analysis of Timed Systems Using Time-Abstracting Bisimulations

The objective of this paper is to show how verification of dense-time systems modeled as timed automata can be effectively performed using untimed verification techniques. In that way, the existing rich infrastructure in algorithms and tools for the verification of untimed systems can be exploited. The paper completes the ideas introduced in (Tripakis and Yovine, 1996, in Proc. 8th Conf. Computer-Aided Verification, CAV'96, Rutgers, NJ. LNCS, Vol. 1102, Springer-Verlag, 1996, pp. 232–243).Our approach consists in two steps. First, given a timed system A, we compute a finite graph G which captures the behavior of A modulo the fact that exact time delays are abstracted away. Then, we apply untimed verification techniques on G to prove properties on A. As property-specification languages, we use both the linear-time formalism of timed Büchi automata (TBA) and the branching-time logic TCTL. Model checking A against properties specified as TBA or TCTL formulae comes down to applying, respectively, automata-emptiness or CTL model-checking algorithms on G.The abstraction of exact delays is formalized under the concept of time-abstracting bisimulations. We define three time-abstracting bisimulations which are strictly ordered with respect to their reduction power. The stronger of them preserves both linear- and branching-time properties whereas the two weaker ones preserve only linear-time properties.The finite graph G is the quotient A with respect to a time-abstracting bisimulation. Generating G is called minimization and can be done by adapting a partition-refinement algorithm to the timed case. The adapted algorithm is symbolic, that is, equivalence classes are represented as simple polyhedra. When these polyhedra are not convex, operations become expensive, therefore, we develop a partition-refinement technique which preserves convexity.We have implemented the minimization algorithm in a prototype module called minim, as part of the real-time verification platform KRONOS (Bozga et al., 1998, in CAV'98). minim connects KRONOS to the CADP tool suite for the verification of untimed graphs (Fernandez et al., 1992, in 14th Int. Conf. on Software Engineering). To demonstrate the practical interest behind our approach, we present two case studies, namely, Fischer's mutual exclusion protocol and the CSMA/CD communication protocol.     

An experimental evaluation of local search heuristics for graph partitioning

A common problem that arises in many applications is to partition the vertices of a graph intok subsets, each containing a bounded number of vertices, such that the number of graph edges with endpoints in different subsets is minimized. This paper describes an empirical study of the performance of various local search heuristics for thisk-way graph partitioning problem. The heuristics examined are local optimization, simulated annealing, tabu search, and genetic algorithms. In addition, the hierarchical hybrid approach is introduced, in which the problem is recursively decomposed into small pieces, to which local search heuristics are then applied.     

Work-efficient BSR-based parallel algorithms for some fundamental problems in graph theory

This paper presents BSR-parallel algorithms for some problems in fundamental graph theory : transitive closure, connected components, spanning tree, bridges and articulation points of a graph and bipartite graph recognition. There already exist constant time algorithms to solve these problems on a mesh with reconfigurable bus system using O(N ⁴) processors. Here we show that these problems can be solved in constant time using only O(N ²) processors on the BSR model (N is the number of vertices of the graph G). Therefore, our algorithms are more work-efficient. These new results suggest that many other problems in graph theory can be solved in constant time using the BSR model.     

离散事件系统拟同余关系的改进算法

针对离散事件系统, 本文主要研究计算最优拟同余关系时减少时间复杂度的算法. 基于Paige & Tarjan提出且Fernandez修改的、可有效计算最粗粒度划分问题的算法, 本文给出一种时间复杂度为O(mlog n)的计算最优拟同余关系的算法. 该算法适用于离散事件系统比较复杂, 尤其是可观事件很少的情况. 与Ramadge和Wonham提出的时间复杂度为O(mn)的算法相比, 该算法计算过程耗时较短. 本文还讨论了计算拟同余关系的边界情况的改进方法. 仿真结果表明所提出算法的有效性.     

Bisimulation, the Supervisory Control Problem and Strong Model Matching for Finite State Machines

A fundamental relationship between the controllability of a language with respect to another language and a set of uncontrollable events in the Supervisory Control Theory initiated by (Ramadge and Wonham, 1989) and bisimulation of automata models is derived. The theoretical results relating bisimulation to controllability support an efficient solution to the Basic Supervisory Control Problem. Using (Fernandez, 1990) generalization of the partition refinement algorithm of (Paige and Tarjan, 1987), it is possible to find a partition which represents the supremal controllable sublanguage of an automaton with respect to the language of another automaton and a set of events in a worst-case running time of O( m log(n)), where m is the number of transitions and n is the number of states. Utilizing the bisimulation property of language controllability and derived relationships between automata languages and input/output finite-state machine behaviors, a precise relationship is formally derived between Supervisory Control Theory and the system-theoretic problem posed by (DiBenedetto et al., 1994) called Strong Input/Output FSM Model Matching. Specifically, it is proven that in deterministic settings instances of each problem can be mapped to the other framework and solved.     

Applying formal concepts to learning systems validation

In the problem area of evaluating complex software systems, there are two distinguished areas of research, development, and application identified by the two buzzwords validation and verification, respectively. From the perspective adopted by the authors, verification is usually more formally based and, thus, can be supported by formal reasoning tools like theorem provers, for instance. The scope of verification approaches is limited by the difficulty of finding a sufficiently complete formalization to build upon. In paramount realistic problem domains, validation seems to be more appropriate, although it is less stringent in character and, therefore, validation results are often less definite. The aim of this paper is to exemplify a validation approach based on a clear and thoroughly formal theory. In this way, validation and verification should be brought closer to each other. To allow for precise and sufficiently clear results, the authors have selected the application domain of algorithms and systems for learning formal languages. By means of the validation toolkit TIC, some series of validation experiments have been performed. The results are presented for the sake of illustrating the underlying formal concepts in use. Comparing the validity of one learning approach to the invalidity of another one can be seen as an interesting result in its own right.     

基于极大团和FP-Tree的挖掘关联规则的改进算法

融合了关联规则挖掘的FP-Tree算法和图论的极大团理论的优势,做了以下主要工作:(1) 提出了用邻接矩阵的产生频繁2-项集的改进方法;(2) 提出了极大有序频繁集的概念,证明了Head关系的等价性、划分定理、局部复杂性定理和归并收敛值域定理;(3) 提出并实现了基于极大团划分的MaxCFPTree算法,扫描时间复杂性小于O(n²);(4) 做了相关实验,以验证算法的正确性.新方法缓解了项目数量巨大而内存不足的矛盾,提高了系统效率和伸缩性.     

Bisimulation Minimization and Symbolic Model Checking

State space minimization techniques are crucial for combating state explosion. A variety of explicit-state verification tools use bisimulation minimization to check equivalence between systems, to minimize components before composition, or to reduce a state space prior to model checking. Experimental results on bisimulation minimization in symbolic model checking contexts, however, are mixed. This paper explores bisimulation minimization as an optimization in symbolic model checking of invariance properties. We consider three bisimulation minimization algorithms. From each, we produce a BDD-based model checker for invariant properties and compare this model checker to a conventional one based on backwards reachability. Our comparisons, both theoretical and experimental, suggest that bisimulation minimization is not viable in the context of invariance verification, because performing the minimization requires as many, if not more, computational resources as model checking the unminimized system through backwards reachability.