Search

We develop a theory of vector spaces spanned by orbit-finite sets. Using this theory, we give a decision procedure for equivalence of weighted register automata, which are the common generalization of weighted automata and register automata for infinite alphabets. The algorithm runs in exponential time, and in polynomial time for a fixed number of registers. As a special case, we can decide, with the same complexity, language equivalence for unambiguous register automata, which improves previous results in three ways: (a) we allow for order comparisons on atoms, and not just equality; (b) the complexity is exponentially better; and (c) we allow automata with guessing.

Supervisory Control Theory (SCT) is a powerful framework to design a controller for a Discrete Event System (DES). However, several issues appear because of the different nature of SCT and synchronous-based systems, on which a controller will be executed. While SCT, which relies on automata theory, is based on the occurrence of asynchronous events, a computer-based system is based on a synchronous digital system. Even though most of the contributions to overcome the problems derived by this fact concentrate on the usability for Programming Logic Controllers, no significant contribution has been made for embedded execution platform. If so, it relies on the hand-coded implementation of the supervisor controller. The work here proposed, combines previous research contributions to develop an embedded and distributed platform for supervisor automata model execution. No code translation is required, since the models, after simulation, can be directly executed on the proposed platform. The results obtained by two case studies show the feasibility of the conceived platform.

For several decades, the role of computers has been appreciated in achieving various educational goals. Computer-assisted instructions become very popular in educational settings nowadays. Various intelligent tutoring systems have been developed to support learning in different contexts. This work investigates a tutoring system for learning Finite State Machines (FSM), one of the models of computation in Automata Theory, called ILSA. ILSA was deliberately developed to appeal to learners' achievement goal orientations. Achievement Goal Orientation theory suggests that learners could be mastery-oriented or performance-oriented. Hence, the specific aim of this investigation is to examine if there is evidence of alignment between system utilization and achievement goal orientations of learners. In other words, did the learners use the features of ILSA according to their respective orientation? Results showed that the goal orientations in Post-ILSA 1 have high manifestations of alignment between utilization and achievement goal orientations.

The intelligent system controls the subsystems of each aircraft in real time to ensure the normal development of the tasks of the aircraft system. In the process of system communication, the control system is required to strictly control the correctness of the control algorithm flow and the accuracy of the control sequence in order to ensure the safety of the aircraft system. This paper uses UPPAAL, a formal model detection tool based on time automata theory, to formally model and validate the algorithm flow of an intelligent system and a subsystem. First, the algorithm flow of the intelligent system is analyzed, and then it is formally modeled using the time automaton method. Second, the properties that need to be verified are extracted from the algorithm flow and described with the formal language BNF. Finally, the function and performance correctness are automatically verified using the UPPAAL model detection tool. The experimental results verify that the intelligent system meets the security, accessibility and activity requirements.

RabbitMQ is a very popular message middleware, which is an implementation of AMQP (Advanced Message Queuing Protocol) using the Erlang language. It supports concurrency and guarantees the sequential consistency of messages. Additionally, RabbitMQ provides the message acknowledgement mechanism to ensure that messages can be delivered reliably to the consumer from the broker. However, these crucial properties have not been verified with formal methods. In this paper, we model the architecture of RabbitMQ with timed automata. By utilizing the model checker UPPAAL, RabbitMQ is abstracted to five timed automata. Based on the formalized model, we verify whether RabbitMQ meets some essential properties, including Reachability of Data, Concurrency, Sequence Consistency and Message Acknowledgement. Consequently, it can be found that RabbitMQ can totally satisfy these properties according to the verification results via UPPAAL.

Smart home is an important application scenario of the Internet of Things. However, smart home tends to suffer from runtime failures due to its complex software/hardware, unexpected/wrong human operations, environmental changes, etc. It is hard to detect the device anomalies, since smart devices have various types, various failure types, and they also generally do not expose the inner runtime information. Current anomaly detection techniques for general programs or distributed systems do not apply for smart home devices. To help both device manufactures and users to detect the device anomalies, we propose a general framework named SmartHome-Detector. It first builds a hierarchical automata based behavior model during the testing phase, and uses it as the baseline of IoT device. At runtime, a comprehensive anomaly detection technique is proposed to identify various device anomalies in time. We implement SmartHomeDetector based on the open source smart home system HomeAssistant. Our experiments and case studies on real-world smart home devices show that SmartHomeDetector is effective. It accurately models the running behavior of IoT devices and can detect various device anomalies at runtime.

