Proof systems for message-passing process algebras

We give sound and complete proof systems for a variety of bisimulation based equivalences over a message-passing process algebra. The process algebra is a generalisation of pureCCS where the actions consist of receiving and sending messages or data on communication channels; the standard prefixing operatora.p is replaced by the two operatorsc?x.p andc!e.p and in addition messages can be tested by a conditional construct. The various proof systems are parameterised on auxiliary proof systems for deciding on equalities or more general boolean identities over the expression language for data. The completeness of these proof systems are thus relative to the completeness of the auxiliary proof systems.     

Bisimilarity control of partially observed nondeterministic discrete event systems and a test algorithm

In this paper, the bisimilarity control of discrete event systems (DESs) under partial observations is investigated, where the plant and the specification are allowed to be nondeterministic. A notation of simulation-based controllability and a synchronization scheme for the supervised system are formalized based on the simulation relation between the specification and the plant. It is shown that the existence of bisimilarity supervisors is characterized by the notions of the simulation-based controllability and the language observability, which extends the traditional results of supervisory control from language equivalence to bisimulation equivalence. In addition, a polynomial algorithm to test the simulation-based controllability is developed by constructing a computing tree. This algorithm together with the test of language observability can be used to check the existence of bisimilarity supervisors.     

Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time

We prove that weak bisimilarity is decidable in polynomial time between finite-state systems and several classes of infinite-state systems: context-free processes and normed basic parallel processes (normed BPP). To the best of our knowledge, these are the first polynomial algorithms for weak bisimilarity problems involving infinite-state systems.     

CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems

Boolean equation systems (Bess) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking and model checking. These problems can be solved on the fly (i.e., without constructing explicitly the state space of the system under analysis) by using a demand-driven construction and resolution of the corresponding Bes. In this article, we present a generic software library dedicated to on-the-fly resolution of alternation-free Bess. Four resolution algorithms are currently provided by the library: algorithms A1 and A2 are general, the latter being optimized to produce small-depth diagnostics, whereas algorithms A3 and A4 are specialized for handling acyclic and disjunctive/conjunctive Bess in a memory-efficient way. The library has been developed within the Cadp verification toolbox using the generic Open/Caesar environment and is currently used for three purposes: on-the-fly equivalence checking modulo five widely used equivalence relations, on-the-fly model checking of regular alternation-free modal μ-calculus, and on-the-fly reduction of state spaces based on τ-confluence .     

Cryptanalysis of Liaw's broadcasting Cryptosystem

In 1999, Liaw proposed a new broadcasting cryptosystem, which requires smaller bandwidth as compared to the previously proposed broadcasting cryptosystems. However, this article will show that the proposed system is insecure enough by presenting a conspiracy attack on it. We will also point out some ambiguous problems in Liaw's paper. Moreover, we propose an improved broadcasting cryptosystem, which is a slight modification of the proposed system to overcome the conspiracy attack.     

Bisimilar linear systems

The notion of bisimulation in theoretical computer science is one of the main complexity reduction methods for the analysis and synthesis of labeled transition systems. Bisimulations are special quotients of the state space that preserve many important properties expressible in temporal logics, and, in particular, reachability. In this paper, the framework of bisimilar transition systems is applied to various transition systems that are generated by linear control systems. Given a discrete-time or continuous-time linear system, and a finite observation map, we characterize linear quotient maps that result in quotient transition systems that are bisimilar to the original system. Interestingly, the characterizations for discrete-time systems are more restrictive than for continuous-time systems, due to the existence of an atomic time step. We show that computing the coarsest bisimulation, which results in maximum complexity reduction, corresponds to computing the maximal controlled or reachability invariant subspace inside the kernel of the observations map. These results establish strong connections between complexity reduction concepts in control theory and computer science.     

Distributed On-the-Fly Equivalence Checking

On-the-fly equivalence checking consists in comparing two Labeled Transition Systems (Ltss) modulo a given equivalence relation by exploring them in a demand-driven way. Since it avoids the explicit construction of Ltss, this method is able to detect errors even in systems that are too large to fit in the memory of a computer. In this paper, we aim at further improving the performance of on-the-fly equivalence checking using several machines connected by a network. We propose DSolve, a new algorithm for distributed on-the-fly resolution of Boolean Equation Systems (Bess), which enables equivalence checking modulo various relations characterized in terms of Bess. DSolve serves as verification engine for the distributed version of Bisimulator, an on-the-fly equivalence checker developed within the Cadp verification toolbox using the Open/Cæsar environment. Our experimental measures show quasi-linear speedups and a good scalability of the distributed version of Bisimulator w.r.t. its sequential version.     

