Search

It is commonly known that every reachable marking of a finite-state Petri net system is represented in its finite unfolding according to McMillan. Also the reachability of markings from each other is represented in the finite unfolding, but it is almost unknown that this information can be hidden very deep. This paper presents an efficient method for gaining this information, which is of course of great importance for potential modelcheckers working on finite unfoldings. All results presented in this paper also hold for a recently proposed optimized unfolding method. [ABSTRACT FROM AUTHOR]

We apply to Petri net theory the technique of polynomialtime many-one reductions. We study boundedness, reachability, deadlock, liveness problems and some of their variations. We derive three main results. Firstly, we highlight the power of expression of reachability which can polynomially give evidence of unboundedness. Secondly, we prove that reachability and deadlock are polynomially-time equivalent; this improves the known recursive reduction and it complements the result of Cheng and al. [4]. Moreover, we show the polynomial equivalence of liveness and t-liveness. Hence, we regroup the problems in three main classes: boundedness, reachability and liveness. Finally, we give an upper bound on the boundedness for post self-modified nets: $$2^{O(size(N)^2 *\log size(N))} $$ . This improves a decidability result of Valk [18]. [ABSTRACT FROM AUTHOR]

The algebra of M-nets, a high level class of labelled Petri nets, was introduced in the Petri Box Calculus in order to cope with the size problem of the low level nets, especially if applied as semantical domain for parallel programming languages. A general, unrestricted refinement operator intended to represent the procedure call mechanism for concurrent calls is introduced into the M-net calculus. Its coherence with the low level refinements is exhibited, together with its main properties. [ABSTRACT FROM AUTHOR]

Showing equivalence of two systems at different levels of abstraction often entails mapping a single step in one system to a sequence of steps in the other, where the relevant state information does not change until the last step. In [BCG 88,dNV 90], bisimulations that take into account such "stuttering" are formulated. These definitions are, however, difficult to use in proofs of bisimulation, as they often require one to exhibit a finite, but unbounded sequence of transitions to match a single transition; thus introducing a large number of proof obligations. We present an alternative formulation of bisimulation under stuttering, in terms of a ranking function over a well-founded set. It has the desirable property, shared with strong bisimulation [Mil 90], that it requires matching single transitions only, which considerably reduces the number of proof obligations. This makes proofs of bisimulation short, and easier to demonstrate and understand. We show that the new formulation is equivalent to the original one, and illustrate its use with non-trivial examples that have infinite state spaces and exhibit unbounded stuttering. [ABSTRACT FROM AUTHOR]

A new compositional logic for verifying safety properties of shared variable concurrency is presented, in which, in order to characterize infinite computations, a Hoare-style I/pre/post format is used where I expresses the communication interface, enabling the characterization of reactive programs. This logic relates to the Rely/Guarantee paradigm of Jones [11], in that Rely/Guarantee formulae can be expressed within our formalism. As novel feature we characterize prefixes of computations through so-called time-diagrams, a mapping from a discrete total wellfounded ordering to states, and combine these with action predicates (already introduced in old work of, e.g., Lamport) in order to obtain a compositional formalism. The use of time diagrams enables the expression of strongest postconditions and strongest invariants directly within the assertion language, instead of through encoding within the natural numbers. A proof of Dekker's mutual exclusion algorithm is given. [ABSTRACT FROM AUTHOR]

In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of a reactive program with its environment makes them particularly appropriate for the specification of open systems. Nevertheless, model-checking algorithms used for the verification of closed systems are not appropriate for the verification of open systems. Correct verification of open systems should check the system with respect to arbitrary environments and should take into account uncertainty regarding the environment. This is not the case with current model-checking algorithms and tools. Module checking is an algorithmic method that checks, given an open system (modeled as a finite structure) and a desired requirement (specified by a temporal-logic formula), whether the open system satisfies the requirement with respect to all environments. In this paper we describe and examine module checking problem, and study its computational complexity. Our results show that module checking is computationally harder than model checking. [ABSTRACT FROM AUTHOR]

In this paper we extend a key result of Nisan and Wigderson [17] to the nondeterministic setting: for all α > 0 we show that if there is a language in E = DTIME(2O(n)) that is hard to approximate by nondeterministic circuits of size 2αn, then there is a pseudorandom generator that can be used to derandomize BP·NP (in symbols, BP·NP = NP). By applying this extension we are able to answer some open questions in [14] regarding the derandomization of the classes BP·σkP and BP·θkP under plausible measure theoretic assumptions. As a consequence, if θ2P does not have p-measure 0, then AM ∩ coAM is low for θ2P. Thus, in this case, the graph isomorphism problem is low for θ2P. By using the Nisan-Wigderson design of a pseudorandom generator we unconditionally show the inclusion MA ⊑ ZPPNPNP and that MA∩ coMA is low for ZPPNP. [ABSTRACT FROM AUTHOR]

