Search

Based on the Kripke structure, linear temporal logic and generalized possibility measure, this article studies the model checking problems of generalized possibilistic fuzzy linear temporal logic (GPoFTL). The generalized possibilistic Kripke structure is introduced to describe the system model. The syntax of GPoFTL, which includes fuzzy temporal operators such as ``soon'', ``presently'', ``gradually'', ``within'', ``last'', ``nearly always'', ``almost alwayss'', ``in the long distant future'', ``in the middle of'', ``nearly until'' and ``almost until'', and its language semantics and path semantics under generalized possibility measure are given. Next, we explain the semantics of fuzzy temporal operators through some examples and prove that GPoFTL is an extension of generalized possibilistic linear temporal logic in fuzzy time temporal logic. Furthermore, the GPoFTL model checking algorithm is given by explicit calculation formulas one by one for any GPoFTL formula involving fuzzy temporal operators using fuzzy matrix operations. Last, the algorithm of necessary threshold model checking of GPoFTL is studied using automata theory and its time complexity is discussed.

The Chinese Train Control System level 3 (CTCS-3) is an open and real-time safety-critical system. Due to the non-deterministic delay behavior in the environment, there is a large number of stimuli to the train control system with different patterns of arrival times. Control strategies must be well considered, as either the logic of the function fails or the real-time constraints are dissatisfied, may directly lead to significant human injury or financial loss. In this paper, we introduce the notion of test specification and the relativized timed input/output conformance based on timed automata theory. A new test case generation and execution algorithm has been proposed, by which the tester can reset Implementation Under Test (IUT) whenever they want, make it more sense in specific domain fields. We apply UPPAAL-TRON based online conformance testing framework to test nondeterministic delay behavior of Radio Block Center (RBC) handover scenario of CTCS-3 against critical safety, real-time, and liveness properties (defined in the system requirement specification (SRS) documents). Our experiments show that assurance of collision avoidance and train non-derailment can be guaranteed, but emergency brake intervention may happen with low probability in this scenario under the requirements specified in the SRS document.

This article investigates a mission scheduling problem for earth observation satellite (EOS) with specific and temporal requirements. As is well known, the challenge is how to automatically generate an optimal actionable sequence for EOS given various physical constraints and temporal/spatial specifications that are often too intuitive to reason. To this end, we propose an automatic scheduling algorithm for EOS with the help of a linear temporal logic (LTL). In particular, LTL semantics are introduced to automate the constraints as well as temporal specifications, such that the argument of the mission specifications can be properly formulated. Toward this, we proceed to construct the state transition system by abstracting the mission objectives and specifications into a directed graph with weighted edges, and the automata theory is applied to obtain the observation sequence that satisfies the said specifications. Numerical examples verified the performance of the proposed strategy.

Cooperation among heterogeneous agricultural field robots in an agricultural environment guarantees the advantages of effectiveness and scalability. However, traditional control theories for coordination among multiple heterogeneous robots lack a systematic modeling method and a control strategy under unstructured and uncertain environments. To handle these limitations, a novel approach based on the Ramadge–Wonham theory and discrete event system is proposed in this letter. Specifications and a supervisory controller based on discrete event models were defined from an agricultural perspective considering cooperation among heterogeneous agricultural field robots. Discrete event systems were modeled through the automata theory and the behavior of heterogeneous field robots satisfied the designed specifications. The resulting supervisor ensures that the control objectives of formation control, obstacle avoidance, movements, and path following are satisfied. The approach and architecture proposed in this study were validated using a physics-based simulator and field experiments.

There are many cases in which our understanding of a system may be limited due to its complexity or lack of access into the entire system, leaving us with only partial system knowledge. This paper proposes a novel systematic active-learning method for realizing a partially-known Discrete Event System (DES). The proposed technique takes the available information about the system into account by tabularly capturing the known data from the system, and then, discovers the unknown part of the system via an active-learning procedure. For this purpose, a series of tables will be constructed to first infer the information about the system from the available data, and if unavailable, the developed algorithm collects the information through basic queries made to an oracle. It is proven that the developed technique returns a language-equivalent finite-state automaton model for the system under identification after a finite number of iterations. A real-world illustrative example is provided to explain the details of the proposed method.