Automata theory is the abstract models of machines used for capturing behavior of systems as well as compute and solve problems. The nurse rostering problem (NRP) is a well-known scheduling problem that focuses on determining the day-to-day shift assignments of each nurse. We present a method to investigate the application of automata theory which can be tailored to the requirements of a clinic to satisfy the required workload to the available staff nurses so that the operational demands can be met. It specifically helps to schedule the roster of the nurses according to the conditions of the healthcare organizations. The proposed solution illustrated how the requirements are uniquely determined by parsing them through a sequence. The output will be generated using one type of finite state transducer, mealy machine to assign the actual shift.

People use high performance computers (HPCs) for computation-intensive tasks. Often these tasks require a lot of running time of their corresponding softwares. It is important to execute several tasks simultaneously for the system utilization while finishing all tasks within their desired deadlines. Therefore, it is important to know the runtime of each computation-intensive task without executing them in order to schedule the tasks on HPC and obtain better system performance. We propose a method for predicting runtime of MPI-based softwares on HPC using automata theory and deep learning. We first analyze a source code of an input program by representing the code as finite automata and measuring their state complexities. Next, we train the execution runtime of each module of our finite automata using deep neural network (DNN) together with its own state complexity. Then we combine all modules and make a single SW-runtime-prediction model. For experiment, we train the proposed model using OSU benchmark data, HPL and two in-house datasets, and present the usefulness of our model. We also demonstrate the adaptability of our model by updating the current model for new inputs using incremental DNN, which is an important feature for coping with new softwares or new systems.

The article focuses on the application of existing provisions of the automata and graph theories to solving the problem of testing software and hardware data security tools (DST). The software and hardware DST, unlike software ones, include hardware components that implement key security functions, while preventing from using a number of testing methods and tools. In addition to the possibility of applying a particular known testing method or tool to software and hardware DST, what remains acute is the problem of ensuring completeness and optimality of such testing. The developers of various DST do not often have a clear understanding of when they can stop testing and whether the test results allow them to talk about its completeness. Accordingly, testing of DST is often spontaneous, and the developer does not understand whether all the security functions have been tested, whether all the states and all possible sets of parameters have been tested, and whether testing is being carried out in the optimal way. To eliminate these shortcomings, the authors of the article propose to use a mathematical approach based on the theories of automata and graphs to solve the problem of testing software and hardware DST, which can be also used for other software and hardware, as well as software tools and systems. Applying this approach in practice, it is possible to confirm or reject the possibility of ensuring completeness of testing a specific data security tool, as well as identifying specific measures to ensure completeness and optimality of testing.

This article describes the formalization of the signal protocol for the organization of audio and video calls via the Internet using the automata theory; the elements of the theory demonstrate the work of this protocol more clearly. Now, the Internet is an integral part of everyday life and messaging apps allow making audio and video calls. The signal protocol is the most important part in organization of such interaction and allows making a connection between users. Therefore, its formalization is actual for nowadays. The interpretation of this protocol on the non-deterministic event-driven automata allows to show its organization, all factors and problems which could be faced by developer more clearly.

As a widely used modeling language, AADL (Architecture Analysis and Design Language) plays an important role in designing safety-critical systems. It provides abundant components for describing system architecture and supports the early prediction and repetitive analysis of performance-critical attributes. However, the approach used by AADL to describe the system behavior is based mainly on automata theory; thus, encountering the state space explosion problem when modeling and verifying large and complex systems is inevitable. Furthermore, due to the lack of means to describe the behavior details, it is also difficult for AADL to support the accurate analysis and verification of functional and non-functional requirements. In this paper, we propose a language called RBML that supports refined behavior modeling to compensate for the behavior modeling and verification deficiencies of AADL. This new language is based on AADL but extends the ability to detail various behaviors and allows SMT (Satisfiability Modulo Theories) solvers to verify the constructed refined behavior model, thus alleviating the state space explosion problem to some extent. Experiments on Baidu Apollo are presented to demonstrate the feasibility of our proposed approach.

