Commodification of accelerations for the Karp and Miller Construction

Karp and Miller’s algorithm is based on an exploration of the reachability tree of a Petri net where, the sequences of transitions with positive incidence are accelerated. The tree nodes of Karp and Miller are labeled with ω-markings representing (potentially infinite) coverability sets. This set of ω-markings allows us to decide several properties of the Petri net, such as whether a marking is coverable or whether the reachability set is finite. The edges of the Karp and Miller tree are labeled by transitions but the associated semantic is unclear which yields to a complex proof of the algorithm correctness. In this work we introduce three concepts: abstraction, acceleration and exploration sequence. In particular, we generalize the definition of transitions to ω-transitions in order to represent accelerations by such transitions. The notion of abstraction makes it possible to greatly simplify the proof of the correctness. On the other hand, for an additional cost in memory, which we theoretically evaluated, we propose an “accelerated” variant of the Karp and Miller algorithm with an expected gain in execution time. Based on a similar idea we have accelerated (and made complete) the minimal coverability graph construction, implemented it in a tool and performed numerous promising benchmarks issued from realistic case studies and from a random generator of Petri nets.

     

A controllable and accountable state-oriented Card-Aided Firewall

This paper proposes a new approach, named Card-Aided Firewall (CAF) that combines the simplified firewall and the state-oriented smart card technologies to construct a controllable and accountable Internet access framework. The idea suggests that a client computer, protected by a light-weight firewall, could establish diversified authenticated communication channels, controlled and accounted by “legal” states of the smart card.The program of a smart card is state-oriented or a state machine, which defines a chain of events involving various state transitions. The “legal” states of a smart card program are defined to be legal to communicate with surfing targets. A predefined Access Control List (ACL), stored in the same card, is necessary. An ACL is a sequential list of permit or deny statements that apply to addresses or upper-layer protocols. The proposed firewall decides acceptance or rejection messages by matching the current state of the card program and the ACL. In addition, a complete surfing account for tracing back is recorded. It is a by-product of the smart card authentication.The proposed Card-Aided Firewall framework is implemented to demonstrate its effectiveness. The implementation is done at the driver level. It keeps up with the high line speed. The driver takes 39K bytes and works well with other firewalls. The average packet processing time of the CAF driver is 31.74 μs. On the premise of secure authentication within the smart card, the Card-Aided Firewall would facilitate various rapidly growing applications in campus cards, family cards, and employee cards, etc. that require accurate controllability and accountability in the surfing boundary.     

A one-symbol printing automaton escaping from every labyrinth

Starting from the result of Budach [1] “No finite automaton can master every maze” automata with additional printing ability are considered. An algorithm for mastering every labyrinth using five print symbols is described. By simulation of this five-symbol-algorithm it is shown that a one-symbol print alphabet is sufficient for escaping from every labyrinth. Main result: A one-symbol, nonerasing print mouse can be constructed escaping from every labyrinth.     

The Art of the Accessibility Statement

ABSTRACT

Many libraries recognize the need to create Web sites accessible to users with disabilities, as legislated in U.S. Code Section 508, but Section 508 compliance defines a minimum legal level of accessibility. The same technology that can make a Web site available to users with disabilities can also make the site available to users with wireless devices, such as PDAs and cell phones, with Internet access. To bring about “maximum accessibility,” library Web designers need to implement Web standards. This article argues the place to begin implementing these standards is with an accessibility statement which serves as both a contract and a navigational aid.     

Computing observers from observation policies in discrete-event systems

This paper considers partially-observed discrete-event systems modeled by finite-state automata. The observation of event occurrences is associated with the transitions of the automaton model. That is, whether or not an event occurrence is observed is state-dependent, i.e., it depends on the transition in which the event label appears. This is in contrast to the case when observations are static and an event is either observed or not observed at every state in which it can occur. We refer to the set of transitions whose associated events are observed as an observation policy. Given an automaton model and an observation policy, we consider the problem of computing a deterministic generator of the language of event sequences that are observed using the automaton model and observation policy (i.e., an observer). Such a generator is useful, e.g., in problems of sensor activation for providing a deterministic mapping from event observations to sensor activation decisions when the decision to activate an event’s sensor is initially modeled as an observation policy. We propose an abstraction of the automaton model that may be used to represent an observer in certain cases. We illustrate cases where this abstraction accurately represents an observer when there is no ambiguity as to which event occurrences are observed following two observationally-identical strings. For the most general case considered, we demonstrate that verifying if the case holds is PSPACE-complete.     

Letter repeats in Enigma ciphertext produced by same-letter keying

Abstract

This paper examines the output ciphertext sequences produced by an Enigma machine that is keyed repeatedly with the same letter. The number of occurrences of runs (subsequences of successive identical characters) of different lengths is counted, and their statistics are compared with what would be expected for an ideal source of independent, equiprobable random letters from a 25-letter alphabet. Unexpectedly high run counts are found for certain rotor configurations; the “extra” runs are shown to arise from particular features of rotor wiring.     