ZTP and deployment of GPU-based computing are the new terms for empowering extreme automation. With notions associated with these terms come new challenges and opportunities, as well as a dramatic shift in the landscape of programming the future collaborative manufacturing systems. We have only touched the surface of this exciting topic.

Translating computation tree logic formulas into Buchi tree automata has been proven to be an effective approach for implementing branching-time model checking. For a more generalized class of lattice-valued (L-valued, for short) computation tree logic formulas, the revelent study has not proceeded yet. We introduce the notion of L-valued alternating Buchi tree automata and achieve the goal of associating each L-valued computation tree logic formula with an L-valued Buchi tree automaton. We show that a satisfiability problem for an L-valued computation tree logic formula can be reduced to one for the language accepted by an L-valued Buchi tree automaton. L-valued alternating Buchi tree automata are the key to the automata-theoretic approach to L-valued computation tree logics, and we also study their expressive power and closure properties.

In this paper we present a Timed Automata model for the Publish/Subscribe paradigm in the context of Web Service Compositions with distributed resources, on the basis of an algebraic language inspired by the WSRF standard constructions. This framework allows a set of participants in a Web Service composition to interact with one another and also to manage a collection of distributed resources. The model includes operations for clients to publish, discover and subscribe to resources, so as to be notified when the resource property values fulfill certain conditions (topic-based subscription). Simulation and model-checking techniques can therefore be applied to the obtained network of timed automata, in order to check whether certain properties of interest are satisfied. A specific case study is finally presented to illustrate the model and the verification of the relevant properties on the obtained timed automata model.

Actin is a filament-forming protein responsible for communication, information processing and decision making in eukariotic cells. To show how computation can be implemented on actin filaments we model actin as a helix of two 1-D quantum automata arrays. The model advances our previous work by exploiting the quantum aspects of the automaton (superposition). We use selected functions of automaton state transitions to compute examples of actin automata evolution and to realize three-valued logical gates in the actin automata. Implementation of operators of several three-valued logical systems is demonstrated on examples. Our results lay a ground for theoretical studies, and possible future experimental laboratory implementations of multiple-valued logical circuits.

We propose in this paper a Petri net approach to online diagnosis of discrete event systems (DESs) modeled by finite state automata. The diagnosis method is based on the construction of a Petri net diagnoser (PND) which is constructed in polynomial time and requires less memory than other methods proposed in the literature. We also present methods for the conversion of the PND to both sequential function chart and ladder diagram for implementation on a programmable logic controller (PLC). Implementation issues are also addressed in the paper.

Regular expression matching, a central task in deep packet inspection and other networking applications, has been traditionally implemented through finite automata. Thanks to their limited per-character processing and memory bandwidth requirements, deterministic finite automata (DFA) are a natural choice for memory-based implementations. In the presence of large datasets of complex patterns, however, DFA suffer from the well-known state explosion problem. Specifically, state explosion can take place during DFA generation when the considered patterns contain bounded and unbounded repetitions of wildcards or large character sets. Several alternative FA representations have been proposed to address this problem. However, these proposals all suffer from one or more of the following problems: some can avoid state explosion only on datasets of limited size and complexity; some have prohibitive worst-case memory bandwidth requirements or processing time; and some can only guarantee functional equivalence for restricted classes of regular expressions and require the user to manually filter out unsupported patterns. In this work we propose JFA, a finite automation that uses state variables to avoid state explosion, and is functionally equivalent to the corresponding DFA. Functional equivalence is guaranteed by construction without requiring user intervention. We also provide optimization techniques to both limit the amount of state variables required and provide a lower bound for the JFA traversal time.

This paper considers fault-tolerant control that ensures the safety of a discrete-event system. We consider multiple faulty modes. Each faulty mode is modeled by an automaton. These automata, together with the automaton modeling normal mode, describe a discrete-event system with faults. Each faulty mode has some illegal states that must be avoided by control so that the fault can be tolerated. We assume that fault-tolerant control takes actions (disablements) only when the occurrence of a fault is certain. We consider cases of both full event observation and partial event observation. We derive necessary and sufficient conditions for the existence of fault-tolerant control. We also provide formulas and algorithms to calculate control actions if the necessary and sufficient conditions are satisfied. Both offline control synthesis (for full event observation) and online control synthesis (for partial event observation) are investigated. We allow multiple faults as well as single faults.

