一句话：提出 Petri 自动机识别有向标号图，证明对应 Kleene 定理，并确定无单位关系 Kleene 格等式理论为 EXPSPACE-完全。
Kleene 代数公理对语言模型和二元关系模型都是完备的：两个正则表达式识别同一语言当且仅当在二元关系模型中普遍等价。若加入交、逆和全关系运算得到 Kleene allegory，正则语言虽对这些运算封闭，但上述刻画不再成立。本文先借助已有结果，用有向标号图的语言给出新刻画；受 Petri 网启发定义有限自动机模型 Petri 自动机以识别这类图，并证明 Kleene 定理：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.