Succinct representation of regular languages by boolean automata

Boolean automata are a generalization of finite automata in the sense that the ‘next state’, i.e. the result of the transition function given a state and a letter, is not just a single state (deterministic automata) or a union of states (nondeterministic automata) but a boolean function of states. Boolean automata accept precisely regular languages; furthermore they correspond in a natural way to certain language equations as well as to sequential networks. We investigate the succinctness of representing regular languages by boolean automata. In particular, we show that for every deterministic automaton A with m states there exists a boolean automaton with [log₂m] states which accepts the reverse of the language accepted by A (m≥1). We also show that for every n≥1 there exists a boolean automation with n states such that the smallest deterministic automaton accepting the same language has 2⁽²ⁿ⁾ states; moreover this holds for an alphabet with only two letters.     

The STAR automaton: expediency and optimality properties

We present the STack ARchitecture (STAR) automaton. It is a fixed structure, multiaction, reward-penalty learning automaton, characterized by a star-shaped state transition diagram. Each branch of the star contains D states associated with a particular action. The branches are connected to a central "neutral" state. The most general version of STAR involves probabilistic state transitions in response to reward and/or penalty, but deterministic transitions can also be used. The learning behavior of STAR results from the stack-like operation of the branches; the learning parameter is D. By mathematical analysis, it is shown that STAR with deterministic reward/probabilistic penalty and a sufficiently large D can be rendered /spl epsi/-optimal in every stationary environment. By numerical simulation it is shown that in nonstationary, switching environments, STAR usually outperforms classical variable structure automata such as L/sub R-P/, L/sub R-I/, and L/sub R-/spl epsi/P/.     

A unified concurrent-composition method to state/event inference and concealment in labeled finite-state automata as discrete-event systems

Discrete-event systems (DESs) usually consist of discrete states and transitions between them caused by spontaneous occurrences of labeled events. In this review article, we study DESs modeled by labeled (nondeterministic) finite-state automata (LFSAs). Due to the partially-observed feature of DESs, fundamental properties therein can be classified into two categories: state/event-inference-based properties (e.g., strong detectability, diagnosability, and predictability) and state-concealment-based properties (e.g., opacity). Intuitively, the former category describe whether one can use observed output sequences to infer the current and subsequent states, past occurrences of faulty events, or future certain occurrences of faulty events; while the latter describe whether one cannot use observed output sequences to infer whether secret states have been visited (that is, whether the DES can conceal the status that its secret states have been visited). Over the past two decades these properties were studied separately using different methods, and particularly, in most works inference-based properties were verified based on two fundamental assumptions of deadlock-freeness and divergence-freeness, where the former implies that an automaton will always run, the latter implies that an automaton has no reachable unobservable cycle, hence the running of such an automaton will always be eventually observed. In this article, for LFSAs, a unified concurrent-composition method is shown to verify all above inference-based and concealment-based properties, resulting in a unified mathematical framework for the two categories of properties. In addition, compared with the previous methods in the literature, the concurrent-composition method does not depend on assumptions and is currently the most efficient. Finally, based on concurrent composition, we represent the negations of the above inference-based properties as linear temporal logic (LTL) formulae; by combining the concurrent composition and an additional tool called observer (i.e., the classical powerset construction for LFSAs), we also represent the above concealment-based properties as LTL formulae. Although LTL formulae model checking algorithms do not provide more efficient verification for these inference-based and concealment-based properties, the obtained LTL formulae show common similarities among these properties.     

A syntactic methodology for automatic diagnosis by analysis of continuous time measurements using hierarchical signal representations

In this paper, we present a methodology for automatic diagnosis of systems characterized by continuous signals. For each condition considered, the methodology requires the development of an alphabet of signal primitives, and a set of hierarchical fuzzy automatons (HFAs). Each alphabet is adaptively obtained by training an adaptive resonance theory (ART2) architecture with signal segments from a particular condition. Then, the original signal is transformed into a string of vectors of primitives, where each vector of primitives replaces a signal segment in the original signal. The string, in turn, is presented to the HFA characterizing that particular condition. Each set of HFA consists of a main automaton identifying the entire signal, and several sub-automata each identifying a particular significant structure in the signal. A transition in the main automaton occurs (i.e., the main automaton moves from one state to another) if the corresponding subautomaton recognizes a token where a token is a portion of the string of vectors of signal primitives with a significant structure. The fuzziness in automaton operation adds flexibility to the operation of the automaton, enabling the processing of imperfect input, allowing for toleration measurement noise and other ambiguities. The methodology is applied to the problem of automatic electrocardiogram diagnosis.     

基于组合策略的单模式串精确匹配算法

以仅使用后缀有限自动机的RF算法作为参照对象,对采用组合策略的LDM、ILDM1、ILDM2等算法时间复杂度进行了比较研究。实验表明,LDM和ILDM1算法的时间复杂度要差于RF算法,即组合策略是失效的。实验还发现,ILDM2算法中把模式前缀长度R是否超过模式长度m的1/ 2作为正向有限自动机暂停匹配的条件,对于中小字母表的模式串的匹配也不是最佳策略。     