Behaviour detection models based on automata have been studied widely. By adding edge e, the local automata are combined into global automata to describe and detect software behaviour. However, these methods introduce nondeterminacy, leading to models that are imprecise or inefficient. We present a model of software Behaviour Detection based on Process Algebra and system call (BDPA). In this model, a system call is mapped into an action, and a function is mapped into a process. We construct a process expression for each function to describe its behaviour. Without constructing automata or introducing nondeterminacy, we use algebraic properties and algorithms to obtain a global process expression by combining the process expressions derived from each function. Behaviour detection rules and methods based on BDPA are determined by equivalence theory. Experiments demonstrate that the BDPA model has better precision and efficiency than traditional methods.

This paper proposes a method for compositional verification of the standard and generalized nonblocking properties of large discrete event systems. The method is efficient as it avoids the explicit construction of the complete state space by considering and simplifying individual subsystems before they are composed further. Simplification is done using a set of abstraction rules preserving generalized nonblocking equivalence, which are shown to be correct and computationally feasible. Experimental results demonstrate the suitability of the method to verify several large-scale discrete event systems models both for standard and generalized nonblocking.

Automata-based scheduling is a recent technique for online scheduling of software control components in embedded systems. This letter studies one important aspect of automata-based scheduling that has not been studied in the past, namely resilience to faults. The goal of the proposed technique is to create an automaton that recommends the scheduling patterns that are admissible with respect to control performance requirements, when the state of the system has been mutated by faults. The problem has been formulated as a game between the scheduler and the (possibly faulty) system, where a winning strategy of the scheduler prevents the system from reaching bad states forever. We present a method for analyzing the structure of the game and extracting an automaton that captures the winning strategies of the scheduler, namely the automaton to be used for automata-based scheduling.

The application of model checking for the formal verification of distributed embedded systems requires the adoption of techniques for realistically modeling the temporal behavior of such systems. This paper discusses how to model with timed automata the different types of relationships that may be found among the computer clocks of a distributed system, namely, ideal clocks, drifting clocks, and synchronized clocks. For each kind of relationship, a suitable modeling pattern is thoroughly described and formally verified.

In control of discrete-event systems (DESs), specifying control requirements in automata is not a trivial task. For many DES applications, designers are often confronted with the long-standing problem of uncertainty in specification, namely, how do we know that a specification automaton does indeed model the intended control requirement? Toward a formal framework that helps mitigate this uncertainty for designer comprehensibility, in this paper, we introduce and develop a new specification concept of automaton transparency and investigate the problem of maximizing the transparency of specification automata for DESs. In a transparent specification automaton, events that are irrelevant to the specification but can occur in the system are “hidden” in self-loops. Different automata of the same specification on a DES can be associated with different sets of such irrelevant events, and any such automaton is said to be the most transparent if it has an irrelevant event set of maximal cardinality. The transparency maximization problem is theoretically formulated, and a provably correct solution algorithm is obtained. Given a specification automaton for a DES, the transparent specification automaton produced by the algorithm is a more comprehensible structure, essentially showing the precedence ordering among events from a minimal cardinality set that is relevant in modeling some requirement for the DES, and should aid designers in clarifying if the requirement prescribed is the one intended.

Traffic incident management (TIM) is a multijurisdictional process. Complications with communications, compatibility, coordination, institutional responsibilities, and legal issues are inherent in TIM systems. Increased delay in incident clearance due to various conflicts has vital economical, safety, environmental, and social impacts. Therefore, a thorough and rigorous modeling of the system is necessary to better understand its properties and systematically discern issues that may arise. The goal of this study is to develop modeling tools for the incident management process. Formal language automata theory is proposed for modeling and analysis since incident management can be viewed as a series of discrete events. Using formal methods allows us to use tools that are well established in this field to systematically study incident management processes. Formal language and automata theory are the foundation for numerous hardware and software development with applications in digital design, compilers, and programming languages. Formal language and automata theory provide us with powerful tools for developing, analyzing, and debugging such models. A systematic structure of an incident management model permits methodical identification of the system's “bugs.” This study demonstrates the development of models of some first response incident management agencies through a case study in the Las Vegas, NV, area using formal languages and automata theory. Sequence properties such as safety and liveness are verified for the developed models.

