Complementation of Büchi automata is complex as Büchi automata in general are nondeterministic. A worst-case state-space growth of O((0.76n)n) cannot be avoided. Experiments suggest that complementation algorithms perform better on average when they are structurally simple. We present a simple algorithm for complementing Büchi automata, operating directly on subsets of states, structured into state-set tuples (similar to slices), and producing a deterministic automaton. Then a complementation procedure is applied that resembles the straightforward complementation algorithm for deterministic Büchi automata, the latter algorithm actually being a special case of our construction. Finally, we prove our construction to be optimal, i.e. having an upper bound in O((0.76n)n), and furthermore calculate the 0.76 factor in a novel exact way.

Compared to many 802.11 based networks, GSM has an significant advantage. In contrast to 802.11, GSM provides a standardized authentication scheme, which requires no configuration on the end userpsilas side, but still allows international roaming. GSM does this by using a trusted module within each client: a subscriber identification module.In contrast to the comparable heavy GSM standard, the early 802.11 standards focused on data transmission within small local area networks, therefore omitting a secure and simple to use authentication mechanism. This caused several different and partly incompatible authentication schemes to evolve, ranging from simple password based login pages to certificate based mutual authentication protocols. While these protocols can provide state of the art secure authentication they are, from a user's point of view, almost unacceptable complex, especially if used in an ad-hoc manner outside an corporate environment. Trusted platform modules, as part of any modern computer, can reduce the user's overhead to establish a secure 802.11 based connection dramatically by providing secure, potentially anonymous identities. As shown in this paper this approach can be further extended by using an modified TLS handshake, allowing an automated, on-the-fly retrieval of required credentials. Together with the trusted platform modules, this extension can provide a full fledged zero configuration authentication for 802.11 networks.

This paper answers (addresses) the questions on how to detect email viruses without signatures and how to determine the probability whether the mail is abnormal and how to detect virus patterns in an infected file. In order to find out relations between email viruses and detectable knowledge, we analysed propagation of email viruses and characteristics of email viruses, studied infected files' structures and applied Bayesian networks and self-organizing maps to adaptive detection against email viruses.

The past decade has seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software systems. Recently, there has been increasing interest in applying logic programming techniques to model checking in particular and verification in general. For example, table-based logic programming can be used as an efficient means of performing explicit model checking. Other research has successfully exploited set-based logic program analysis, constraint logic programming, and logic program transformation techniques to verify systems.

Abstract The satisfaction of linear‐time temporal properties within fairness introduces an implicit fairness constraint to the verification process. To be applied to practical verification tasks, weakly continuation‐closed abstractions preserve properties satisfied within fairness. Being defined on the complete behaviour of a distributed system, weakly continuation‐closed abstractions require, in principle, an exhaustive state space construction prior to abstraction. Constructing the state space of a practically relevant specification exhaustively, however, is usually not feasible. Based on the notion of traces, i.e. certain equivalence classes of behaviours, trace reductions are defined in this paper. Trace reduction is a particular partial‐order reduction based on the persistent‐set selective search technique. It is shown that a trace reduction can be used on behalf of the complete behaviour of a distributed system in order to compute abstractions as well as to check whether the abstractions are weakly continuation closed. Thus, trace reductions allow one, in the discussed context, to overcome the requirement of an exhaustive state‐space construction prior to abstraction. Copyright © 2003 John Wiley & Sons, Ltd.

Weakly continuation-closed abstractions are known to preserve properties satisfied within fairness, i.e. linear-time temporal properties under an abstract notion of fairness. Being defined on the complete behaviour of a distributed system, weakly continuation-closed abstractions require, in principle, an exhaustive state-space construction prior to abstraction. Constructing the state-space of a practically relevant specification exhaustively, however, is usually unfeasible.

Abstract. The sh-verification tool comprises computing abstractions of finite-state behaviour representations as well as automata and temporal logic based verification approaches. To be suitable for the verification of so called co-operating systems, a modified type of satisfaction relation (approximate satisfaction) is considered. Regarding abstraction, alphabetic language homomorphisms are used to compute abstract behaviours. To avoid loss of important information when moving to the abstract level, abstracting homomorphisms have to satisfy a certain property called simplicity on the concrete (i.e. not abstracted) behaviour. The well known state space explosion problem is tackled by a compositional method combined with a partial order method.

This paper is motivated by the fact that verifying liveness properties under a fairness condition is often problematic, especially when abstraction is used.It shows that using a more abstract notion than truth under fairness, specifically the concept of relative liveness property can lead to interesting possibilities.Technically, it is first established that deciding relative liveness is a PSPACE-complete problem and it is shown that relative liveness properties ca aiways be satisfied by some fair implementation.Thereafter, the interaction between behavior abstraction and relative Iiveness properties is studied and it is proved that relative liveness properties can be verified on behavior abstractions, if the abstracting homomorphism is simple in the sense of Ochsenschlager.

No abstract available.