Probabilistic and nondeterministic aspects of anonymity

The concept of anonymity comes into play in a wide range of situations, varying from voting and anonymous donations to postings on bulletin boards and sending emails. The protocols for ensuring anonymity often use random mechanisms which can be described probabilistically, while the agents’ behavior may be totally unpredictable, irregular, and hence expressible only nondeterministically. Formal definitions of the concept of anonymity have been investigated in the past either in a totally nondeterministic framework, or in a purely probabilistic one. In this paper, we investigate a notion of anonymity which combines both probability and nondeterminism, and which is suitable for describing the most general situation in which the protocol and the users can have both probabilistic and nondeterministic behavior. We also investigate the properties of the definition for the particular cases of purely nondeterministic users and purely probabilistic users. We formulate the notions of anonymity in terms of probabilistic automata, and we describe protocols and users as processes in the probabilistic π-calculus, whose semantics is again based on probabilistic automata. Throughout the paper, we illustrate our ideas by using the example of the dining cryptographers.     

Distance automata having large finite distance or finite ambiguity

A distance automaton is a (nondeterministic finite) automaton which is equipped with a nonnegative cost function on its transitions. The distance of a word recognized by such a machine quantifies the expenses associated with the recognition of this word. The distance of a distance automaton is the maximal distance of a word recognized by this machine or is infinite, depending on whether or not a maximum exists. We present distance automata havingn states and distance 2 ⁿ – 2. As a by-product we obtain regular languages having exponential finite order. Given a finitely ambiguous distance automaton withn states, we show that either its distance is at most 3 ⁿ – 1, or the growth of the distance in this machine is linear in the input length. The infinite distance problem for these distance automata is NP-hard and solvable in polynomial space. The infinite-order problem for regular languages is PSPACE-complete.A preliminary version of this article appeared in theProceedings of the 15th Symposium on Mathematical Foundations of Computer Science, 1990.     

Probabilistic π-Calculus and Event Structures

This paper proposes two semantics of a probabilistic variant of the π-calculus: an interleaving semantics in terms of Segala automata and a true concurrent semantics, in terms of probabilistic event structures. The key technical point is a use of types to identify a good class of non-deterministic probabilistic behaviours which can preserve a compositionality of the parallel operator in the event structures and the calculus. We show an operational correspondence between the two semantics. This allows us to prove a “probabilistic confluence” result, which generalises the confluence of the linearly typed π-calculus.     

Algorithm-based fault tolerance for matrix inversion with maximum pivoting

Existing fault-tolerant matrix-inversion schemes suffer several drawbacks, such as being limited to fault detection, requiring rollback to resume computation, cost ineffectiveness, instability, significant roundoff errors, and potential false alarms. In this paper, an algorithm-based fault-tolerant scheme for matrix inversion with maximum pivoting that can rectify the above problems is presented. This scheme can correct a single fault and detect multiple faults in each row and column in each iteration within a computation. The sequential and parallel algorithms based on checksums to support the fault-tolerant capability are developed. In this scheme, redundant processing elements needed and additional overhead for the enhanced fault correcting ability are relatively small compared to those in existing schemes. An implementation example that performs n × n matrix inversion with maximum pivoting on an (n + 1) × (n + 1) mesh-connected array processor with a time complexity of O(n²) is also described.     

Inclusion dynamics hybrid automata

Hybrid systems are dynamical systems with the ability to describe mixed discrete-continuous evolution of a wide range of systems. Consequently, at first glance, hybrid systems appear powerful but recalcitrant, neither yielding to analysis and reasoning through a purely continuous-time modeling as with systems of differential equations, nor open to inferential processes commonly used for discrete state-transition systems such as finite state automata. A convenient and popular model, called hybrid automata, was introduced to model them and has spurred much interest on its tractability as a tool for inference and model checking in a general setting. Intuitively, a hybrid automaton is simply a “finite-state” automaton with each state augmented by continuous variables, which evolve according to a set of well-defined continuous laws, each specified separately for each state. This article investigates both the notion of hybrid automaton and the model checking problem over such a structure. In particular, it relates first-order theories and analysis results on multivalued maps and reduces the bounded reachability problem for hybrid automata whose continuous laws are expressed by inclusions (x′f(x,t)) to a decidability problem for first-order formulæ over the reals. Furthermore, the paper introduces a class of hybrid automata for which the reachability problem can be decided and shows that the problem of deciding whether a hybrid automaton belongs to this class can be again decided using first-order formulæ over the reals. Despite the fact that the bisimulation quotient for this class of hybrid automata can be infinite, we show that our techniques permit effective model checking for a nontrivial fragment of CTL.     

