Causality in Bounded Petri Nets is MSO Definable

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F16%3A00465187" target="_blank" >RIV/67985840:_____/16:00465187 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-662-52921-8_13" target="_blank" >http://dx.doi.org/10.1007/978-3-662-52921-8_13</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-662-52921-8_13" target="_blank" >10.1007/978-3-662-52921-8_13</a>

Result language
angličtina
Original language name
Causality in Bounded Petri Nets is MSO Definable
Original language description
In this work we show that the causal behaviour of any bounded Petri net is definable in monadic second order (MSO) logic. Our proof relies in a definability vs recognizability result for DAGs whose edges and vertices can be covered by a constant number of paths. Our notion of recognizability is defined in terms of saturated slice automata, a formalism for the specification of infinite families of graphs. We show that a family G of k-coverable DAGs is recognizable by a saturated slice automaton if and only if G is definable in monadic second order logic. This result generalizes Büchi’s theorem from the context of strings, to the context of k-coverable DAGs.
Czech name
—
Czech description
—

Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)