In order to study the complexity of computational problems that arise from group theory in a general framework, Babai and Szemerédi [4, 2] introduced the theory of black-box groups. They proved that several problems over black-box groups are in the class NP ∩ co-AM, thereby implying that these problems are low (powerless as oracle) for ∑2p and hence cannot be complete for NP unless the polynomial hierarchy collapses. In [1], Arvind and Vinodchandran study the counting complexity of a number of computational problems over solvable groups. Using a constructive version of a fundamental structure theorem about finite abelian groups and a randomized algorithm from [3] for computing generator sets for the commutator series of any solvable group, they prove that these problems are in randomized versions of low complexity counting classes like SPP and LWPP and hence low for the class PP. In this paper, we improve the upper bounds of [1] for these problems. More precisely, we avoid the randomized algorithm from [3] for computing the commutator series. This immediately places all these problems in either SPP or LWPP. These upper bounds imply lowness of these problems for classes other than PP. In particular, SPP is low for all gap-definable counting classes [9] (PP, C=P, ModkP etc) and LWPP is known to be low for PP and C=P. These results are in favor of the belief that these problems are unlikely to be complete for NP. [ABSTRACT FROM AUTHOR]

In this paper we improve on some results of [3] and extend them to the setting of implicit definability. We show a strong necessary condition on classes of structures on which PSPACE can be captured by extending PFP with a finite set of generalized quantifiers. For IFP and PTIME the limitation of expressive power of generalized quantifiers is shown only on some specific nontrivial classes. These results easily extend to implicit closure of these logics. In fact, we obtain a nearly complete characterization of classes of structures on which IMP(PFP) can capture PSPACE if finitely many generalized quantifiers are also allowed. We give a new proof of one of the main results of [3], characterizing the classes of structures on which L∞,ωω (Q) collapses to FO(Q), where Q is a set of finitely many generalized quantifiers. This proof easily generalizes to the case of implicit definability, unlike the quantifier elimination argument of [3] which does not easily get adapted to implicit definability setting. This result is then used to show the limitation of expressive power of implicit closure of L∞,ωω (Q). Finally, we adapt the technique of quantifier elimination due to Scott Weinstein, used in [3], to show that IMP(Lk(Q))-types can be isolated in the same logic. [ABSTRACT FROM AUTHOR]

The goal of this article is to provide a gentle introduction to the basic definitions, goals and constructions in coding theory. In particular we focus on the algorithmic tasks tackled by the theory. We describe some of the classical algebraic constructions of error-correcting codes including the Hamming code, the Hadamard code and the Reed Solomon code. We describe simple proofs of their error-correction properties. We also describe simple and efficient algorithms for decoding these codes. It is our aim that a computer scientist with just a basic knowledge of linear algebra and modern algebra should be able to understand every proof given here. We also describe some recent developments and some salient open problems. [ABSTRACT FROM AUTHOR]

We illustrate in this paper a compositional and stepwise method for designing programs that offer a potentially unique tolerance to each of their fault-classes. More specifically, our illustration is a design of a repetitive agreement program that offers two tolerances: (a) it masks the effects of Byzantine failures and (b) it is stabilizing in the presence of transient and Byzantine failures. [ABSTRACT FROM AUTHOR]

In the study of distributed systems, the assumption —commitment framework is crucial for compositional specification of processes. The idea is that we reason about each process separately, making suitable assumptions about other processes in the system. Symmetrically, each process commits to certain actions which the other processes can rely on. We study such a framework from an automata-theoretic viewpoint. We present systems of finite state automata which make assumptions about the behaviour of other automata and make commitments about their own behaviour. We characterize the languages accepted by these systems to be the regular trace languages (of Mazurkiewicz) over an associated independence alphabet, and present a syntactic characterization of these languages using top-level parallelism. The results smoothly generalize for automata over infinite words as well. [ABSTRACT FROM AUTHOR]

While it is well-known how normal logic programs may be viewed as a form of abduction and argumentation, the problem of how disjunctive programs may be used for abductive reasoning is rarely discussed. In this paper we propose an abductive semantics for disjunctive logic programs with default negation and show that Eshghi and Kowalski's abductive proof procedure for normal programs can be adopted to compute abductive solutions for disjunctive programs. [ABSTRACT FROM AUTHOR]

We study several data-structures and operations that commonly arise in parallel implementations of logic programming languages. The main problems that arise in implementing such parallel systems are abstracted out and precisely stated. Upper and lower bounds are derived for several of these problems. We prove a lower bound of Ω(log n) on the overhead incurred in implementing even a simplified version of or-parallelism. We prove that the aliasing problem in parallel logic programming is at least as hard as the union-find problem. We prove that an and-parallel implementation can be realized on an extended pointer machine with an O(1) overhead. [ABSTRACT FROM AUTHOR]

The use of a rewrite-based theorem prover for verifying properties of arithmetic circuits is discussed. A prover such as Rewrite Rule Laboratory (RRL) can be used effectively for establishing numbertheoretic properties of adders, multipliers and dividers. Since verification of adders and multipliers has been discussed elsewhere in earlier papers, the focus in this paper is on a divider circuit. An SRT division circuit similar to the one used in the Intel Pentium processor is mechanically verified using RRL. The number-theoretic correctness of the division circuit is established from its equational specification. The proof is generated automatically, and follows easily using the inference procedures for contextual rewriting and a decision procedure for the quantifier-free theory of numbers (Presburger arithmetic) already implemented in RRL. Additional enhancements to rewrite-based provers such as RRL that would further facilitate verifying properties of circuits with structure similar to that of the SRT division circuit are discussed. [ABSTRACT FROM AUTHOR]