Real-time systems modeled by timed automata are often symbolically verified using Difference Bound Matrix (DBM) and Binary Decision Diagram (BDD) operations. When designing concurrent real-time systems with two or more processes sharing a resource, priorities are often used to schedule processes and to resolve conflicting resource requests. Concurrent real-time systems can thus be modeled by timed automata with priorities. However, model checking timed automata with priorities needs the DBM subtraction operation, whose result may not be convex, i.e., DBMs are not closed under subtraction. Thus, a partition of the resulting DBM is required. In this work, we propose Prioritized Timed Automata (PTA) and resolve all the issues related to the model checking of PTA. Two algorithms are proposed including an optimal DBM subtraction algorithm that produces the minimal number of DBM partitions, and a DBM merging algorithm that reduces the DBM partitions after a series of DBM subtractions. Application examples show the advantages of the proposed method in terms of support for the efficient verification of prioritized timed systems.

We consider the class of o-minimally definable hybrid automata with a bounded discrete-transition horizon. We show that for every hybrid automata in this class, there exists a bisimulation of finite index, and that the bisimulation quotient can be effectively constructed when the underlying o-minimal theory is decidable. More importantly, we give natural specifications for hybrid automata which ensure the boundedness of discrete-transition horizons. In addition, we show that these specifications are reasonably tight with respect to the decidability of the models and that they can model modern day real-time and embedded systems. As a result, the analysis of several problems for these systems admit effective algorithms. We provide a representative example of a hybrid automaton in this class. Unlike previously examined subclasses of o-minimally defined hybrid automata with decidable verification properties and extended o-minimal hybrid automata, we do not impose re-initialization of the continuous variables in a memoryless fashion when a discrete transition is taken. Our class of hybrid systems has both rich continuous dynamics and strong discrete-continuous coupling, showing that it is not necessary to either simplify the continuous dynamics or restrict the discrete dynamics to achieve decidability.

In cooperative spectrum sensing (CSS), an optimal decision fusion rule can effectively improve the performance of the secondary system. Considering that a priori knowledge about the characteristics of primary users and secondary users (SUs) is usually unknown in practice, we propose a learning automata-based algorithm to derive the optimal voting rule for decision fusion in CSS. The proposed algorithm can work with any detection method used at SUs. Its convergence and robustness are shown here. Its stability is also analyzed by using noncooperative game theory. The condition that the obtained optimal voting rule remains unchanged is derived based on the concept of subgame perfect Nash equilibrium. It is shown that the proposed algorithm generally does not need to run many times and can work at a low cost in practice. Computer simulations validate the effectiveness of the proposed scheme.

Codiagnosability and coobservability in discrete event systems where observations are dynamic are considered. Instead of having a fixed set of observable events, the observation of an event is dynamic (trace-dependent) in this paper. A procedure is developed to transform the problem of coobservability to the problem of codiagnosability in the context of dynamic observations. This proves that problems of coobservability are transformable to problems of codiagnosability and enables us to leverage the large literature available for codiagnosability to solve problems of coobservability. Furthermore, in the case of dynamic observations, the known polynomial-complexity tests for the property of codiagnosability based on verifier automata with fixed observable event set(s) are no longer directly applicable. A new testing procedure is developed that can handle transition-based dynamic observations and remains of polynomial complexity in the state space of the system. This new testing procedure employs a covering of the state space of the system based on cluster automata, which enhances its computational efficiency. Based on cluster automata, a new type of verifier automaton is built, called the C-VERIFIER, for verification of codiagnosability. As an application of the above mentioned transformation, the C-VERIFIER becomes a unified method for verifying both codiagnosability and coobservability.