Devising an emergency evacuation plan through physical experiments is costly and inefficient. Hence, a computer-based cellular automaton model that uses microscopic approach is used to simulate emergency evacuation from a room to save costs and resources. This paper proposes a cellular automaton-based emergency evacuation simulation model which consists of two main parts. The former is a conventional cellular automaton that is used to simulate the propagation of fire and smoke, while the latter is an additional list-like data structure that is used to keep track of human movements across the cells that represent the evacuation space to overcome the former’s limitation on simultaneous changes of multiple cells. To further improve the model, human behaviour during emergency evacuation such as competing for space is also simulated through conflict resolution based on age and gender with several assumptions. Nevertheless, complex human behaviour such as herd effect is not under consideration in this model. For demonstration purpose, this model is used to simulate emergency evacuation from a computer lab based on a modifiable distance map where each cell is labelled with one of the 8 predefined states used to represent the room. Hence, it is also applicable to other types of indoor rooms.

Train-centric Train Control System (TcTCS) is a novel solution for ensuring train safety. Compared with traditional train control systems, the train undertakes more functionalities, and the controlling modes are more flexible. TcTCS has safety-critical characteristic, and its route protection is a real time process. In order to find out defects in its design logic, it is necessary to formally analyse the implementation process of route protection described in the system requirement specification (SRS). This paper analysed the implementation process of route protection and the function, performance and security requirements from SRS of TcTCS. The timed automata network model was built by UPPAAL based on the timed automata theory. Simulation was made, and properties of function, real-time and safety were verified. According to the counter-example, the model can be refined. This may help to strengthen comprehension of the system, reduce system design faults, improve safety of the system and lay a good foundation for system execution.

Virtual training complexes are used to train professional ergatic system personnel, develop the necessary practical skills and reduce the possibility of human mistake in working and emergency situations. However, the use of virtual reality tools does not provide a complete sense of realism for the trainees, so the topical problem is to develop and integrate into the training complexes various simulation systems that increase the degree of human immersion into the virtual world. In this study the problem of simulation of physical loads and realistic movement of the user in the virtual world is considered. In order to solve it, it is proposed to develop a universal software and hardware platform based on an automated treadmill, which allows organizing the user’s natural movement in a virtual environment with the ability to programmatically control various movement parameters, such as speed and incline of the running belt. Thus, it is required to implement the software of the control system, as well as the algorithmic support necessary for its work for the realization of these functions. This paper considers the general scheme of functioning of the software and hardware platform, its hardware and software components, as well as the algorithm of controlling the hardware actuating elements of the platform. The results were applied in the implementation of the control system of the software and hardware platform to ensure its correct functioning. The conducted tests of the platform allowed us to conclude about the applicability of the obtained scientific results and to formulate areas for the further research.

This paper describes a novel high-performance library collection called libbft, specially designed to deal with byzantine fault tolerance for consensus mechanisms. This library is inspired by timed automata theory, and by the groundbreaking work of Practical Byzantine Fault Tolerance (PBFT). As case study, we tackle recently proposed consensus algorithms, such as the Delegated Byzantine Fault Tolerance (dBFT) used on the NEO Blockchain. This library is organized in a multiprogramming language paradigm, being already implemented on C++ and Golang. The library handles states and transitions from regular automata machines, besides timed transitions, activated through conditions, actions and events. We also propose a mathematical notation to represent these elements, and an automatic tool to export the generated state machine into graphviz platform. We also integrate the library with state-ofthe-art communication protocols, like the gRPC (Google RPC) and protobuf, which provides efficient and language-independent communication. This paper briefly describes the technological background behind libbft, practical applications and preliminary computational experiments.

Computation and automata theory is very frequently used in the lexical analysis of compilers and programming languages, image compression, bioinformatics, morphological analysis etc., This research work proposed the design of Ludo game using automata and computation theory. Deterministic finite state automata (DFA) and Non-Deterministic finite state automata (NDFA) are used at different levels to design LUDO for multi-player gaming.

In this era, almost Every person spends 8 to 12 hours in office within a day for the sake of earn money. Offices are considered employees second home as much of the time of employees is spent over there. Employees spent their mental or physical energy to do work in offices and to get money for fulfilments of their desired needs. However, to increase the efficiency and better performance of the employees there are important steps which are followed. The modelling of smart offices provides the system view for understanding and visualizing of office management system from multiple perspectives. In this paper, the modeling and verification of smart office management system is done using UML diagrams, Automata Theory and formal specification language. The operational and behavioral model of the system is captured using UML diagrams. Automata based models are used to provide automated behavior of a system in terms of states. The consistency, accuracy and reliability of the smart office system is done using formal methods. Vienna Development Method and Specification Language (VDM-SL) is used in this paper for verification and validation of the proposed model.