An operational semantics for a calculus for wireless systems

In wireless systems, the communication mechanism combines features of broadcast, synchrony, and asynchrony. We develop an operational semantics for a calculus of wireless systems. We present different Reduction Semantics and a Labelled Transition Semantics and prove correspondence results between them. Finally, we apply CWS to the modelling of the Alternating Bit Protocol, and prove a simple correctness result as an example of the kind of properties that can be formalized in this framework.A major goal of the semantics is to describe the forms of interference among the activities of processes that are peculiar of wireless systems. Such interference occurs when a location is simultaneously reached by two transmissions. The Reduction Semantics differ on how information about the active transmissions is managed.We use the calculus to describe and analyse a few properties of a version of the Alternating Bit Protocol.     

Repetition-based cooperative broadcasting for vehicular ad-hoc networks

In vehicular ad hoc networks, most of critical applications involved with safety rely on reliable broadcast communications with low latency. Recently, repetition-based protocols have been proposed to meet the requirements of timeliness and reliability for broadcasting. In these protocols, a sender repeatedly retransmits the broadcast message during the lifetime of the message. However, existing protocols face serious problems such as deterioration of the signal quality caused by wireless fading. In particular, since excessive repetitions might cause network congestion and waste channel resources, reliability of broadcasting should be achieved with as small a number of repetitions as possible. In this paper, we therefore propose a novel repetition-based broadcast protocol which exploits a cooperative diversity technique (called RB-CD) making a small number of repetitions robust for wireless fading. To support this cooperative diversity, neighboring nodes transmit the same message almost simultaneously (that is, using the same repetition pattern for each other) in order to form a virtual antenna array. The virtual antenna array achieves a diversity gain at the receivers. In the RB-CD protocol, the virtual antenna array consists of the source and some of its neighbors (called relays) which participate in repeating the transmission of a broadcast message. In addition, a new distributed relay selection algorithm is introduced in the RB-CD protocol. From the ns-2 simulation results, we verified that RB-CD provides a more reliable broadcasting service due to its capability of exploiting cooperative diversity.     

TSV: A novel energy efficient Memory Integrity Verification scheme for embedded systems

Embedded systems are ubiquitous in this era of portable computing. These systems are empowered to access, store and transmit abundance of critical information. Thus their security becomes a prime concern. Moreover, most of these embedded devices often have to operate under insecure environments where the adversary may acquire physical access. To provide security, cryptographic security mechanisms could be employed in embedded systems. However, these mechanisms consume excessive energy that cannot be tolerated by the embedded systems. Therefore with the focus on achieving energy efficiency in cryptographic Memory Integrity Verification (MIV) mechanism, we present a novel energy efficient approach called Timestamps Verification (TSV) to provide Memory Integrity Verification in embedded systems. This paper elaborates the proposed approach along with its theoretical evaluation, simulation results, and experimental evaluation. The results prove that the energy savings in the TSV approach are in the range of 36–81% when compared with traditional MIV mechanisms.     

A framework for specifying and verifying the behaviour of open systems

Coding no longer represents the main issue in developing software applications. It is the design and verification of complex software systems that require to be addressed at the architectural level, following methodologies which permit us to clearly identify and design the components of a system, to understand precisely their interactions, and to formally verify the properties of the systems. Moreover, this process is made even more complicated by the advent of the “network-centric” model of computation, where open systems dynamically interact with each other in a highly volatile environment. Many of the techniques traditionally used for closed systems are inadequate in this context.We illustrate how the problem of modeling and verifying behavioural properties of open system is addressed by different research fields and how their results may contribute to a common solution. Building on this, we propose a methodology for modeling and verifying behavioural aspects of open systems. We introduce the IP-calculus, derived from the π-calculas process algebra so as to describe behavioural features of open systems. We define a notion of partial correctness, acceptability, in order to deal with the intrinsic indeterminacy of open systems, and we provide an algorithmic procedure for its effective verification.     

Safety verification and reachability analysis for hybrid systems

Safety verification and reachability analysis for hybrid systems is a very active research domain. Many approaches that seem quite different, have been proposed to solve this complex problem. This paper presents an overview of various approaches for autonomous, continuous-time hybrid systems and presents them with respect to basic problems related to verification.     

Decidability of performance equivalence for basic parallel processes

We study an extension of the class of Basic Parallel Processes (BPP), in which actions are durational and urgent and parallel components have independent local clocks. The main result is decidability of strong bisimilarity, known also as performance equivalence, in this class. This extends the earlier decidability result for plain BPP by Christensen et al. Our decision procedure is based on decidability of the validity problem for Presburger arithmetic. We prove also polynomial complexity in positive-duration fragment, thus properly extending a previous result by Bérard et al. Both ill-timed and well-timed semantics are treated.     