The Dartmouth Summer Research Project on Artificial Intelligence, held at Datrmouth College in 1956, is regarded as the official "birthplace" of Al. This article draws on unpublished archives to shed new light on the origins of the conference and the complex relationships between cybernetics, automata studies, and Al in the 1950s.

This paper presents a symbolic pattern analysis method for robust feature extraction from sidescan sonar images that are generated from autonomous underwater vehicles (AUVs). The proposed data-driven algorithm, built upon the concepts of symbolic dynamics and automata theory, is used for detection of mines and mine-like objects in the undersea environment. This real-time algorithm is based on symbolization of the data space via coarse graining, i.e., partitioning of the two-dimensional sonar images. The statistical information, in terms of stochastic matrices that serve as features, is extracted from the symbolized images by construction of probabilistic finite state automata. A binary classifier is designed for discrimination of detected objects into mine-like and nonmine-like categories. The pattern analysis algorithm has been validated on sonar images generated in the exploration phase of a mine hunting operation; these data have been provided by the Naval Surface Warfare Center. The algorithm is formulated for real-time execution on limited-memory commercial-of-the-shelf platforms and is capable of detecting objects on the seabed-bottom.

The recommendation systems look for to offer customized products to their users. These systems identify the users preferences and the preferences of the rest of the community to the products available. This article presents a recommendation system that uses an adaptive automaton to store the relationship between resources and the users' preferences and determine the possible recommendations customized to each of its users. The details of the implementation are presented and discussed. An experiment is presented for verification and analysis of the recommendations generated in the developed system.

The paper proposes a new message passing algorithm for cycle-free factor graphs. The proposed "entropy message passing" (EMP) algorithm may be viewed as sum-product message passing over the entropy semiring, which has previously appeared in automata theory. The primary use of EMP is to compute the entropy of a model. However, EMP can also be used to compute expressions that appear in expectation maximization and in gradient descent algorithms., 5 pages, 1 figure, to appear in IEEE Transactions on Information Theory

This paper proposes a methodology for performance evaluation of schedules for job-shops modeled using tag machines. The most general tag structure for capturing dependences is shown to be inadequate for the task. A new tag structure is proposed. Comparison of the method with existing ones reveals that the proposed method has no dependence on schedule length in terms of modeling efficiency and it shares the same order of complexity with existing approaches. The proposed method, however, is shown to bear promise of applicability to other models of computation and hence to heterogeneous system models having such constituent models.

Motivated by Zadeh's paradigm of computing with words (CWs) rather than numbers, several formal models of CWs have recently been proposed. These models are based on automata and, thus, are not well suited for concurrent computing. In this paper, we incorporate the well-known model of concurrent computing, which is called the Petri net, together with fuzzy-set theory and, thereby, establish a concurrency model of CWs-fuzzy Petri nets for CWs (FPNCWs). The new feature of such fuzzy Petri nets is that the labels of transitions are some special words modeled by fuzzy sets. By employing the methodology of fuzzy reasoning, we give a faithful extension of an FPNCW that makes computing with more words possible. The language expressiveness of the two formal models of CWs, i.e., fuzzy automata for CWs as well as FPNCWs, is compared. A few small examples are provided to illustrate the theoretical development.

In this technical note we examine the relationship between linear hybrid automata (LHA) and piecewise affine (PWA) systems. While a LHA is an autonomous non-deterministic model, a PWA is a deterministic model with inputs. Through the key idea of modeling the uncertainty associated with LHA transitions as input disturbances in a PWA model, by extending continuous-time PWA models to include the dynamics of discrete states and resets we show in a constructive way that a LHA can be equivalently represented as a PWA system, where equivalent means that the two systems generate the same trajectories. Besides filling in a missing theoretical link between the LHA modelling framework and the PWA modelling framework, the result has the practical advantage of enabling the use of several existing control theoretical tools developed for PWA models to a wider class of hybrid systems.