Studying automata theory exposes the students to the theoretical foundation of Computer Science where they learn abstraction, generalization, and reasoning. However, teaching and learning automata is challenging because of the involved abstract notions and mathematical background. Many students experience difficulty in understanding the computability concepts. Hence, recent advances in teaching the course focus on the development of different pedagogical tools that can be used to facilitate the learning of automata theory and formal languages. Another factor that mediates student achievement is achievement goal orientation. Some students are mastery-oriented and some others are performance-oriented. Both types of learners have different learning needs. This study presents the appeal of the developed tutoring system for automata, ILSA, to the different achievement goal orientations of learners.

Internet of things (IoT) means interconnection of heterogeneous nodes implemented in order to sense input data, interpretation, processing and output within a network. The smart environment is transformed by embedding heterogeneous devices into real scenarios. In the existing work, IoT infrastructure is rarely implemented in real time scenarios because of lack of knowledge, infrastructure handling and lack of resources. The researchers have proposed many techniques to implement IoT based smart city but these do not implement the above issues effectively. In this paper, we have focused on the IoT, UML, automata and Temporal Logic of Actions (TLA+) based sewerage system of a smart city. Our proposed sewerage system is developed by UML activity diagram and then converted into Non-deterministic Finite Automata (NFA) in which a junction is represented by a state and flow of water is represented as a transition. A state of system is defined as safe if flow of wastage from one junction to another has a safe path predicting behavior of water. The proposed UML and automata-based models are then transformed into a formal model using TLA+ which has an effective model checking capability. The proof of correctness of the proposed model is provided by TLC which is a model checking facility available in TLA+ toolbox.

The intelligent management of all the processes of registration and administrative services are managed by smart campus. Smart campus provides management of clearance, transportation, departments, classrooms, offices, accounts, parking, notification and registration management system. Researchers have proposed many models to automate smart campus system using IoT, Mobile networking, cloud computing and machine learning techniques. But there is a need of more investigation of smart campus system modeling, validation and simulation. We have focused on Smart Registration system based on ubiquitous computing which is modeled using Unified Modeling Language (UML), Non-Deterministic Finite Automata (NFA) and Vienna Development Method Specification Language (VDM-SL). Registration system has many operations and functions to manage all the registration purpose tasks of the users, teachers and administration. The functions of the system include register, add or delete course, check, and view or delete Prerequisite, add or drop course, update, view or delete scheme of study. All the working of functions from one state to another is depicted in UML diagram. UML based model is further converted into Automata theory using NFA models to validate system states and transaction. The NFA based model is further converted into mathematical notations to provide proof of correctness of the model using VDM-SL. The specification is checked against the facilities available in VDM-SL to provide validation, verification and proof of correctness of proposed model.

The interconnection of heterogeneous sensing devices used to sense real environment data and to perform some actions accordingly is known as Internet of Things (IoT). Smart city is interconnection of different automated components in which sensors and actuators are embedded to handle real scenarios within a network. There are different approaches that are used to model IoT based smart city, but smart lightening system is not addressed in terms of energy efficiency and validation of the model. We have focused on smart lightening system using Unified Modelling Language (UML), Automata Theory and TLA+. In the proposed model, usage of energy is divided into three types: first is low energy usage, second is moderate and third is high. The energy usage in the system is dependent on the current state of the system. The street lights are turned on when a vehicle enters in region or there is dim light on the roads which is sensed by the embedded sensors. A region is defined as collection of sensors which detect vehicle entrance and exit and collectively on or off lights at a time by using a certain mechanism and communicate with the actors for decision making. The UML model developed using activity diagram is transformed into non-deterministic finite automata (NFA) which supports for validation of proposed model. The NFA-based model is further transformed into formal model using TLA+ which can be implemented after further refinements. The proof of correctness of proposed model is provided using TLC model checking facility.