In this paper we address the open problem of classifying the expressive power of classes of rewriting systems. We introduce a framework to reason about the relative expressive power between classes of rewrite system, with respect to every property of interest P. In particular, we investigate four main classes of rewriting systems: left-linear Term Rewriting Systems, Term Rewriting Systems, Normal Conditional Term Rewriting Systems and Join Conditional Term Rewriting Systems. It is proved that, for all the main properties of interest of rewriting systems (completeness, termination, confluence, normalization etc.) these four classes form a hierarchy of increasing expressive power, with two total gaps, between left-linear TRSs and TRSs, and between TRSs and normal CTRSs, and with no gaps between normal CTRSs and join CTRSs. Therefore, these results formally prove the strict increase of expressive power between left-linear and non left-linear term rewriting, and between unconditional and conditional term rewriting, and clarify in what sense normal CTRSs can be seen as equivalent in power to join CTRSs. [ABSTRACT FROM AUTHOR]

We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. Our main result is a direct proof, via a small-step unloading machine, of the correctness of compilation to a closure-based abstract machine. Our second result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of CIU equivalence for an object-oriented language. [ABSTRACT FROM AUTHOR]

We extend the well-known analysis of recursion-removal in first-order program schemes to a higher-order language of finitely typed and polymorphically typed functional programs, the semantics of which is based on call-by-name parameter-passing. We introduce methods for recursion-removal, i.e. for translating higher-order recursive programs into higher-order iterative programs, and determine conditions under which this translation is possible. Just as finitely typed recursive programs are naturally classified by their orders, so are finitely typed iterative programs. This syntactic classification of recursive and iterative programs corresponds to a semantic (or computational) classification: the higher the order of programs, the more functions they can compute. [ABSTRACT FROM AUTHOR]

Graph editing problems deal with the complexity of transforming a given input graph G from class Q to any graph H in the target class H by adding and deleting edges. Motivated by a physical mapping scenario in Computational Biology, we consider graph editing to the class of bipartite interval graphs (BIGs). We prove asymptotic and exact bounds on the minimum number of editions needed to convert a graph into a BIG. [ABSTRACT FROM AUTHOR]

We show that several discrepancy-like problems can be solved in NC2 nearly achieving the discrepancies guaranteed by a probabilistic analysis and achievable sequentially. For example, given a set system (X, S), where X is a ground set and S ⊑ 2X, a set R ⊑ X can be computed in NC2 so that, for each S ε S, the discrepancy $$\left\ {R \cap S\left - \right\bar R \cap S} \right\$$ is $$O\left( {\sqrt {\left S \right\log \left S \right} } \right)$$ . Whereas previous NC algorithms could only achieve $$O\left( {\sqrt {\left S \right^{1 + e} \log \left S \right} } \right)$$ , ours matches the probabilistic bound achieved sequentially within a multiplicative factor 1 + o(1). Other problems whose NC solution we improve are lattice approximation, ε-approximations of range spaces of bounded VC-exponent, sampling in geometric configuration spaces, approximation of integer linear programs, and edge coloring of graphs. [ABSTRACT FROM AUTHOR]

This paper introduces a 2-dimensional triangulation scheme based on a topological triangulation that approximates a given domain X within a specified Hausdorff distance from X. The underlying space of the resulting good quality triangulation is homeomorphic to X and contains either equilateral triangles or right angled triangles with 30‡, 60‡ and 90‡ angles. For a particular range of approximation tolerance, the number of triangles in the triangulation produced by the method is O(t log2t) where t is the number of triangles in an optimal triangulation where the optimum is taken over bounded aspect ratio triangulations satisfying a certain boundary condition with respect to X. The method can also produce a quadrangulation of X having similar properties. Relevant implementation issues and results are discussed. [ABSTRACT FROM AUTHOR]

The Queuing Shared Memory (qsm) model is a general purpose shared-memory model for parallel computation. The QSM provides a high-level shared-memory abstraction for effective parallel algorithm design, as well as the ability to capture bandwidth limitations, as evidenced by a randomized work-preserving emulation on the bsp, which is a lower-level, distributed-memory model. [ABSTRACT FROM AUTHOR]

Model checking is an automatic technique for verifying finite-state reactive systems, such as sequential circuit designs and communication protocols. Specifications are expressed in temporal logic, and the reactive system is modeled as a statetransition graph. An efficient search procedure is used to determine whether or not the state-transition graph satisfies the specifications. We describe the basic model checking algorithm and show how it can be used with binary decision diagrams to verify properties of large state-transition graphs. We illustrate the power of model checking to find subtle errors by verifying part of the Contingency Guidance Requirements for the Space Shuttle. [ABSTRACT FROM AUTHOR]