Causality in Bounded Petri Nets is MSO Definable
Pages 200 - 214
Abstract
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 $$\mathfrak {G}$$ of k-coverable DAGs is recognizable by a saturated slice automaton if and only if $$\mathfrak {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.
References
[1]
Bauderon, M., Courcelle, B.: Graph expressions and graph rewritings. Math. Syst. Theor. 202---3, 83---127 1987
[2]
Bodlaender, H.L., Heggernes, P., Telle, J.A.: Recognizability equals definability for graphs of bounded treewidth and bounded chordality. In: Proceedings of the 7th European Conference on Combinatorics EUROCOMB 2015 2015
[3]
Brandenburg, F.-J., Skodinis, K.: Finite graph automata for linear and boundary graph languages. Theor. Comput. Sci. 3321---3, 199---232 2005
[4]
Bruggink, H.S., König, B.: On the recognizability of arrow and graph languages. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. eds. ICGT 2008. LNCS, vol. 5214. Springer, Heidelberg 2008
[5]
Büchi, J.R.: Weak second order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66---92 1960
[6]
Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 851, 12---75 1990
[7]
Courcelle, B.: The monadic second-order logic of graphs V: on closing the gap between definability and recognizability. Theor. Comput. Sci. 802, 153---202 1991
[8]
Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, vol. 138. Cambridge University Press, Cambridge 2012
[9]
de Oliveira Oliveira, M.: Hasse diagram generators and Petri nets. Fundamenta Informaticae 1053, 263---289 2010
[10]
de Oliveira Oliveira, M.: Canonizable partial order generators. In: Dediu, A.-H., Martín-Vide, C. eds. LATA 2012. LNCS, vol. 7183, pp. 445---457. Springer, Heidelberg 2012
[11]
de Oliveira Oliveira, M.: Subgraphs satisfying MSO properties on z-topologically orderable digraphs. In: Gutin, G., Szeider, S. eds. IPEC 2013. LNCS, vol. 8246, pp. 123---136. Springer, Heidelberg 2013
[12]
de Oliveira Oliveira, M.: MSO logic and the partial order semantics of place/transition-nets. In: Leucker, M., Rueda, C., Valencia, F.D. eds. ICTAC 2015. LNCS, vol. 9399, pp. 368---387. Springer, Heidelberg 2015.
[13]
Engelfriet, J., Vereijken, J.J.: Context-free graph grammars and concatenation of graphs. Acta Informatica 3410, 773---803 1997
[14]
Gaifman, H., Pratt, V.R.: Partial order models of concurrency and the computation of functions. In: LICS 1987, pp. 72---85 1987
[15]
Gischer, J.L.: The equational theory of pomsets. Theor. Comput. Sci. 61, 199---224 1988
[16]
Goltz, U., Reisig, W.: Processes of place/transition-nets. In: Díaz, J. ed. ICALP 1983. LNCS, vol. 154, pp. 264---277. Springer, Heidelberg 1983
[17]
Jaffke, L., Bodlaender, H.L.: Definability equals recognizability for k-outerplanar graphs. In: Proceedings of the 10th International Symposium on Parameterized and Exact Computation, IPEC 2015. LIPIcs, vol. 43, pp. 175---186 2015
[18]
Jaffke, L., Bodlaender, H.L.: MSOL-definability equals recognizability for Halin graphs and bounded degree $$k$$-outerplanar graphs 2015. Preprint arXiv:1503.01604
[19]
Jagadeesan, L.J., Jagadeesan, R.: Causality and true concurrency: a data-flow analysis of the pi-calculus. In: Alagar, V.S., Nivat, M. eds. AMAST 1995. LNCS, vol. 936, pp. 277---291. Springer, Heidelberg 1995
[20]
Kabanets, V.: Recognizability equals definability for partial $$k$$-paths. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. eds. ICALP 1997. LNCS, vol. 1256, pp. 805---815. Springer, Heidelberg 1997
[21]
Kaller, D.: Definability equals recognizability of partial 3-trees and $$k$$-connected partial $$k$$-trees. Algorithmica 273---4, 348---381 2000
[22]
Langerak, R., Brinksma, E., Katoen, J.-P.: Causal ambiguity and partial orders in event structures. In: Mazurkiewicz, A., Winkowski, J. eds. CONCUR 1997. LNCS, vol. 1243, pp. 317---331. Springer, Heidelberg 1997
[23]
Lapoire, D.: Recognizability equals monadic second-order definability for sets of graphs of bounded tree-width. In: Morvan, M., Meinel, C., Krob, D. eds. STACS 1998. LNCS, vol. 1373, pp. 618---628. Springer, Heidelberg 1998
[24]
Petri, C.A.: Fundamentals of a theory of asynchronous information flow. In: Proceedings of IFIP Congress 62, Munchen, pp. 166---168 1962
[25]
Thomas, W.: Finite-state recognizability of graph properties. Theorie des Automates et Applications 172, 147---159 1992
[26]
Vogler, W. ed.: Modular Construction and Partial Order Semantics of Petri Nets. LNCS, vol. 625. Springer, Heidelberg 1992
- Causality in Bounded Petri Nets is MSO Definable
Recommendations
MSO definable string transductions and two-way finite-state transducers
We extend a classic result of Büchi, Elgot, and Trakhtenbrot: MSO definable string transductions i.e., string-to-string functions that are definable by an interpretation using monadic second-order (MSO) logic, are exactly those realized by deterministic ...
How unprovable is Rabin's decidability theorem?
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer ScienceWe study the strength of set-theoretic axioms needed to prove Rabin's theorem on the decidability of the MSO theory of the infinite binary tree. We first show that over the second-order arithmetic theory ACA0, the complementation theorem for ...
Forcing MSO on Infinite Words in Weak MSO
LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer ScienceWe propose a forcing-based interpretation of monadic second-order logic (MSO) on infinite (omega) words in Weak MSO (WMSO). The interpretation is purely syntactic. We show that a formula with parameters is true in MSO if and only if its interpretation ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 16 August 2016
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 05 Mar 2025