Fully Scalable Fault-Tolerant Simulations for BSP and CGM

In this paper we consider general simulations of algorithms designed for fully operational BSP and CGM machines on machines with faulty processors. The BSP (or CGM) machine is a parallel multicomputer consisting of p processors for which a memory of n words is evenly distributed and each processor can send and receive at most h messages in a superstep. The faults are deterministic (i.e., worst-case distributions of faults are considered) and static (i.e., they do not change in the course of computation). We assume that a constant fraction of processors are faulty.  We present two fault-tolerant simulation techniques for BSP and CGM:  1. A deterministic simulation that achieves O(1) slowdown for local computations and O((log_h p)²) slowdown for communications per superstep, provided that a preprocessing is done that requires O((log_h p)²) supersteps and linear (in h) computation per processor in each superstep.  2. A randomized simulation that achieves O(1) slowdown for local computations and O(log_h p) slowdown for communications per superstep with high probability, after the same (deterministic) preprocessing as above.  Our results are fully scalable over all values of p from Θ(1) to Θ(n). Furthermore, our results imply that if pn for 0<<1 and h=Θ((n/p)^δ) for 0<δ1 (which hold in almost all practical BSP and CGM computations), algorithms can be made resilient to a constant fraction of processor faults without any asymptotic slowdown.     

Two-Pass Rearrangeability in Faulty Benes Networks

Existing fault-tolerant routing schemes for Benes networks either consider only the control line stuck-at faults, or handle the switch faults by some graceful degradation routing schemes that reconfigure the network into a smaller system with minimal loss. Now, even in the presence of a single switch fault in anN×NBenes networkB(n), (n= log₂N), noN×Npermutation can be realized in a single pass. In this paper, we attempt to characterize the switch fault sets inB(n), in the presence of which the network is always capable of realizing any arbitraryN×NpermutationPin two passes, such that any source–destination path is set up in a single pass, no recirculation is needed, but the whole set ofNsource–destination paths ofPis partitioned in two subsets and are realized in two successive passes. We propose an algorithm that will detect if the switch fault set present in aB(n), belongs to this class; if it is yes, we present another algorithm that computes the fault-tolerant routing to realize any arbitrary permutationPin two passes. This scheme enables us to makeB(n) fault-tolerant in the presence of a restricted class of multiple switch faults, without any recirculation through intermediate nodes, or any reconfiguration of the system.     

Symbolic model checking for probabilistic timed automata

Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton’s clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of probabilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies.     

The query complexity of order-finding

We consider the problem where π is an unknown permutation on {0,1,…,2ⁿ−1}, y₀{0,1,…,2ⁿ−1}, and the goal is to determine the minimum r>0 such that π^r(y₀)=1. Information about π is available only via queries that yield π^x(y) from any x{0,1,…,2^m−1} and y{0,1,…,2ⁿ−1} (where m is polynomial in n). The main resource under consideration is the number of these queries. We show that the number of queries necessary to solve the problem in the classical probabilistic bounded-error model is exponential in n. This contrasts sharply with the quantum bounded-error model, where a constant number of queries suffices.     

On the Construction of Fault-Tolerant Cube-Connected Cycles Networks