We consider the microaggregation problem (MAP) that involves partitioning a set of individual records in a microdata file into a number of mutually exclusive and exhaustive groups. This problem, which seeks for the best partition of the microdata file, is known to be NP-hard and has been tackled using many heuristic solutions. In this paper, we present the first reported fixed-structure-stochastic-automata-based solution to this problem. The newly proposed method leads to a lower value of the information loss (IL), obtains a better tradeoff between the IL and the disclosure risk (DR) when compared with state-of-the-art methods, and leads to a superior value of the scoring index, which is a criterion involving a combination of the IL and the DR. The scheme has been implemented, tested, and evaluated for different real-life and simulated data sets. The results clearly demonstrate the applicability of learning automata to the MAP and its ability to yield a solution that obtains the best tradeoff between IL and DR when compared with the state of the art.

Timed automata have proven to be useful for specification and verification of real-time systems. System design using timed automata relies on explicit manipulation of clock variables. A number of automated analyzers for timed automata have been developed. However, timed automata lack composable patterns for high-level system design. Specification languages like Timed Communicating Sequential Process (CSP) and Timed Communicating Object-Z (TCOZ) are well suited for presenting compositional models of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchical constructs in time-enriched process algebras. The patterns facilitate the hierarchical design of complex systems using timed automata. They also allow a systematic translation from Timed CSP/TCOZ models to timed automata so that analyzers for timed automata can be used to reason about TCOZ models. A prototype has been developed to support system design using timed automata patterns or, if given a TCOZ specification, to automate the translation from TCOZ to timed automata.

Privacy is an important aspect when modeling computer systems which need to establish relationships among users and their information. To face this issue, many privacy protection mechanisms have been considered. Generic mechanisms deal with the information security of a certain user restricting a system in a way to have only relationships among subjects and objects which comply with this system rules. This paper presents an access control model formalism using adaptive automaton on a auditable privacy system. The adaptive automaton is suitable for this purpose, because of the self-modifications capacity and complex languages recognition. The model using the the proposed formalism is a new approach to privacy protection mechanisms, and is generic enough to be used not just in privacy, but in another classes of problems.

This work presents a model of software of the semantics for the adaptive automata (AA) in terms of sequences of messages between objects. The elaboration of the model is based on the formularization proposal of J.J. Neto citeneto:aa:2001 as primary origin of the class objects and its respective behaviors. Several techniques of software engineering had been used throughout the work for the elaboration of the model, such as the domain modeling, behavior specification and design patterns. The resultant model complements the original formularization providing an operational semantics for the AA.

Cement milling circuits are controlled by linear quadratic strategies with the purpose of retaining the circuit stability. Generally, the controlled variables of milling circuits present discontinuities over the range of values they take during the plant operation. The design of linear quadratic control algorithms is based on linear approximations of the nonlinear differential equations that hold over the continuous time ranges of the controlled variables. These approximations make the practical implementation of these algorithms less effective than expected and for this reason there is the need to verify the range of the variable values over which the algorithms can retain the circuit stability before commissioning them. In this paper, an alternative model to that of the nonlinear differential equations is developed for the verification of the milling circuit stability. The model is based on the rectangular hybrid automata formalism. This formalism provides a more systematic and formal way of modeling the plant operation over different ranges of variables presenting discontinuities and does not require to develop informal textual description of the conditions under which different sets of differential equations model the plant operation within the different continuous ranges of the variables. In order to use this model for verifying the circuit stability, the requirements for the circuit stability are expressed in the form of a logical proposition of the ranges of the values within which certain variables of the cement milling circuit must remain. The circuit stability is verified by finding whether the states that are defined by the logical proposition are included in the state space of the automaton. There are, however, cases in which existing algorithms that search into the state space either do not terminate or take very long times in identifying the existence or not of the desired state. After the elapse of a significant portion of time the analyst does not know whether this long time is due to algorithm termination problem or to the very large number of remaining computations. In this paper, a new algorithm was developed which does not search into the state space of the automaton as most of the other algorithms do, but computes the number of automaton iterations required for reaching a state. If this is a finite number one can conclude that the desired state is reachable. This algorithm was used in verifying the circuit stability.

This article describes new theoretical results concerning the general behavior of a feedback with carry shift register (FCSR) automaton. They help to better understand how the initial parameters must be chosen to use this automaton as a basic block of a filtered stream cipher. These results especially concern the structure of the transition graph of an FCSR automaton and the number of iterations of the FCSR transition function required to reach the main part of the graph. A potential linear weakness and a easy way to prevent the corresponding attack are also given.

