We present a characterization that shows what it means for a formula to be a weak or strong version of another formula. We show that the weak version of a formula is not the same as Alpern and Schneider's safety component, but can be achieved by taking the closure in the Cantor topology over an augmented alphabet in which every formula is satisfiable. The resulting characterization allows us to show that the set of semantically weak formulas is exactly the set of nonpathological safety formulas. Furthermore, we use the characterization to show that the original versions of the ieee standard temporal logics psl and sva are broken, and we show that the source of the problem lies in the semantics of the sere intersection and fusion operators. Finally, we use the topological characterization to show the internal consistency of the alternative semantics adopted by the latest version of the psl standard.

The verification community anticipates the adoption of assertions in the Analog and Mixed-Signal (AMS) domain in the near future. Several questions need to be answered before AMS assertions are brought into practice, such as: (a) How will the languages for AMS assertions be different from the ones in the digital domain? (b) Does the analog simulator have to be assertion aware? (c) If so, then how and where on the time line will the AMS assertion checker synchronize with the analog simulator? and (d) What will be the performance penalty for monitoring AMS assertions accurately over analog simulation? This article attempts to answer these questions through theoretical analysis and empirical results obtained from industrial test cases. We study logics which extend Linear Temporal Logic (LTL) with predicates over real variables, and show that further extensions allowing the binding of real-valued variables across time makes the logic undecidable. We present a toolkit which can integrate with existing AMS simulators for checking AMS assertions on practical designs. We study the problem of synchronizing the AMS simulator with the AMS assertion checker and demonstrate the performance penalty of different synchronization options.

We are interested in the relation between weak and strong temporal operators. We would like to find a characterization that shows what it means for an operator to be the weak or strong version of another operator, or more generally for a formula to be a weak or strong version of another formula. We show that the weak version of a formula is not the same as Alpern and Schneider's safety component. By working over an extended alphabet, we show that their topological characterization of safety can be adapted to obtain a topological characterization of weakness. We study the resulting topology and the relations between weak and strong formulas. Finally, we apply the method to show the internal consistency of a logic containing both weak and strong versions of regular expressions.

In the atomic snapshot system model, the processes of an asynchronous distributed system communicate by atomic write and atomic snapshot read operations on a shared memory consisting of single-writer multiple-reader registers. The processes may fail by crashing. It is shown that in this model, a wait-free full-information protocol complex is homotopy equivalent to the underlying input complex. A span in the sense of Herlihy and Shavit provides the homotopy equivalence. It follows that the protocol and input complexes are indistinguishable by ordinary homology or homotopy groups.

We provide a general method for ameliorating state explosion via symmetry reduction in certain asymmetric systems, such as systems with many similar, but not identical, processes. The method applies to systems whose structures (i.e., state transition graphs) have more state symmetries than arc symmetries. We introduce a new notion of "virtual symmetry" that strictly subsumes earlier notions of "rough symmetry" and "near symmetry" (Emerson and Trefler, 1999). Virtual symmetry is the most general condition under which the structure of a system is naturally bisimilar to its quotient by a group of state symmetries. We give several example systems exhibiting virtual symmetry that are not amenable to symmetry reduction by earlier techniques: a one-lane bridge system, where the direction with priority for crossing changes dynamically; an abstract system with asymmetric communication network; and a system with asymmetric resource sharing motivated from the drinking philosophers problem. These examples show that virtual symmetry reduction applies to a significantly broader class of asymmetric systems than could be handled before.

Effectively computable obstructions are associated to a distributed decision task (/spl Iscr/,/spl Oscr/,/spl Delta/) in the asynchronous, wait-free, read-write shared-memory model. The key new ingredient of this work is the association of a simplicial complex /spl Tscr/, the task complex, to the input-output relation d. The task determines a simplicial map /spl alpha/ from /spl Tscr/ to the input complex /spl Iscr/. The existence of a wait-free protocol solving the task implies that the map /spl alpha//sub */ induced in homology must surject, and thus elements of H/sub */(/spl Iscr/) that are not in the image of /spl alpha//sub */, are obstructions to solvability of the task. These obstructions are effectively computable when using suitable homology theories, such as mod-2 simplicial homology. We also extend Herlihy and Shavit's Theorem on Spans to the case of protocols that are anonymous relative to the action of a group, provided the action is suitably rigid. For such rigid actions, the quotients of the input complex and the task complex by the group are well-behaved, and obstructions to anonymous solvability of the task are obtained analogously, using the homology of the quotient complexes.