This paper presents a new approach to tolerating edge faults and node faults in (CCC) networks of Cube-Connected Cycles in a worst-case scenario. Our constructions of fault-tolerant CCC networks are obtained by adding extra edges to the CCC. The main objective is to reduce the cost of the fault-tolerant network by minimizing the degree of the network. Specifically, we have two main results. (i) We have created a fault tolerant CCC that can tolerate any single fault, either a node fault or an edge fault. When the dimension of the CCC is odd, the degree of the fault tolerant graph is 4. In the even case, there is a single node per cycle that is of degree 5 and the rest are of degree 4. (ii) We have created a fault-tolerant CCC, where every node has degree y + 2, which can tolerate any 2y − 1 cube-edge faults. Our constructions are extremely efficient for the case of edge faults-they result in healthy CCC networks that utilize all of the processors.     

Liveness Checking as Safety Checking for Infinite State Spaces

In previous work we have developed a syntactic reduction of repeated reachability to reachability for finite state systems. This may lead to simpler and more uniform proofs for model checking of liveness properties, help to find shortest counterexamples, and overcome limitations of closed-source model-checking tools. In this paper we show that a similar reduction can be applied to a number of infinite state systems, namely, (ω−)regular model checking, push-down systems, and timed automata.     

Bounded Model Checking for Timed Automata

Given a timed automaton M, a linear temporal logic formula φ, and a bound k, bounded model checking for timed automata determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification φ. This problem can be reduced to the satisfiability problem for Boolean constraint formulas over linear arithmetic constraints. We show that bounded model checking for timed automata is complete, and we give lower and upper bounds for the length k of counterexamples. Moreover, we define bounded model checking for networks of timed automata in a compositional way.     

Model checking for a probabilistic branching time logic with fairness

We consider concurrent probabilistic systems, based on probabilistic automata of Segala & Lynch [55], which allow non-deterministic choice between probability distributions. These systems can be decomposed into a collection of “computation trees” which arise by resolving the non-deterministic, but not probabilistic, choices. The presence of non-determinism means that certain liveness properties cannot be established unless fairness is assumed. We introduce a probabilistic branching time logic PBTL, based on the logic TPCTL of Hansson [30] and the logic PCTL of [55], resp. pCTL [14]. The formulas of the logic express properties such as “every request is eventually granted with probability at least p”. We give three interpretations for PBTL on concurrent probabilistic processes: the first is standard, while in the remaining two interpretations the branching time quantifiers are taken to range over a certain kind of fair computation trees. We then present a model checking algorithm for verifying whether a concurrent probabilistic process satisfies a PBTL formula assuming fairness constraints. We also propose adaptations of existing model checking algorithms for pCTL [4, 14] to obtain procedures for PBTL under fairness constraints. The techniques developed in this paper have applications in automatic verification of randomized distributed systems. Received: June 1997 / Accepted: May 1998     

Decision problems for lower/upper bound parametric timed automata

We investigate a class of parametric timed automata, called lower bound/upper bound (L/U) automata, where each parameter occurs in the timing constraints either as a lower bound or as an upper bound. For such automata, we show that basic decision problems, such as emptiness, finiteness and universality of the set of parameter valuations for which there is a corresponding infinite accepting run of the automaton, is Pspace-complete. We extend these results by allowing the specification of constraints on parameters as a linear system. We show that the considered decision problems are still Pspace-complete, if the lower bound parameters are not compared with the upper bound parameters in the linear system, and are undecidable in general. Finally, we consider a parametric extension of MITL\mathsf{MITL} _0,∞, and prove that the related satisfiability and model checking (w.r.t. L/U automata) problems are Pspace-complete.     

Implicit fault-tolerant control: application to induction motors

In this paper we propose an innovative way of dealing with the design of fault-tolerant control systems. We show how the nonlinear output regulation theory can be successfully adopted in order to design a regulator able to offset the effect of all possible faults which can occur and, in doing so, also to detect and isolate the occurred fault. The regulator is designed by embedding the (possible nonlinear) internal model of the fault. This idea is applied to the design of a fault-tolerant controller for induction motors in presence of both rotor and stator mechanical faults.     

Interval Duration Logic: Expressiveness and Decidability