Lower bounds for the polynomial calculus

We show that polynomial calculus proofs (sometimes also called Groebner proofs) of the pigeonhole principle must have degree at least over any field. This is the first non-trivial lower bound on the degree of polynomial calculus proofs obtained without using unproved complexity assumptions. We also show that for some modifications of , expressible by polynomials of at most logarithmic degree, our bound can be improved to linear in the number of variables. Finally, we show that for any Boolean function in n variables, every polynomial calculus proof of the statement “ cannot be computed by any circuit of size t,” must have degree . Loosely speaking, this means that low degree polynomial calculus proofs do not prove . Received: January 15, 1997.     

An enhanced recursive frequency splitting broadcasting algorithm for near video-on-demand services

This work presents a novel method for enhancing the recursive frequency splitting broadcasting algorithm proposed by Tseng et al. The proposed method outperforms the previous broadcasting methods in terms of the maximum waiting time, for the same number of channels.     

Clock synchronization and the power of broadcasting

Summary We investigate the power of a broadcast mechanism in a distributed network. We do so by considering the problem of synchronizing clocks in an errorfree network, under the assumption that there is no upper bound on message transmission time, but that broadcast messages are guaranteed to be received within an interval of size , for some fixed constant . This is intended to be an idealization of what happens in multiple access networks, such as the Ethernet. We then consider tradeoffs between the type and number of broadcasts, and the tightness of synchronization. Our results include (1) matching upper and lower bounds of (1+1/K) on the precision of clock synchronization attainable forn3 process usingK (n–1)-casts, 3Kn, (2) matching upper and lower bounds of (1+1/n) on the precision of clock synchronization attainable forn3 processes using an arbitrary number of (n–1)-casts, and (3) matching upper and lower bounds of (1+n–2/n) on the precision attainable using 2-casting. Joseph Y. Halpern received a B.Sc. in mathematics from the University of Toronto in 1975, and a Ph.D. in mathematics from Harvard University in 1981. In between, he spent two years as the head of the Mathematics Department at Bawku Secondary School in Ghara. After a year as a visiting scientist at MIT, he joined IBM in 1982, where he is currently a research staff member, as well as being a consulting professor at Stanford University. He was manager of the mathematics and related computer sience department at IBM from 1987–1989. He was program chairman and organizer of the first conference on Theoretical Aspects of Reasoning About Knowledge in 1986, program chairman of the 1986 ACM Symposium on Principles of Distributed Computing and of the 1991 ACM Symposium on Theory of Computing. He was recipent (together with Ron Fagin) of the MIT Publisher's Prize for best paper at the 1985 International Joint Conference on Artificial Intelligence and again winner of the Publisher's Prize at the 1989 International Joint Conference on Artificial Intelligence. Ichiro Suzuki is an Associate Professor of Computer Science at the University of Wisconsin-Milwaukee. He received a D.E. degree in information and computer sciences from Osaka University, Japan, in 1983. His major research interests are distributed systems and computational geometry.This author was supported in part by the National Science Foundation under grant CCR-9004346     

On the efficiency of secure XML broadcasting

Secure broadcasting of web documents is becoming a crucial requirement for many web-based applications. Under the broadcast document dissemination strategy, a web document source periodically broadcasts (portions of) its documents to a potentially large community of users, without the need for explicit requests. By secure broadcasting, we mean that the delivery of information to users must obey the access control policies of the document source. Traditional access control mechanisms that have been adapted for XML documents, however, do not address the performance issues inherent in access control. In this paper, a labeling scheme is proposed to support rapid reconstruction of XML documents in the context of a well-known method, called XML pool encryption. The proposed labeling scheme supports the speedy inference of structure information in all portions of the document. The binary representation of the proposed labeling scheme is also investigated. In the experimental results, the proposed labeling scheme is efficient in searching for the location of decrypted information.     

Bisimilar control affine systems

The notion of bisimulation plays a very important role in theoretical computer science where it provides several notions of equivalence between models of computation. These equivalences are in turn used to simplify verification and synthesis for these models as well as to enable compositional reasoning. In systems theory, a similar notion is also of interest in order to develop modular verification and design tools for purely continuous or hybrid control systems. In this paper, we introduce two notions of bisimulation for nonlinear systems. We present differential geometric characterizations of these notions and show that bisimilar systems of different dimensions are obtained by factoring out certain invariant distributions. Furthermore, we also show that all bisimilar systems of different dimension are of this form.