×

Causality in bounded Petri nets is MSO definable. (English) Zbl 1478.68189

Väänänen, Jouko (ed.) et al., Logic, language, information, and computation. 23rd international workshop, WoLLIC 2016, Puebla, Mexico, August 16–19th, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9803, 200-214 (2016).
Summary: 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.
For the entire collection see [Zbl 1343.03002].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B16 Higher-order logic
03D05 Automata and formal grammars in connection with logical questions
68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bauderon, M., Courcelle, B.: Graph expressions and graph rewritings. Math. Syst. Theor. 20(2–3), 83–127 (1987) · Zbl 0641.68115 · doi:10.1007/BF01692060
[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) · Zbl 1346.05249 · doi:10.1016/j.endm.2015.06.076
[3] Brandenburg, F.-J., Skodinis, K.: Finite graph automata for linear and boundary graph languages. Theor. Comput. Sci. 332(1–3), 199–232 (2005) · Zbl 1070.68064 · doi:10.1016/j.tcs.2004.09.040
[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) · Zbl 1175.68264
[5] Büchi, J.R.: Weak second order arithmetic and finite automata. Z. Math. Logik Grundl. Math. 6, 66–92 (1960) · Zbl 0103.24705 · doi:10.1002/malq.19600060105
[6] Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990) · Zbl 0722.03008 · doi:10.1016/0890-5401(90)90043-H
[7] Courcelle, B.: The monadic second-order logic of graphs V: on closing the gap between definability and recognizability. Theor. Comput. Sci. 80(2), 153–202 (1991) · Zbl 0754.68065 · doi:10.1016/0304-3975(91)90387-H
[8] Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, vol. 138. Cambridge University Press, Cambridge (2012) · Zbl 1257.68006 · doi:10.1017/CBO9780511977619
[9] de Oliveira Oliveira, M.: Hasse diagram generators and Petri nets. Fundamenta Informaticae 105(3), 263–289 (2010) · Zbl 1217.68155
[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) · Zbl 1351.68189 · doi:10.1007/978-3-642-28332-1_38
[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) · Zbl 1406.68048 · doi:10.1007/978-3-319-03898-8_12
[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). doi: 10.1007/978-3-319-25150-9_22 · Zbl 1471.68162 · doi:10.1007/978-3-319-25150-9_22
[13] Engelfriet, J., Vereijken, J.J.: Context-free graph grammars and concatenation of graphs. Acta Informatica 34(10), 773–803 (1997) · Zbl 0896.68092 · doi:10.1007/s002360050106
[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) · Zbl 0669.68015 · doi:10.1016/0304-3975(88)90124-7
[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) · Zbl 0523.68046 · doi:10.1007/BFb0036914
[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) · Zbl 1378.03032
[18] Jaffke, L., Bodlaender, H.L.: MSOL-definability equals recognizability for Halin graphs and bounded degree \[ k \] -outerplanar graphs (2015). Preprint arXiv:1503.01604 · Zbl 1378.03032
[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) · doi:10.1007/3-540-60043-4_59
[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) · Zbl 1401.03066 · doi:10.1007/3-540-63165-8_233
[21] Kaller, D.: Definability equals recognizability of partial 3-trees and \[ k \] -connected partial \[ k \] -trees. Algorithmica 27(3–4), 348–381 (2000) · Zbl 0959.68095 · doi:10.1007/s004530010024
[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) · Zbl 0936.03036 · doi:10.1007/BFb0028596
[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) · Zbl 1293.68015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.