The investigation of determinism issues in formal adaptive devices is particularly important when designing formal adaptive devices that must exhibit high operation performance. In the special case of adaptive formalisms, there is a serious difficulty related to determinism assurance, since their inherent self-modifying behavior makes it very difficult to assure that determinism is kept throughout the device’s operation. This work formally states the concept of determinism for adaptive finite-state automata, a class of adaptive devices that is particularly important for their relative simplicity. By studying this particular formalism, some generalizations to the adaptive devices were proposed. In addition, a set of requirements that should be satisfied in order to obtain deterministic adaptive finite-state automata were stated and a specific subclass of deterministic adaptive devices was defined.

In an earlier paper, we introduced the notion of directed control, where a directed controller, which is simply referred to as a director, is one that selects at most one controllable event to be enabled at any instant. In this paper, we develop an optimization-based approach for the design of a director: starting from any state, the worst cost to the nearest reachable marked state is minimized. The motivation is that a pending task can be completed in the least possible cost. A necessary and sufficient condition for the existence of an optimal director is obtained. Furthermore, for systems that are cycle-free, we provide an algorithm of polynomial complexity to compute an optimal director.

With rapid developments in science and technology, we now see the ubiquitous use of different types of safety-critical systems in our daily lives such as in avionics, consumer electronics, and medical systems. In such systems, unintentional design faults might result in injury or even death to human beings. To make sure that safety-critical systems are really safe, there is a need to verify them formally. However, the verification of such systems is getting more and more difficult because designs are becoming very complex. To cope with high design complexity, currently, model-driven architecture design is becoming a well-accepted trend. However, existing methods of testing and standards conformance are restricted to implementation code, so they do not fit very well with model-based approaches. To bridge this gap, we propose a model-based formal verification technique for safety-critical systems. In this work, the model-checking paradigm is applied to the Safecharts model, which was used for modeling but not yet used for verification. Our contributions listed are as follows: first, the safety constraints in Safecharts are mapped to semantic equivalents in timed automata for verification. Second, the theory for safety constraint verification is proven and implemented in a compositional model checker (that is, the state-graph manipulator (SGM)). Third, prioritized and urgent transitions are implemented in SGM to model the risk semantics in Safecharts. Finally, it is shown that the priority-based approach to mutual exclusion of resource usage in the original Safecharts is unsafe and corresponding solutions are proposed. Application examples show the feasibility and benefits of the proposed model-driven verification of safety-critical systems

Many robot systems employ logic-based or reactive controllers, making them hybrid systems (i.e., mixed discrete continuous). However, designing such control laws in a systematic manner remains a challenging task. In this paper, we apply the formal modeling paradigm to a team of mobile robots. The linear hybrid automata modeling framework is used to describe the high-level design, and the verification software HyTech is used for symbolic analysis of the description. The goal is to symbolically quantify system-level performance as a function of the design parameters, for the purpose of optimizing and synthesizing design parameters, verifying safe operation, and quantitatively exploring tradeoff issues. In order to make the analysis tractable, a series of restrictive assumptions and simplifications must be made-some dictated by the linear hybrid automata model and others necessitated by computational cost. We comment on the restrictiveness of these assumptions and the overall utility of this automated analysis approach in designing complex robotic systems

In this paper, different research trends that use symbolic techniques for robot motion planning and control are illustrated. As it often happens in new research areas, contributions to this topic started at about the same time by different groups with different emphasis, approaches, and notation. This article tries to describe a framework in which many of the current methods and ideas can be placed and to provide a coherent picture of what the authors want to do, what have they got so far, and what the main missing pieces are. Generally speaking, the aim of symbolic control as is envisioned in this article is to enable the usage of methods of formal logic, languages, and automata theory for solving effectively complex planning problems for robots and teams of robots. The results presented in this article can be divided in two groups: top-down approaches, whereby formal logic tools are employed on rather abstract models of robots; and bottom up approaches, whose aim is to provide means by which such abstractions are possible and effective. The two ends do not quite tie as yet, and much work remains to be done in both directions to obtain generally applicable methods. However, the prospects of symbolic control of robots are definitely promising, and the challenging nature of problems to be solved warrants for the interest of a wide community of researchers

