Recognition of Forbidden Pattern - 0.3alpha
This software provides algorithms for checking if languages is in special language classes.
In special we use an forbidden pattern approach to decide if language defined with an
deterministic finite automate.
We can decide the following classes: \(\mathcal B_{1/2,1}\) and \(\mathcal L_{1/2,1,3/2}\).
\[\newcommand\mathdef{{=_{\text{def}}}}
\newcommand\lclass[1]{{\mathcal{#1}}}
\newcommand\dea[1]{{\mathcal{#1}}}
\newcommand\reg[1]{{\mathbf{#1}}}
\let\notmodels\nvDash\]\[\DeclareMathOperator{\Pol}{Pol}
\DeclareMathOperator{\FU}{FU}
\DeclareMathOperator{\BC}{BC}
\DeclareMathOperator{\co}{co}
\DeclareMathOperator{\BFS}{BFS}
\DeclareMathOperator{\ZK}{ZK}
\DeclareMathOperator{\sZK}{sZK}\]\[\DeclareMathOperator{\first}{first}
\DeclareMathOperator{\last}{last}
\DeclareMathOperator{\append}{append}\]\[\newcommand\FP{\ensuremath{\mathcal{FP}}\xspace}\]
The classes of the dot depth hierarchy is defined as follows:
\[\begin{split}\begin{align}
\lclass B_{1/2} &\mathdef ~ \FU( w_0\Sigma^* w_1 \Sigma^* \cdots \Sigma^* w_n)
&& \text{für } n\ge 0 \wedge w_i \in \Sigma^*, \\
\lclass B_{n+1} &\mathdef \BC(\lclass B_{n+1/2}) && \text{für } n \ge 0 \text{ und}\\
\lclass B_{n+3/2} &\mathdef \Pol(\lclass B_{n+1})&& \text{für } n \ge 0\text{.}
\end{align}\end{split}\]
The classes of the Straubin-Therien depth hierarchy is defined as follows:
\[\begin{split}\begin{align}
\lclass L_{1/2} &\mathdef ~ \FU(\Sigma^*a_1\Sigma^* \cdots \Sigma^* a_m\Sigma^*)
&& \text{für } m \ge 0 \wedge a_i \in \Sigma, \\
\lclass L_{n+1} &\mathdef \BC(\lclass L_{n+1/2}) && \text{für } n \ge 0 \text{ und}\\
\lclass L_{n+3/2} &\mathdef \Pol(\lclass L_{n+1}) && \text{für } n \ge 0 \text{.}
\end{align}\end{split}\]
\(\FU\) is the finite union. \(\BC\) the boolean closure under complement, intersection and union. \(\Pol\) the polynominal closure (\(\FU + \cdot\)).
If you need more information you should refer to [Weigl12] and [Schm00] as the primary sources. [Weigl12] explains the algorithms and [Schm00] the forbidden patterns.
Dependencies:
Software Overview
- Modules
- dea: utilities for the algorithms
- trap: for loading DFA in xml files. see http://trap.fh-trier.de for more information about TrAP
- algorithms: this module contains the decision algorithms
- witnesscheck: special module for providing a control mechanism for the decision algorithm
- generator: Prototype and framework for generating algorithms
- Scripts
-
License
This software is license under GPL 3
Citation
primary:
| [Weigl12] | (1, 2) Weigl, Alexander: Algorthims for Forbidden Pattern Detection in Transitiondiagrams; 2012 (German). |
secondary:
| [AB02] | Asteroth, Alexander; Baier, Christel: Theoretische Informatik - Eine Einführung in Berechenbarkeit, Komplexit und formale Sprachen mit 101 Beispielen. Pearson Studium, 2002 |
| [CLRS09] | Cormen, Thomas H.; Leiserson, Charles E.; Rivest, Ronald L.; Stein, Clifford: Introduction to Algorithms, Third Edition. 3rd. The MIT Press, 2009. |
| [CPP93] | Cohen, Jo ̈lle; Perrin, Dominique; Pin, Jean-Eric: On the expressive power of temporal logic. In: Journal of Computer and System Sciences 46 (1993), Nr. 3, 271 - 294. |
| [HL11] | Hofmann, M.; Lange, M.: Automatentheorie und Logik. Springer Verlag, 2011. |
| [Rot08] | Rothe, Jörg: Komplexit ̈tstheorie und Kryptologie: Eine Einführung in Kryptokomplexit. Gabler Wissenschaftsverlage, 2008. |
| [Tar72] | Tarjan, Robert E.: Depth-First Search and Linear Graph Algorithms. In: SIAM J. Comput. 1 (1972), Nr. 2, S. 146–160 |
