Contents
Preface
Contributors
1. Finite Automata (Rana Barua and K. C. Gupta)
1.1 Introduction
1.2 Deterministic Finite Automata (DFA)
1.3 Nondeterministic Finite Automata (NFA)
1.4 Properties of Regular Languages
1.5 Variants of Finite Automata
1.6 Finite Automata and Logic
1.7 Conclusion
2. Large-scale Regular Expression Matching on FPGA (Yi-Hua E. Yang and Viktor K. Prasanna)
2.1 Introduction
2.2 Background
2.3 Modular RE-NFA Construction
2.4 REM Circuit Construction
2.5 REM Circuit Optimizations
2.6 Implementation Procedures on FPGA
2.7 Related Work
2.8 Conclusion
3. Finite Transducers (Javier Baliosian and Dina Wonsever)
3.1 Introduction
3.2 An Introduction to Classic FSTs
3.3 Deterministic Transducers
3.4 Weighted Finite State Transducers
3.5 Applications
4. Tree Automata (Olivier Gauwin)
4.1 Introduction
4.2 Tree Automata for Ranked Trees
4.3 Logics over Ranked Trees
4.4 Tree Automata for Unranked Trees
4.5 Further Readings
5. Timed Automata (Jun Sun, Yang Liu and Jin Song Dong)
5.1 Introduction
5.2 Timed Automata Syntax and Semantics
5.3 Verifying Timed Automata
5.4 Timed Automata Patterns
5.5 Stateful Timed CSP
5.6 Summary
6. Quantum Finite Automata (Daowen Qiu, Lvzhou Li, Paulo Mateus and Jozef Gruska)
6.1 Introduction
6.2 Preliminaries
6.3 Quantum finite automata
6.4 More powerful quantum automata
6.5 Concluding remarks and further work
7. Finite Automata Minimization (Marco Almeida, Nelma Moreira and Rogério Reis)
7.1 Introduction
7.2 Preliminaries
7.3 Minimization
7.4 Moore’s Algorithm
7.5 Hopcroft’s algorithm
7.6 Brzozowski’s algorithm
7.7 Incremental minimization
7.8 Experimental results
7.9 Conclusions
8. Incremental Construction of Finite-State Automata (Jan Daciuk)
8.1 Introduction
8.2 Basic Definitions
8.3 Insights from the Traditional Construction
8.4 Algorithm for Sorted Data
8.5 Algorithm for Data in Arbitrary Order
8.6 Semi-Incremental Construction
8.7 Extensions of the Incremental Algorithms
8.8 Bibliographical Notes
9. Esterel and the Semantics of Causality (Mohammad Reza Mousavi)
9.1 Introduction
9.2 Esterel Language: A Cook's Tour
9.3 Causality: An Informal Introduction
9.4 Structured Operational Semantics
9.5 Structured Operational Semantics for Esterel
9.6 Conclusions and Future Work
10. Regular Path Queries of Graph-Structured Data (Alex Thomo and S. Venkatesh)
10.1 Introduction
10.2 Graph-Structured Databases and Regular Path Queries
10.3 Query Answering Using Views
10.4 Maximal View-Based Rewritings
10.5 Optimization Techniques
10.6 Experimental Results
11. Applying Timed Automata to Model Checking of Security Protocols (Miroslaw Kurkowski and Wojciech Penczek)
11.1 Introduction to security protocols
11.2 Examples of protocols
11.3 Specification and verification of protocol properties
11.4 Automata based methods of protocols verification
11.5 Syntax of Timed Cryptographic Protocols
11.6 Computational Structure
11.7 Networks of Synchronizing Timed Automata
11.8 Experimental Results
11.9 Conclusions and Perspectives
12. Optimal Adaptive Pattern-Matching Using Finite State Automata (Nadia Nedjah and Luiza de Macedo Mourelle)
12.1 Introduction
12.2 Preliminaries
12.3 Adaptive Tree Matching Automata
12.4 Optimal Adaptive Matching Automata
12.5 Adaptive Dag Automata Construction
12.6 Automaton State Equivalence
12.7 Automaton Complexity
12.8 Conclusion
13. Finite Automata in Compiler Design (Yang Zhao)
13.1 Introduction
13.2 Lexical Analysis
13.3 Syntax Analysis
13.4 Conclusion
14. Finite State Models for XML Processing (Murali Mani)
14.1 Introduction
14.2 XML Validation
14.3 XML Processing
14.4 Conclusions
15. Petri Nets (Jiacun Wang)
15.1 Introduction
15.2 Graphic Representations
15.3 Formal Definition
15.4 Modeling Power
15.5 Petri Net Analysis
15.6 Petri Net Properties
15.7 Colored Petri Nets
15.8 Timed Petri Nets
15.9 Continuous Petri Nets and Hybrid Petri Nets
15.10 Concluding Remarks
16. Statecharts (Hanlin Lu and Sheng Yu)
16.1 Introduction
16.2 Basic Elements of Statecharts
16.3 The Computing Power of Statecharts
16.4 Conclusion
17. Temporal Logic and Model Checking (Zhenhua Duan and Cong Tian)
17.1 Principle of Model Checking
17.2 Basic Model Checking Scheme for PLTL
17.3 Model Checking Scheme for CTL
17.4 Model Checking Scheme for PITL and PPTL
17.5 Unified Model Checking with PTL
17.6 State Space Explosion Problem
18. System Modeling with UML State Machines (Omar El Ariss and Dianxiang Xu)
18.1 Introduction
18.2 UML Behavioral state machines
18.3 States
18.4 Transitions
18.5 Events
18.6 Pseudostates
18.7 Final State
18.8 System Design and Component Communication
18.9 Applications of UML State Machines
18.10 Summary
Index