Engineering students often find difficulties in understanding electrical diagrams, specially those from Design and Mechanical Engineering. A tool that can automatically generate the ladder diagram out of the wiring diagram would be extremely useful for them in their studies. Unfortunately, such a tool does not exist yet. We present in this paper a novel CAD tool that offers this functionality. The tool, called CADDI (standing for CAD for Electrical Diagrams) is designed to help students better understanding wiring and ladder diagrams. In CADDI, the user can either draw the ladder diagram using its graphical interface, or code the wiring diagram using a novel simple programming language, and it will automatically generate its ladder diagram. The mentioned new language was especially designed for this purpose by the students of Automata Theory and Formal Languages subject, from Computer Science Engineering degree of the University of Cadiz. In order to make CADDI accessible to all students, it was implemented as a web page. The tool has become a great assistance for students, who regularly use it during their studies.

We consider control systems where the input signal is transferred over a network and therefore, it is subject to packet losses. In this setting, the closed-loop behavior can be described as a constrained switching system. We investigate whether there exists a switching signal that prevents reachability of some target state, or alternatively, how much additional input energy is required to reach a target state in comparison to the dropout-free case. Mathematically, we formulate a reachability problem defined on a hybrid automaton and tackle an optimization problem, whose feasibility variants, the controllability and reachability properties, have been recently shown to be decidable. To do so, we provide automata-theoretic algorithms to study the properties of an appropriate generalization of the Controllability Gramian matrix. Additionally, we provide polynomial time heuristics for computations for a specific family of automata and show numerical evidence that they work well in practice. Last, we extend our observations to the analogous observability energy problem.

While automated network verification is emerging as a critical enabler to manage large complex networks, current approaches come with a high computational complexity. This paper initiates the study of communication networks whose configurations can be verified fast, namely in polynomial time. In particular, we show that in communication networks based on prefix rewriting, which include MPLS networks, important network properties such as reachability, loop-freedom, and transparency, can be verified efficiently, even in the presence of failures. This enables a fast what-if analysis, addressing a major concern of network administrators: while configuring and testing network policies for a fully functional network is challenging, ensuring policy compliance in the face of (possibly multiple) failures, is almost impossible for human administrators. At the heart of our approach lies an interesting connection to the theory of prefix rewriting systems, a subfield of language and automata theory.

Real-time systems have to be verified and tested for timely behavior as well as functional behavior. Thus, time is an extra dimension that adds to the complexity of software testing. A timed automata model with a model-checker can be used to generate timed test traces. To properly test the timely behavior, the set of test traces should challenge the different time constraints in the model. This paper describes and adapts mutation operators that target such time constraints in timed automata models. Time mutation operators apply a delta to the time constraints to help testers design tests that exceed the time constraints. We suggest that the size of this delta determines how easy the mutant is to kill and that the optimal delta varies by the program, mutation operator, and the individual mutant. To avoid trivial and equivalent time mutants, the delta should be set individually for each mutant. We discuss mutant subsumption and define the problem of finding dominator mutants in this new domain. In this position paper, we outline an iterative tuning process where a statistical model-checker, UPPAAL SMC, is used to: (i) create a tuned set of dominator time mutants, and (ii) generate test traces that kill the mutants.