Detection and diagnosis of faults in a large-scale distributed system is a formidable task. Interest in monitoring and using traces of user requests for fault detection has been on the rise recently. In this paper we propose novel fault detection methods based on abnormal trace detection. One essential problem is how to represent the large amount of training trace data compactly as an oracle. Our key contribution is the novel use of varied-length n-grams and automata to characterize normal traces. A new trace is compared against the learned automata to determine whether it is abnormal. We develop algorithms to automatically extract n-grams and construct multiresolution automata from training data. Further, both deterministic and multihypothesis algorithms are proposed for detection. We inspect the trace constraints of real application software and verify the existence of long n-grams. Our approach is tested in a real system with injected faults and achieves good results in experiments

Hardware cache behavior is an important factor in the performance of memory-resident, data-intensive systems such as XML filtering engines. A key data structure in several recent XML filters is the automaton, which is used to represent the long-running XML queries in the main memory. In this paper, we study the cache performance of automaton-based XML filtering through analytical modeling and system measurement. Furthermore, we propose a cache-conscious automaton organization technique, called the hot buffer, to improve the locality of automaton state transitions. Our results show that (1) our cache performance model for XML filtering automata is highly accurate and (2) the hot buffer improves the cache performance as well as the overall performance of automaton-based XML filtering.

This paper examines the efficacy of a novel method for anomaly detection in mechanical systems, which makes use of a hidden Markov model, derived from the time-series data of pertinent measurement(s). The core concept of the anomaly detection method is symbolic time-series analysis that is built upon the principles of Automata Theory, Information Theory, and Pattern Recognition. The performance of this method is compared with that of other existing pattern-recognition techniques from the perspective of early detection of small fatigue cracks in ductile alloy structures. The experimental apparatus, on which the anomaly detection method is tested, is a multi-degree-of-freedom mass-beam structure excited by oscillatory motion of two electromagnetic shakers. The evolution of fatigue crack damage at one or more failure sites are detected from symbolic time-series analysis of displacement sensor signals

In this note, we formalize real-time task scheduling by applying an extension of supervisory control theory (SCT) of discrete-event systems to real-time models. The set of all possible timed traces of the system is specified by a discrete timed automaton where each transition is associated with an event occurrence or the passage of one unit of time. We introduce priorities to SCT, and apply them to the setting of discrete timed automata in order to develop a formal and unified framework for task scheduling on a single CPU.

We consider control questions for finite automata viewed as input/output systems. In particular, we find estimates of the minimal number of states of an automaton able to control a given automaton. We prove that, on average, feedback closed-loop control automata do not have fewer states than open-loop control automata when the control objective is to steer the controlled automaton to a target state. We compare our approach to other ways of formalizing of formalizing analogous control objectives.

This paper presents a novel method for the scheduling and control of flexible manufacturing cells (FMCs). The approach employs automata, augmented by time labels proposed herein, for the modeling of machines, transportation devices, buffers, precedence constraints, and part routes. Ramadge-Wonham's supervisory-control theory is then used to synthesize a deadlock-free controller that is also capable of keeping track of time. For a given set of parts to be processed by the cell, A/sup */ search algorithm is subsequently employed using a proposed heuristic function. Three different production configurations are considered: Case 1) each part has a unique route; Case 2) parts may have multiple routes, but same devices in each route; and Case 3) parts may have multiple routes with different devices. The proposed approach yields optimal deadlock-free schedules for the first two cases. For Case 3, our simulations have yielded effective solutions but in practice, optimal deadlock-free schedules may not be obtainable without sacrificing computational time efficiency. One such nontime-efficient method is included in this paper. The proposed approach is illustrated through three typical manufacturing-cell simulation examples; the first adopted from a Petri-net-based scheduling paper, the second adopted from a mathematical-programming-based scheduling paper, and the third, a new example that deals with a more complex FMC scenario where parts have multiple routes for their production. These and other simulations clearly demonstrate the effectiveness of the proposed automata-based scheduling methodology.