Petri Automata
Petri Automata
复制标题
皮氏自动机
DOI：
10.23638/lmcs-13(3:33)2017
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Damien Pous
中科院分区：
文献类型：
--
作者：
Paul Brunet;Damien Pous
Kleene代数公理对于语言模型和二元关系模型都是完备的。特别是，两个正则表达式识别同一种语言，当且仅当它们在二元关系模型中是通用等价的。我们认为克林寓言，即，带有两个附加运算和一个常数的Kleene代数，这在二元关系模型中是很自然的：交集，匡威和全关系。虽然常规语言在这些操作下是封闭的，但上述特征化被打破了。把几个结果从文献中，我们给出了一个表征的语言的有向图和标记图。从Petri网的灵感，我们设计了一个有限的自动机模型，Petri自动机，允许识别这样的图形。我们证明了一个Kleene定理，这个自动机模型：由Petri自动机识别的图形集正是通过我们考虑的扩展正则表达式定义的图形集。Petri自动机允许我们获得无身份关系Kleene格的可判定性，即，等式理论生成的二元关系上的签名正则表达式与交集，但其中一个禁止单位。此限制用于确保相应的图是非循环的。我们实际上证明了这个决策问题是EXPSPACE完全的。
Kleene algebra axioms are complete with respect to both language models and binary relation models. In particular, two regular expressions recognise the same language if and only if they are universally equivalent in the model of binary relations. We consider Kleene allegories, i.e., Kleene algebras with two additional operations and a constant which are natural in binary relation models: intersection, converse, and the full relation. While regular languages are closed under those operations, the above characterisation breaks. Putting together a few results from the literature, we give a characterisation in terms of languages of directed and labelled graphs. By taking inspiration from Petri nets, we design a finite automata model, Petri automata, allowing to recognise such graphs. We prove a Kleene theorem for this automata model: the sets of graphs recognisable by Petri automata are precisely the sets of graphs definable through the extended regular expressions we consider. Petri automata allow us to obtain decidability of identity-free relational Kleene lattices, i.e., the equational theory generated by binary relations on the signature of regular expressions with intersection, but where one forbids unit. This restriction is used to ensure that the corresponding graphs are acyclic. We actually show that this decision problem is EXPSPACE-complete.