Automata processing has seen a resurgence in importance due to its usefulness for pattern matching and pattern mining of "big data." While large-scale automata processing is known to bottleneck von Neumann processors due to unpredictable memory accesses, spatial architectures excel at automata processing. Spatial architectures can implement automata graphs by wiring together automata states in reconfigurable arrays, allowing parallel automata state computation, and point-to-point state transitions on-chip. However, spatial automata processing architectures can suffer from output constraints (up to 255x in commercial systems!) due to the physical placement of states, output processing architecture design, I/O resources, and the massively parallel nature of the architecture. To understand this bottleneck, we conduct the first known characterization of output requirements of a realistic set of automata processing benchmarks. We find that most benchmarks report fairly frequently, but that few states report at any one time. This observation motivates new output compression schemes and reporting architectures. We evaluate the benefit of one purely software automata transformation and show that output reporting costs can be greatly reduced (improving performance by up to 40% without hardware modification. We then explore bottlenecks in the reporting architecture of a commercial spatial automata processor and propose a new architecture that improves performance by up to 5.1x.

The CRISPR/Cas system is a bacteria immune system protecting cells from foreign genetic elements. One version that attracted special interest is CRISPR/Cas9, because it can be modified to edit genomes at targeted locations. However, the risk of binding and damaging off-target locations limits its power. Identifying all these potential off-target sites is thus important for users to effectively use the system to edit genomes. This process is computationally expensive, especially when one allows more differences in gRNA targeting sequences. In this paper, we propose using automata to search for off-target sites while allowing differences between the reference genome and gRNA targeting sequences. We evaluate the automata-based approach on four different platforms, including conventional architectures such as the CPU and the GPU, and spatial architectures such as the FPGA and Micron's Automata Processor. We compare the proposed approach with two off-target search tools (CasOFFinder (GPU) and CasOT (CPU)), and achieve over 83x speedups on the FPGA compared with CasOFFinder and over 600x speedups compared with CasOT. More customized hardware such as the AP can provide additional speedups (1.5x for the kernel execution) compared with the FPGA. We also evaluate the automata-based solution using single-thread HyperScan (a high-performance automata processing library) on the CPU. HyperScan outperforms CasOT by over 29.7x. The automata-based approach on iNFAnt2 (a DFA/NFA engine on the GPU) does not consistently work better than CasOFFinder, and only show a slightly better speedup compared with single-thread HyperScan on the CPU (4.4x for the best case). These results show that the automata-based approach provides significant algorithmic benefits, and that accelerators such as the FPGA and the AP can provide substantial additional speedups. However, iNFAnt2 does not confer a clear advantage because the proposed method does not map well to the GPU architecture. Furthermore, we propose several methods to further improve the performance on spatial architectures, and some potential architectural modifications for future automata processing hardware.

In the paper, the hybrid model of electronic design document in the form of combining set-theoretical, graph-theoretical models and automata theory using mathematical apparatus of domain specific ontologies, which include models of structure and dynamics of life cycle of electronic design document is offered. The model considered in this paper can be applied in the process of creating the integrated information environment of microelectronic systems engineering enterprise.

Programming Micron's Automata Processor (AP) requires expertise in both automata theory and the AP architecture, as programmers have to manually manipulate state transition elements (STEs) and their transitions with a low-level Automata Network Markup Language (ANML). When the required STEs of an application exceed the hardware capacity, multiple reconfigurations are needed. However, most previous AP-based designs limit the dataset size to fit into a single AP board and simply neglect the costly overhead of reconfiguration. This results in unfair performance comparisons between the AP and other processors. To address this issue, we propose a framework for the fast and fair evaluation of AP devices. Our framework provides a hierarchical approach that automatically generates automata for large datasets through user-defined paradigms and allows the use of cascadable macros to achieve highly optimized reconfigurations. We highlight the importance of counting the configuration time in the overall AP performance, which in turn, can provide better insight into identifying essential hardware features, specifically for large-scale problem sizes. Our framework shows that the AP can achieve up to 461x overall speedup fairly compared to CPU counterparts.

The rapid expansion and increased popularity of cloud computing comes with no shortage of privacy concerns about outsourcing computation to semi-trusted parties. Leveraging the power of encryption, in this project, I used Cryptoleq: an abstract machine based on the concept of one instruction set computer, capable of performing general-purpose computation on encrypted programs. Abstract machine is a theoretical model of a computer hardware or software system used in automata theory. Then, abstract mechanic are used by heterogeneous for mechanic assembly language. The encryption and decryption of data is done in same memory location. The program operands are protected using the Paillier and RSA homomorphic cryptosystem, which supports multiplication on the encrypted domain. Programming with Cryptoleq is facilitated using an enhanced assembly language that allows the development of any advanced algorithm on encrypted data sets. In our evaluation, we compare Cryptoleq's performance against a popular fully homomorphic cryptosystem i.e. Paillier and RSA.

Antimirov's partial derivatives are used in classical automata theory for the conversion of regular expressions to finite automata, tree regular expressions to tree automata, and ω-regular expressions to Buchi automata. In this paper, we describe a new variant of the Antimirov's partial derivatives for the conversion of fuzzy regular expressions to e-free fuzzy non-deterministic finite automata. The membership values in fuzzy automata are assigned by using integral lattice-ordered monoids. The resulting automaton turns out to be an improvement over the existing approaches, because it is e -free. Furthermore, herein it is formally proved that a non-deterministic fuzzy automaton M is obtained from a fuzzy regular expression r such that LR(M) LR(r).

In this paper we discuss how the web-service security can be checked using finite automata. We analyze existed attack patterns and discuss different representations for these patterns. We also consider automata equations in order to describe malicious inputs. We describe a class of such equations that have no solutions and provide some venues for a future work.

The dot-depth hierarchy of Brzozowski and Cohen classifies the star-free languages of finite words. By a theorem of McNaughton and Papert, these are also the first-order definable languages. The dot-depth rose to prominence following the work of Thomas, who proved an exact correspondence with the quantifier alternation hierarchy of first-order logic: each level in the dot-depth hierarchy consists of all languages that can be defined with a prescribed number of quantifier blocks. One of the most famous open problems in automata theory is to settle whether the membership problem is decidable for each level: is it possible to decide whether an input regular language belongs to this level? Despite a significant research effort, membership by itself has only been solved for low levels. A recent breakthrough was achieved by replacing membership with a more general problem: separation. Given two input languages, one has to decide whether there exists a third language in the investigated level containing the first language and disjoint from the second. The motivation is that: (1) while more difficult, separation is more rewarding (2) it provides a more convenient framework (3) all recent membership algorithms are reductions to separation for lower levels. We present a separation algorithm for dot-depth two. While this is our most prominent application, our result is more general. We consider a family of hierarchies that includes the dot-depth: concatenation hierarchies. They are built via a generic construction process. One first chooses an initial class, the basis, which is the lowest level in the hierarchy. Further levels are built by applying generic operations. Our main theorem states that for any concatenation hierarchy whose basis is finite, separation is decidable for level one. In the special case of the dot-depth, this can be lifted to level two using previously known results.

Automata Theory is a tool which is used in multidisciplinary computing and scientific research. It is the basis behind the traditional model of computation and is used for many purposes such as controller circuit design, sequential circuit design etc. A Sequence detector is a sequential state machine used to detect consecutive bits in a binary string. This technical paper examines various sequences and gives output as 1 if the sequence 1101 is detected. The types of the sequence examined are overlapping sequences. Algorithm designed for detecting the sequence 1101 uses flip-flops. The flip-flops help to detect the pattern in the given string.

In this note we introduce two categories, called BL-general fuzzy automata and fuzzy behavior, and then we obtain some relationship between these categories.

We investigate the synthesis of optimal controllers for continuous-time and continuous-state systems under temporal logic specifications. The specification is expressed as a deterministic, finite automaton (the specification automaton) with transition costs, and the optimal system behavior is captured by a cost function that is integrated over time. We construct a dynamic programming problem over the product of the underlying continuous-time, continuous-state system and the discrete specification automaton. To solve this dynamic program, we propose controller synthesis algorithms based on approximate dynamic programming (ADP) for both linear and nonlinear systems under temporal logic constraints. We argue that ADP allows treating the synthesis problem directly, without forming expensive discrete abstractions. We show that, for linear systems under co-safe temporal logic constraints, the ADP solution reduces to a single semidefinite program.

In this paper we consider two properties of timed automata, which help to reduce their complexity. We understand complexity as the number of time variables associated with a given timed automaton. The first property concerns redundant time variables and the second — timed automata composition.

Theoretical Computer Science area (TCS) stands out by being an important study field, and it is composed by Formal Languages and Automata Theory (FLA), Computer Science Theory (CST), and Theory of Compilers (TC). This area is responsible for introducing the beginnings of the Computer Science through formalisms - which represent a set of methods, techniques, or rules that describe the solution to a problem with restrictions - and it has a substantial impact on the student's knowledge. Computer science theory is based on the understanding of computability and techniques to solve challenges, and to improve the teaching-learning process used to introduce these concepts we proposed a Combined Methodology for Theoretical Computing (CMTC). Our methodology is based on formalism development to ground the knowledge acquired during classes of FLA, CST, and TC, where students are introduced to Theoretical Computing during one year and a half. In each course, we applied the same methodology where each student used data structures, computer graphics, and algorithms to solve problems. We address this methodology to understand how much the incomprehension of formalisms is influenced by new concepts and its abstractions. Against this background, we demonstrate that the that CMTC has the aim to build knowledge and make the new concepts and formalisms concrete. Our results are based on statistical analysis from students' grades, where we could observe among other results, the correlation between the practical activities and the conceptual knowledge.