We investigate a variant of dense-time Duration Calculus which permits model checking using timed/hybrid automata. We define a variant of the Duration Calculus, called Interval Duration Logic, (IDL), whose models are timed state sequences [1].A subset LIDL of IDL consisting only of located time constraints is presented. As our main result, we show that the models of an LIDL formula can be captured as timed state sequences accepted by an event-recording integrator automaton. A tool called IDLVALID for reducing LIDL formulae to integrator automata is briefly described. Finally, it is shown that LIDL has precisely the expressive power of event-recording integrator automata, and that a further subset LIDL- corresponds exactly to event-recording timed automata [2]. This gives us an automata-theoretic decision procedure for the satisfiability of LIDL– formulae.     

Robust satisfactory fault-tolerant control of uncertain linear discrete-time systems: an LMI approach

Fault-tolerant control is an important issue in practical systems. Based on satisfactory control and estimation theory, a passive fault-tolerant control strategy is proposed for a class of uncertain linear discrete-time systems in this article. Manipulating linear matrix inequality (LMI) technique, robust fault-tolerant state-feedback controllers are designed which take the possible actuator faults and sensor faults into consideration, respectively. The closed-loop systems are guaranteed by the designed controllers to meet the required constraints on regional pole index φ(q, r), steady-state variance matrix X index and control-cost function V ²(u) index simultaneously. Then, whether possible faults occur or not, the closed-loop systems would maintain the three desirable performance indices accordingly. Meanwhile, the consistency of the performance indices mentioned earlier is also discussed for fault-tolerant control.     

Testing for independence in heavy-tailed time series using the codifference function

In this paper, we consider a Portmanteau-type test of randomness for symmetric α stable random variables with exponent 0<α≤2, using a test statistic that differs from, but has the same general form as Box–Pierce Q-statistic, which is defined using the codifference function. We obtain that unlike a similar test proposed in [Runde, R., 1997. The asymptotic null distribution of the Box–Pierce Q-statistic for random variables with infinite variance—with an application to German stock returns. Journal of Econometrics 78, 205–216], the asymptotic distribution of the proposed statistic is similar to the classical case, that is asymptotically χ² distributed, both in finite and infinite variance cases. Simulation studies are performed to obtain the small sample performance of the proposed statistic. We found that the proposed statistic works fairly well, in the sense that in the infinite variance case, under suitable choice of the design parameter, its empirical levels are closer to the theoretical ones than Runde’s statistic. In the finite variance case, its empirical level is approximately the same as that of Ljung–Box’s statistic [Ljung, G.M. and Box, G.E.P., 1978. On a measure of lack of fit in time series models. Biometrika 65, 297–303]. Furthermore, the statistic also has good power against the AR(1) alternative. We provide an empirical example using some stocks chosen from the LQ45 index listed in the Indonesia Stock Exchange (IDX).     

The sample complexity of worst-case identification of FIR linear systems

We consider the problem of identification of linear systems in the presence of measurement noise which is unknown but bounded in magnitude by some δ > 0. We focus on the case of linear systems with a finite impulse response. It is known that the optimal identification error is related (within a factor of 2) to the diameter of a so-called uncertainty set and that the latter diameter is upper-bounded by 2δ, if a sufficiently long identification experiment is performed. We establish that, for any K 1, the minimal length of an identification experiment that is guaranteed to lead to a diameter bounded by 2Kδ behaves like 2^Nf(1/K), when N is large, where N is the length of the impulse response and is a positive function known in closed form. While the framework is entirely deterministic, our results are proved using probabilistic tools.     

基于SMT的PTACTL限界模型检测方法

概率时间自动机是在时间自动机的基础上加上各个状态迁移的概率以后形成的一种扩展的时间自动机,能用来对基于时间的随机协议、容错系统等进行建模,具有很强的实用性。本文针对概率时间自动机给出一种基于SMT的限界模型检测方法来验证该模型下的PTACTL性质,该方法由基于SMT的限界模型检测算法演变而来,通过将迁移时间和迁移概率融入ACTL性质中,改变模型的编码以及待验证性质的编码方式来实现对性质的验证。通过2个实例说明检测过程的有效性和高效性。