Observability of discrete event dynamic systems

A finite state automaton is adopted as a model for discrete event dynamic systems (DEDS). Observations are assumed to be a subset of the event alphabet. Observability is defined as having perfect knowledge of the current state at points in time separated by bounded numbers of transitions. A polynomial test for observability is given. It is shown that an observer may be constructed and implemented in polynomial time and space. A bound on the cardinality of the observer state space is also presented. A notion of resiliency is defined for observers, and a test for resilient observability and a procedure for the construction of a resilient observer are presented     

Holdings about holdings: modeling contradictions in judicial precedent

This paper attempts to formalize the differences between two methods of analysis used by judicial opinions in common law jurisdictions to contradict holdings posited by earlier opinions: “disagreeing” with the holdings of the earlier opinions and “attributing” holdings to the prior opinions. The paper will demonstrate that it is necessary to model both methods of analysis differently to generate an accurate picture of the state of legal authority in hypothetical examples, as well as in an example based on Barry Friedman’s analysis of the “stealth overruling” of Miranda v. Arizona through subsequent judicial interpretations. Because the question of whether “disagreement” and “attribution” need to be modeled separately relates to contradictions rather than to subtler interactions between holdings such as “distinguishing,” it can be answered using the simple technique of modeling holdings as propositional variables and evaluating the holdings using truth tables.     

Five-tier barrier anti-phishing scheme using hybrid approach

ABSTRACT

Though hoaxing people to make financial benefits is an old idea, phishers have realized that social engineering tools for web attacks are relatively easy to execute and are highly profitable over the Internet. One of the threatening criminal activities is phishing, in which the phishers trap users into revealing their identities and financial information to a fraudulent website. Researchers have proposed a number of anti-phishing techniques based on blacklist, whitelist, and visual similarity, but the major disadvantage with such approaches is that they are slow techniques with high false positive rates. For robust detection of phishing attacks, this article uses fundamentals of heuristic factors and a whitelist. The article proposes a safeguard scheme referred as the five-tier barrier hybrid approach. Input to the five-tier barrier is a uniform resource locator (URL), and output of the application is a status of the page (“Secure Connection” representing a legitimate URL, “Phishing Alert” representing phishing URL, and “Query Page” representing that the webpage needs to be processed further/failure of JSoup connection). In comparison to a blacklist, the five-tier barrier is competent in detecting zero-hour phishing attacks, and it is much faster than visual similarity–based anti-phishing techniques.     

On the complexity of computing the profinite closure of a rational language

Profinite topology is used in the classification of rational languages. In particular, several important decidability problems, related to the Malcev product, reduce to the computation of the closure of a rational language in the profinite topology. It is known that, given a rational language by a deterministic automaton, computing a deterministic automaton accepting its profinite closure can be done with an exponential upper bound. This paper is dedicated the study of a lower bound for this problem: we prove that, in some cases, if the alphabet contains at least three letters, it requires an exponential time.     

When does abstraction help?

Abstraction is a leading technique for coping with large state spaces. Abstraction over-approximates the transitions of the original system or the automaton that models it and may introduce nondeterminism. In applications where determinism is essential, we say that an abstraction function is helpful if, after determining and minimizing the abstract automaton, we end up with fewer states than the original automaton. We show that abstraction functions are not always helpful; in fact, they may introduce an exponential blow-up. We study the problem of deciding whether a given abstraction function is helpful for a given deterministic automaton and show that it is PSPACE-complete.     

Context-free languages over infinite alphabets

In this paper we introduce context-free grammars and pushdown automata over infinite alphabets. It is shown that a language is generated by a context-free grammar over an infinite alphabet if and only if it is accepted by a pushdown automaton over an infinite alphabet. Also the generated (accepted) languages possess many of the properties of the ordinary context-free languages: decidability, closure properties, etc.. This provides a substantial evidence for considering context-free grammars and pushdown automata over infinite alphabets as a natural extension of the classical ones. Received November 27, 1995 / March 4, 1997     

State-space support for path-based reward variables

Many sophisticated formalisms exist for specifying complex system behaviors, but methods for specifying performance and dependability variables have remained quite primitive. To cope with this problem, modelers often must augment system models with extra state information and event types to support particular variables. This often leads to models that are non-intuitive, and must be changed to support different variables. To address this problem, we extend the array of performance measures that may be derived from a given system model, by developing new performance measure specification and model construction techniques. Specifically, we introduce a class of path-based reward variables, and show how various performance measures may be specified using these variables. Path-based reward variables extend the previous work with reward structures to allow rewards to be accumulated based on sequences of states and transitions. To maintain the relevant history, we introduce the concept of a path automaton, whose state transitions are based on the system model state and transitions. Furthermore, we present a new procedure for constructing state spaces and the associated transition rate matrices that support path-based reward variables. Our new procedure takes advantage of the path automaton to allow a single system model to be used as the basis of multiple performance measures that would otherwise require separate models or a single more complicated model.